CPAchecker
swMATH ID: | 7408 |
Software Authors: | Beyer, Dirk; Löwe, Stefan; Wendler, Philipp |
Description: | 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. |
Homepage: | http://cpachecker.sosy-lab.org/ |
Related Software: | BLAST; z3; CBMC; SLAM; UFO; KLEE; SatAbs; SeaHorn; NuSMV; SMTInterpol; SPIN; LLVM; Wolverine; Isabelle/HOL; LLBMC; SMACK; Threader; Predator; MathSAT5; GitHub |
Cited in: | 53 Documents |
Standard Articles
2 Publications describing the Software | Year |
---|---|
Cpachecker with sequential combination of explicit-value analyses and predicate analyses. (Competition contribution) Löwe, Stefan; Mandrykin, Mikhail; Wendler, Philipp |
2014
|
Cpachecker with sequential combination of explicit-state analysis and predicate analysis. (Competition contribution) Wendler, Philipp |
2013
|
all
top 5
Cited by 142 Authors
all
top 5
Cited in 12 Serials
all
top 5