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

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

1 2 next

  1. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  2. 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)
  3. Karpenkov, Egor George; Monniaux, David; Wendler, Philipp: Program analysis with local policy iteration (2016)
  4. Koskinen, Eric; Yang, Junfeng: Reducing crash recoverability to reachability (2016)
  5. Leroux, Jér^ome; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
  6. Mordan, Vitaly; Mutilin, Vadim: Checking several requirements at once by CEGAR (2016)
  7. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  8. 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)
  9. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  10. Khoroshilov, Alexey; Mutilin, Vadim; Novikov, Evgeny; Zakharov, Ilja: Modeling environment for static verification of Linux kernel modules (2015)
  11. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  12. Zakharov, I. S.; Mutilin, V. S.; Khoroshilov, A. V.: Pattern-based environment modeling for static verification of Linux kernel modules (2015) ioport
  13. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  14. Löwe, Stefan; Mandrykin, Mikhail; Wendler, Philipp: Cpachecker with sequential combination of explicit-value analyses and predicate analyses. (Competition contribution) (2014) ioport
  15. Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013) ioport
  16. Botinčan, Matko; Babić, Domagoj: Sigma$^*$, symbolic learning of input-output specifications (2013)
  17. Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto: The MathSAT5 SMT solver (2013)
  18. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)
  19. Löwe, Stefan: Cpachecker with explicit-value analysis based on CEGAR and interpolation. (Competition contribution) (2013) ioport
  20. Novikov, E. M.: An approach to implementation of aspect-oriented programming for C (2013) ioport

1 2 next