The Q-compiler for verifying high-consequence controls

John Aytac - Sandia National Labs

The purpose of the Q compiler is to prove relatively complexproperties about relatively simple digital controls -- controls for high-consequence systems where correctness is critical to safety. Starting with a generalized state machine, called a statechart, and progressing through multiple refinements, the state machine transition relation is proven against implementation code. The implementation can take the form of either C, using ACSL and Frama-C, or VHDL/Verilog using SVA in a commercial prover (e.g. Jasper). Refinements, and refinement across language boundaries afford a number of advantages. It enables proofs for more complex properties, more scalably than would otherwise be possible. The presentation will include some theory and an example of the development process.

Download this presentation

About John Aytac

Jon Aytac is a senior staff member in the Sandia Formal Methods Group. He earned Bachelor’s degrees in Physics and Computer Science at UC Berkeley, worked at Apple for 5 years, then studied Quantum Computing at the Graduate Physics Program at Berkeley.