Cpachecker with sequential combination of explicit-state analysis and predicate analysis. (Competition contribution). CPAchecker is an open-source framework for software verification, based on the concepts of configurable program analysis (CPA). We submit a CPAchecker configuration that uses a sequential combination of two approaches. It starts with an explicit-state analysis, and, if no answer can be found within some time, switches to a predicate analysis with adjustable-block encoding and CEGAR.

References in zbMATH (referenced in 46 articles , 2 standard articles )

Showing results 1 to 20 of 46.
Sorted by year (citations)

1 2 3 next

  1. Meseguer, José: Generalized rewrite theories, coherence completion, and symbolic methods (2020)
  2. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Yao, Chenguang: Translating Xd-C programs to MSVL programs (2020)
  3. Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Hongwei: A novel approach to verifying context free properties of programs (2020)
  4. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  5. Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)
  6. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  7. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  8. Chaves, Lennon; Bessa, Iury; Cordeiro, Lucas; Kroening, Daniel: DSValidator: an automated counterexample reproducibility tool for digital systems (2018)
  9. Hoenicke, Jochen; Schindler, Tanja: Efficient interpolation for the theory of arrays (2018)
  10. Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey: Predicate abstraction for program verification (2018)
  11. Lauko, Henrich; Ročkai, Petr; Barnat, Jiří: Symbolic computation via program transformation (2018)
  12. Greitschus, Marius; Dietsch, Daniel; Podelski, Andreas: Loop invariants from counterexamples (2017)
  13. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  14. Karpenkov, Egor George; Monniaux, David; Wendler, Philipp: Program analysis with local policy iteration (2016)
  15. Koskinen, Eric; Yang, Junfeng: Reducing crash recoverability to reachability (2016)
  16. Leroux, Jérôme; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
  17. Mordan, Vitaly; Mutilin, Vadim: Checking several requirements at once by CEGAR (2016)
  18. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  19. ter Beek, Maurice H.; Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints (2016)
  20. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)

1 2 3 next