Bernhard Kragl
Description: A verifier for concurrent programs
Civl is a verifier for concurrent programs following two core design principles.
Layered Refinement (instead of monolithic proofs): Programs are verified across multiple layers of stacked refinements. Each refinement layer corresponds to a simplifying program transformation. Proof construction becomes more productive by decomposing the problem into small, manageable, and automatable pieces. The resulting proofs become simpler and easier to reuse.
Structured Programs (instead of transition systems): Each layer of abstraction (from low-level implementations to high-level specifications) is represented in the same language of structured programs. This naturally bridges the verification gap down to implementations and enables the utilization of program structure in proofs. All layers (and their connection) are compactly expressed together as a single syntactic unit in a layered concurrent program .
Bernhard Kragl