Cited in
(55)- Model checking boot code from AWS data centers
- Horn clauses as an intermediate representation for program analysis and transformation
- Predicate abstraction for program verification
- The MathSAT5 SMT solver
- Efficient strategies for CEGAR-based model checking
- Block-wise abstract interpretation by combining abstract domains with SMT
- Leveraging compiler intermediate representation for multi- and cross-language verification
- Loop Invariants from Counterexamples
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Learning inductive invariants by sampling from frequency distributions
- Automated discovery of simulation between programs
- BLAST
- SLAM
- FunFrog
- CPAchecker
- Predator
- SMTInterpol
- Ultimate Automizer
- Deciding local theory extensions via E-matching
- Interproc
- Cleaneling
- LLBMC
- NuSMV3
- eVolCheck
- BULL
- ESBMC
- Threader
- LTSA-WS
- CSIsat
- SatAbs
- PAGAI
- PIC2LNT
- IKOS
- Wolverine
- TOrPEDO : witnessing model correctness with topological proofs
- Tools and algorithms for the construction and analysis of systems. 19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings
- c2i
- Coverity
- BOXES
- PKind
- DyTa
- CTIGAR
- GRASShopper
- H-PILoT
- SMACK
- Ultimate
- Klocwork
- Ultimate Taipan
- Cascade
- CoVEGI
- SMT-based model checking for recursive programs
- TOrPEDO
- Exploiting partial variable assignment in interpolation-based model checking
- A unifying view on SMT-based software verification
- Integrating topological proofs with model checking to instrument iterative design
This page was built for software: UFO
