CPAchecker

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 29 articles , 2 standard articles )

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

1 2 next

  1. 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)
  2. Karpenkov, Egor George; Monniaux, David; Wendler, Philipp: Program analysis with local policy iteration (2016)
  3. Koskinen, Eric; Yang, Junfeng: Reducing crash recoverability to reachability (2016)
  4. Leroux, Jér^ome; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
  5. Mordan, Vitaly; Mutilin, Vadim: Checking several requirements at once by CEGAR (2016)
  6. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  7. 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)
  8. Khoroshilov, Alexey; Mutilin, Vadim; Novikov, Evgeny; Zakharov, Ilja: Modeling environment for static verification of Linux kernel modules (2015)
  9. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  10. Zakharov, I.S.; Mutilin, V.S.; Khoroshilov, A.V.: Pattern-based environment modeling for static verification of Linux kernel modules (2015) ioport
  11. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  12. Löwe, Stefan; Mandrykin, Mikhail; Wendler, Philipp: Cpachecker with sequential combination of explicit-value analyses and predicate analyses. (Competition contribution) (2014) ioport
  13. Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013)
  14. Botinčan, Matko; Babić, Domagoj: Sigma$^*$, symbolic learning of input-output specifications (2013)
  15. Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: The mathsat5 SMT solver (2013)
  16. Löwe, Stefan: Cpachecker with explicit-value analysis based on CEGAR and interpolation. (Competition contribution) (2013)
  17. Popeea, Corneliu; Rybalchenko, Andrey: Threader: a verifier for multi-threaded programs. (Competition contribution) (2013)
  18. Wendler, Philipp: Cpachecker with sequential combination of explicit-state analysis and predicate analysis. (Competition contribution) (2013)
  19. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: From under-approximations to over-approximations and back (2012)
  20. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco: Software model checking with explicit scheduler and symbolic threads (2012)

1 2 next