N40AI 2024
as the organisers put it
The purpose of the Next 40 years of Abstract Interpretation (N40AI) event is to gather ”4 generations of PhDs in abstract interpretation” and to reflect on the past, current, and future research trends in this field. Abstract interpretation was proposed in the 1970s by Patrick Cousot and Radhia Cousot as a general formalism to compare program semantics. The landmark papers at POPL’77 and POPL’79 have inspired an impressive amount of works by many generations of researchers, on the foundations of program semantics, program analysis, program transformations, applications in making computer s ...
who it's for
abstract interpretation researchers, formal verification engineers, static analysis engineers, programming languages researchers, security engineers, tool builders and integrators, compiler engineers
topics
mechanized abstract interpretation in Coq; extraction to OCaml executable analyzers; reduced-product program synthesis; bit-manipulation inductive synthesis; quantum abstract interpretation; verification of quantum programs; scaling deductive verification with AI; EVM and Wasm bytecode verification; unique pointer analysis for bump allocation; incremental analyzers for pull requests
| title | author | length |
|---|---|---|
| Mechanizing Abstract Interpretation | Xavier Leroy | 46m |
Mechanizes abstract interpretation using Coq and produces an executable analyzer extracted to OCaml; 30,000 lines of Coq implement Verasco with interval… | ||
| Program Synthesis via Bi-directional Reduced-product Abstract Interpretation | Kwangkeun Yi, Yongho Yoon, Woosuk Lee | 39m |
Claims that a forward-and-backward abstract interpretation pipeline with a reduced-product of simple domains (bitwise, unsigned interval, sign interval) plus… | ||
| Quantum Abstract Interpretation | Jens Palsberg, Nengkun Yu | 41m |
Claims that abstract interpretation can verify quantum program assertions in polynomial time by representing abstract states as tuples of local projections and… | ||
| Trust but Verify: Scaling Deductive Verification with Abstract Interpretation | Mooly Sagiv | 50m |
Certora Prover verifies EVM and Wasm bytecode by combining abstract interpretation with SMT solving, an internal decompiler to a TP IR, and mutation testing… | ||
| AI for the People | Peter W. O'Hearn | 51m |
Built an incremental Infer-based analyzer that runs on code changes against 100,000 commits per week, comments on pull requests and shifts fix rate from… | ||
| Unified Compositional Symbolic Execution | Philippa Gardner | 41m |
Claims a unified engine that combines OX (correctness) and UX (incorrectness) reasoning via an axiomatic interface and parametric consume/produce functions… | ||
| Short talks: Past, Present and Future of AI | Roberto Giacobazzi, Eric Goubault, Laurent Mauborgne, Dominique Mery, David Monniaux, Andreas Podelski, David Schmidt, Reinhard Wilhelm | 01h 30m |
A rapid history of abstract interpretation that traces concrete claims and engineering outcomes: presents the formal method used to analyze Airbus C code with… | ||
| nothing matches | ||