Kragl, B., & Qadeer, S. (2021). The Civl Verifier. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 143–152). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Series:
Conference Series: Formal Methods in Computer-Aided Design
-
Published in:
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
-
Date (published):
Oct-2021
-
Number of Pages:
10
-
Publisher:
TU Wien Academic Press, Wien
-
Peer reviewed:
Yes
-
Keywords:
formal methods
en
formale Methode
de
Abstract:
Civl is a static verifier for concurrent programs
designed around the conceptual framework of layered refinement,
which views the task of verifying a program as a sequence of
program simplification steps each justified by its own invariant.
Civl verifies a layered concurrent program that compactly
expresses all the programs in this sequence and the supporting
invariants. This paper presents the design and implementation
of the Civl verifier.
CC BY 4.0
