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
-
Reihe:
Conference Series: Formal Methods in Computer-Aided Design
-
Erschienen in:
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
-
Datum (veröffentlicht):
Okt-2021
-
Umfang:
10
-
Verlag:
TU Wien Academic Press, Wien
-
Peer Reviewed:
Ja
-
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.
en
Zugehörige Publikationen und Daten in reposiTUm: beinhaltet:
CC BY 4.0
