PLDI 2024 Workshop Honoring Andreas Podelski
as the organisers put it
This event will honor Andreas Podelski on the occasion of his 65th birthday. The program will feature talks by Andreas’ collaborators, colleagues, and friends to celebrate his numerous contributions to the field of program analysis and verification. All PLDI 2024 attendees are welcome!
who it's for
program verification researchers, formal methods tool developers, theorem prover users, model checking engineers, SMT and solver developers, software verification engineers
topics
cesan abstraction for parameterized verification; partial order reduction for executions; monitors and test generators from specs; embedding logics inside theorem provers; Boogie memory model encodings; liveness-to-safety via fair abstract lasso; temporal prophecy witness constants; Rust message-passing DSL model checking; optimal quantum circuit compilation; Hilbert epsilon choice terms in SMT; FM-Tools repository for reproducible artifacts; Cartesian abstraction and linear ranking functions
| title | author | length |
|---|---|---|
| Closing Remarks | Andreas Podelski | 15m |
Proposes combining partial order reduction with parameterized verification by using cesan abstraction to summarize unmodeled threads, and studies whether to… | ||
| Living inside a Theorem Proving Universe | Natarajan Shankar | 41m |
Talk argues for working entirely inside a theorem prover by embedding other logics, languages and tools and shows concrete wins and costs. Examples include… | ||
| On the Power of Temporal Prophecy | Jochen Hoenicke | |
Shows a reduction of liveness/termination to safety in uninterpreted first‑order logic using a fair abstract lasso and a nondeterministic monitor automaton… | ||
| Liveness to Safety for Distributed Systems | Lenore Zuck | 28m |
Claims a mechanical reduction of liveness to safety by encoding justice (weak fairness) as finite planners — finite sequences of fairness conditions — and… | ||
| Model Checking Distributed Software Systems | Rupak Majumdar | 31m |
An implementation-level model checker called Must embeds a small message-passing DSL in Rust and exhaustively explores nonisomorphic execution graphs with… | ||
| Optimal Quantum Programs | Jens Palsberg | 32m |
Three notions of optimality are compared: reliability (gate error rates ~single‑qubit 99.99%, two‑qubit ~99.9%), depth (mapping to hardware is NP‑complete and… | ||
| Reasoning About Hilbert’s Choice Operator in SMT | Byron Cook | 32m |
Proposes adding Hilbert ε-terms to SMT by translating quantifiers to choice terms, then replacing those with fresh logical constants (e.g. introduce L1 and L2)… | ||
| Find, Use, and Conserve Tools for Formal Methods | Dirk Beyer | 34m |
Central repository collects YAML metadata for 91 formal-methods tools (59 C verifiers from the last competition), records exact versions with Zenodo DOI… | ||
| Abstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…) | Thomas Ball | 34m |
A retrospective of SLAM’s engineering and theory: a C-to-Boolean pipeline that under-approximates correlations (SLAM’s actual abstraction is Cartesian… | ||
| nothing matches | ||