@inproceedings{10688,
  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.},
  author       = {Kragl, Bernhard and Qadeer, Shaz},
  booktitle    = {Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design},
  editor       = {Ruzica, Piskac and Whalen, Michael W.},
  isbn         = {978-3-85448-046-4},
  location     = {Virtual},
  pages        = {143–152},
  publisher    = {TU Wien Academic Press},
  title        = {{The Civl verifier}},
  doi          = {10.34727/2021/isbn.978-3-85448-046-4_23},
  volume       = {2},
  year         = {2021},
}