The Civl verifier Conference Series Kragl, Bernhard ; https://orcid.org/0000-0001-7745-9117 Qadeer, Shaz Ruzica, Piskac Whalen, Michael W. ddc:000 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. TU Wien Academic Press 2021 info:eu-repo/semantics/conferenceObject doc-type:conferenceObject text http://purl.org/coar/resource_type/c_5794 https://research-explorer.ista.ac.at/record/10688 https://research-explorer.ista.ac.at/download/10688/10689 Kragl B, Qadeer S. The Civl verifier. In: Ruzica P, Whalen MW, eds. <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design</i>. Vol 2. TU Wien Academic Press; 2021:143–152. doi:<a href="https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23">10.34727/2021/isbn.978-3-85448-046-4_23</a> eng info:eu-repo/semantics/altIdentifier/doi/10.34727/2021/isbn.978-3-85448-046-4_23 info:eu-repo/semantics/altIdentifier/isbn/978-3-85448-046-4 info:eu-repo/semantics/openAccess