23 mars 2026 à 13h30
Alexandre Moine, postdoc at New York University
Abstract:
Bugs in critical software can ground airplanes, disable hospitals, or compromise security infrastructure, and this list will only grow in the era of LLM-generated code. Program logics are the gold standard for verifying precise and rigorous specifications, yet they suffer from two shortcomings. First, they remain difficult to use, particularly in the presence of parallelism and other advanced programming features. Second, standard program logics certify correctness but not efficiency, leaving the door open to efficiency bugs, which are notoriously difficult to detect and fix.
In this talk, I start to address these shortcomings and present the two sides of my research: verifying efficient programs and proving their efficiency. First, I present Musketeer and Angelic, a new framework for verifying parallel programs when parallel tasks do not logically interfere with each other. This framework reduces concurrent verification to reasoning about a single execution, dramatically lowering proof complexity. Second, I present Irisfit, a program logic for formally verifying space complexity in the presence of garbage collection, where the absence of explicit deallocation makes resource reasoning subtle and context-sensitive. This work led to the discovery of space overconsumption bugs in OCaml. To provide one of the highest possible levels of confidence, all the tools I develop are formally mechanized in a proof assistant, serving in particular as a bedrock for certifying LLM-generated proofs.
Looking forward, I outline my research agenda connecting high-level reasoning principles, covering parallelism, cache locality, and resource consumption to low-level guarantees through verified compilers and runtimes.
Salle Agora 1, Bâtiment ESPRIT
français
English