Software Verification with PDR: An Implementation of the State of the Art
19
5.1 Data Availability Statement
A replication package for this article including all evaluated implementations
and BenchExec is available at Zenodo [9]. Current versions of CPAchecker
are available at https://github.com/sosy-lab/cpachecker. The benchmark
set of SV-COMP 2018 used in Sect. 4 is available online at https://github.
com/sosy-lab/sv-benchmarks/releases/tag/svcomp18 and the dataset from
SV-COMP 2019 [4] that we analyzed is available at https://sv-comp.sosy-lab.
org/2019/results/results-verified/All-Raw.zip.
References
1. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model
checking C programs. In: Proc. TACAS. pp. 268–283. LNCS 2031, Springer (2001).
https://doi.org/10.1007/3-540-45319-9_19
2. Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL. pp. 1–3. ACM (2002).
https://doi.org/10.1145/503272.503274
3. Beckert, B., Hähnle, R.: Reasoning and verification: State of the art
and current trends. IEEE Intelligent Systems 29(1), 20–29 (2014).
https://doi.org/10.1109/MIS.2014.3
4. Beyer, D.: Automatic verification of C and Java programs: SV-COMP
2019. In: Proc. TACAS (3). pp. 133–155. LNCS 11429, Springer (2019).
https://doi.org/10.1007/978-3-030-17502-3_9
5. Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuouslyrefined invariants. In: Proc. CAV. pp. 622–640. LNCS 9206, Springer (2015).
https://doi.org/10.1007/978-3-319-21690-4_42
6. Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reasoning 60(3), 299–335 (2018). https://doi.org/10.1007/s10817017-9432-6
7. Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184–190. LNCS 6806, Springer (2011).
https://doi.org/10.1007/978-3-642-22110-1_16
8. Beyer, D., Dangl, M.: Software verification with PDR: Implementation and empirical
evaluation of the state of the art (August 2019), http://arxiv.org/abs/1908.
06271
9. Beyer, D., Dangl, M.: Replication package for article ‘Software verification
with PDR: An implementation of the state of the art’. Zenodo (2020).
https://doi.org/10.5281/zenodo.3678766
10. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS. pp. 193–207. LNCS 1579, Springer (1999).
https://doi.org/10.1007/3-540-49059-0_14
11. Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to inductionguided abstraction-refinement (CTIGAR). In: Proc. CAV. pp. 831–848. LNCS 8559,
Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_55
12. Bradley, A.R.: SAT-based model checking without unrolling. In: Proc. VMCAI. pp.
70–87. LNCS 6538, Springer (2011). https://doi.org/10.1007/978-3-642-18275-4_7
13. Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation.
Formal Asp. Comput. 20(4-5), 379–405 (2008). https://doi.org/10.1007/s00165008-0080-9
19
5.1 Data Availability Statement
A replication package for this article including all evaluated implementations
and BenchExec is available at Zenodo [9]. Current versions of CPAchecker
are available at https://github.com/sosy-lab/cpachecker. The benchmark
set of SV-COMP 2018 used in Sect. 4 is available online at https://github.
com/sosy-lab/sv-benchmarks/releases/tag/svcomp18 and the dataset from
SV-COMP 2019 [4] that we analyzed is available at https://sv-comp.sosy-lab.
org/2019/results/results-verified/All-Raw.zip.
References
1. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model
checking C programs. In: Proc. TACAS. pp. 268–283. LNCS 2031, Springer (2001).
https://doi.org/10.1007/3-540-45319-9_19
2. Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL. pp. 1–3. ACM (2002).
https://doi.org/10.1145/503272.503274
3. Beckert, B., Hähnle, R.: Reasoning and verification: State of the art
and current trends. IEEE Intelligent Systems 29(1), 20–29 (2014).
https://doi.org/10.1109/MIS.2014.3
4. Beyer, D.: Automatic verification of C and Java programs: SV-COMP
2019. In: Proc. TACAS (3). pp. 133–155. LNCS 11429, Springer (2019).
https://doi.org/10.1007/978-3-030-17502-3_9
5. Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuouslyrefined invariants. In: Proc. CAV. pp. 622–640. LNCS 9206, Springer (2015).
https://doi.org/10.1007/978-3-319-21690-4_42
6. Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reasoning 60(3), 299–335 (2018). https://doi.org/10.1007/s10817017-9432-6
7. Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184–190. LNCS 6806, Springer (2011).
https://doi.org/10.1007/978-3-642-22110-1_16
8. Beyer, D., Dangl, M.: Software verification with PDR: Implementation and empirical
evaluation of the state of the art (August 2019), http://arxiv.org/abs/1908.
06271
9. Beyer, D., Dangl, M.: Replication package for article ‘Software verification
with PDR: An implementation of the state of the art’. Zenodo (2020).
https://doi.org/10.5281/zenodo.3678766
10. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS. pp. 193–207. LNCS 1579, Springer (1999).
https://doi.org/10.1007/3-540-49059-0_14
11. Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to inductionguided abstraction-refinement (CTIGAR). In: Proc. CAV. pp. 831–848. LNCS 8559,
Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_55
12. Bradley, A.R.: SAT-based model checking without unrolling. In: Proc. VMCAI. pp.
70–87. LNCS 6538, Springer (2011). https://doi.org/10.1007/978-3-642-18275-4_7
13. Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation.
Formal Asp. Comput. 20(4-5), 379–405 (2008). https://doi.org/10.1007/s00165008-0080-9