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 27 articles , 1 standard article )

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

1 2 next

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

1 2 next