Fri 20 Jan 2023 17:10 - 17:35 at Square - Relational & Automated Verification Chair(s): Christoph Matheja

The development of constraint solvers simplified automated reasoning about programs and shifted the engineering burden to implementing symbolic compilation tools that translate programs into efficiently solvable constraints. We describe Grisette, a reusable symbolic evaluation framework for implementing domain-specific symbolic compilers. Grisette evaluates all execution paths and merges their states into a normal form that avoids making guards mutually exclusive. This ordered-guards representation reduces the constraint size 5-fold and the solving time more than 2-fold. Grisette is designed entirely as a library, which sidesteps the complications of lifting the host language into the symbolic domain. Grisette is purely functional, enabling memoization of symbolic compilation as well as monadic integration with host libraries. Grisette is statically typed, which allows catching programming errors at compile time rather than delaying their detection to the constraint solver. We implemented Grisette in Haskell and evaluated it on benchmarks that stress both the symbolic evaluation and constraint solving.

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:45 - 18:00
Relational & Automated VerificationPOPL at Square
Chair(s): Christoph Matheja DTU
16:45
25m
Talk
An Algebra of Alignment for Relational Verification
POPL
Timos Antonopoulos Yale University, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Ramana Nagasamudram Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Minh Ngo Stevens Institute of Technology
DOI
17:10
25m
Talk
Grisette: Symbolic Compilation as a Functional Programming Library
POPL
Sirui Lu University of Washington, Rastislav Bodík Google Research
DOI
17:35
25m
Talk
HFL(Z) Validity Checking for Automated Program Verification
POPL
Naoki Kobayashi University of Tokyo, Kento Tanahashi University of Tokyo, Ryosuke Sato University of Tokyo, Takeshi Tsukada Chiba University
DOI