Manuel Rigger

DuckDB was added to the wall of fame of CWI, next to Dijkstra’s shortest path algorithm, the Atlantic Crossing of the Internet & the creation of Python

On the occasion of our 80th (really!) bday

Congrats to @hannes.muehleisen.org & @markraasveldt.bsky.social

@duckdb.org
@cwi-amsterdam.bsky.social

New post on "Proofs and Intuitions": Verifying Distributed Protocols in Veil.

We take a tour of Veil, a Lean-based verification framework that combines TLA+-style model checking with formal proofs and enables AI-powered invariant inference.

proofsandintuitions.net/2026/02/09/d...

You can find more details on the fees and program here: fuzzingsummerschool.github.io/Registration...

Posting on behalf of the organizing team: @abhikrc.bsky.social, @umathur.bsky.social, Vivien Hao, Zhenkai Liang, and myself.

We are organizing the third edition of the "Fuzzing and Software Security Summer School 2026", at NUS on 26th–29th May 2026. We have a stellar set of speakers and will also have a Hackathon. Please share, and/or consider joining! fuzzingsummerschool.github.io/index.html

Thanks a lot to @umathur.bsky.social and Djordje Zikelic (as well as to @93mschwarz.bsky.social) for organizing the second edition of the Singapore Programming Languages Summit! It's great to see the growing community of PL researchers in Singapore. sg-pl-summit.github.io

FM-Fuzz: Continuous Fuzzing and AI-based Bug Fixing for Formal Methods at The University of Manchester on FindAPhD.com PhD Project - FM-Fuzz: Continuous Fuzzing and AI-based Bug Fixing for Formal Methods at The University of Manchester, listed on FindAPhD.com

We are hiring!

Suzanne Embury and I are looking for a talented Ph.D. student 👩‍🎓👨‍🎓 to join an exciting, high-impact project on automated testing and bug fixing of Formal Methods tools.

www.findaphd.com/phds/project...

Gaetano's paper on Scaling Security Testing by Adressing the Reachability Gap has been accepted at #ICSE26!

📝 gpsapia.github.io/files/ICSE_2...
🧑‍💻 github.com/GPSapia/Reac...

How to scale automatic security testing to arbitrary systems?

Had a blast at my first Google Summer of Code (GSoC) Mentor Summit. My personal highlight was speaking with the developers of many important open-source projects and learning about the various challenges they face. Hopefully, we can help address some of those with our research.

Thanks to @ningkeli.bsky.social and Yibo Dong for co-organizing!

We finished the second @icfp-conference.bsky.social/SPLASH hike! We spotted multiple crocodiles, lizards, macaques, mudskippers, various fishes (e.g., archerfish and halfbeaks), birds (hornbills, kingfishers, herons, and egrets), bats, and snakes (oriental whip snake and some a king cobra).

Super excited by the SPLASH ACM Student Research Competition (SRC) results! @junwenan.bsky.social won the gold medal in the graduate category, while Emily Ong won in the undergraduate category! By the way, Junwen is looking for summer internship positions.

Outdoor Activities - SPLASH 2025 Latest Announcements Information for presenters at NUS (Sunday) and at MBS (Monday-Saturday) is now available! Official tag for social media posting about the conference is #icfpsplash25 If you’re pl...

A reminder that we will have another @icfp-conference.bsky.social/SPLASH nature walk planned for tomorrow. Consider joining if you are (still) in Singapore! 2025.splashcon.org/attending/ou...

It seems the first hike as part of @icfp-conference.bsky.social/SPLASH went well! A shoutout to @ningkeli.bsky.social and Yibo DONG (as well as my wife, Ting), who guided the participants on this walk. I could unfortunately not participate, as I had to travel abroad due to an urgent issue.

I am thrilled to announce Velvet: a new foundational multi-modal verifier for imperative programs in Lean.

Velvet unifies execution, testing, automated and interactive proofs; and is itself proven sound.

💻 github.com/verse-lab/loom
📄 verse-lab.github.io/papers/loom-...

ICFP/SPLASH 2025 Latest Announcements Information for presenters at NUS (Sunday) and at MBS (Monday-Saturday) is now available! The registration is now open. Early Registration deadline: 31 August 2025. Activities ...

One week until ICFP/SPLASH’25!

conf.researchr.org/home/icfp-sp...

First Day: A New Chapter at the JKU

It's Wednesday. Is this important? It's my first day in a new position. So, perhaps the real question is: what's going to be important to me from now on?

stefan-marr.de/2025/10/firs...

Front page of a paper titled "Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM" by Ao Li et al. from Carnegie Mellon University.

Excited to announce that the Fray paper has been accepted to OOPSLA'25! Work led by @aoli.al with a full pastalab.org collaboration.

📄: rohan.padhye.org/files/fray-o...
💻: github.com/cmu-pasta/fray
🎥: www.youtube.com/watch?v=AX6P...

To set expectations: on some other days, we saw close to nothing on the same hike.

I will be organizing two nature walks for ICFP/SPLASH (‪@icfp-conference.bsky.social‬)! I did one of them this weekend and was very lucky to see 11 saltwater crocodiles (including a tiny baby one), countless monitor lizards, otters, macaques, fruit bats, various kinds of birds, and fish.

MPLR 2025 - ICFP/SPLASH 2025 The 22nd International Conference on Managed Programming Languages and Runtimes (MPLR 2025, formerly ManLang, originally PPPJ) is a premier forum for presenting and discussing novel results in all asp...

Already registered for SPLASH or @icfp-conference.bsky.social?

If not, check out our list of accepted papers:

conf.researchr.org/home/icfp-sp...

It's language implementation techniques, from debugging and JIT compiling on microcontrollers to visualizing execution patterns between CPU and GPU!

25yrs of delta dbg

25 years of delta debugging! On this day in 2000, I presented “Simplifying Failure-Inducing Inputs” at ISSTA - now one of the most influential works in the 50-year history of Transactions on Software Engineering. Read all about its genesis and impact at doi.ieeecomputersociety.org/10.1109/TSE....

Do it for science!

Estimating Correctness Without Oracles in LLM-Based Code Generation Generating code from natural language specifications is one of the most successful applications of Large Language Models (LLMs). Yet, they hallucinate: LLMs produce outputs that may be grammatically c...

Can we statistically estimate how likely an LLM-generated program is correct w/o knowing what is a correct program for that task?

Sounds impossible-but it's actually really simple. In fact, our measure of "correctness" called incoherence can be estimated (PAC guarantees).

arxiv.org/abs/2507.00057

SQuaLity is a unified database system test suite. Currently, database test suites are not systematically re-used across systems. We explore the opportunities and challenges of doing so. Reusing test suites is difficult due to multiple factors, but also allows finding otherwise overlooked bugs.

CODDTest is a new testing approach for finding logic bugs in relational database systems. We got inspiration from constant folding and propagation and compilers; by ensuring that the database state is constant, we can fold elements of a query to then check whether its result remains unchanged.

Our second paper is on finding bugs in graph libraries and databases. The key insight behind "Graph-Cutting" is that graph algorithms are sensitive to graph structures. By dividing one graph into multiple subgraphs, we can infer checkable relationships between the results while stressing the system.

We will present "Affine Equivalent Inputs", an approach to finding logic bugs in spatial databases like PostGIS. The key contribution of the paper is a new test oracle. If we apply an affine transformation like rotation to two geometries, topological relationships like intersection are preserved.