swMATH9570MaRDI QIDQ21551FDOQ21551
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/978-3-642-31424-7_48
Cited In (53)
- Efficient strategies for CEGAR-based model checking
- 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
- Exploiting partial variable assignment in interpolation-based model checking
- Block-wise abstract interpretation by combining abstract domains with SMT
- Predicate abstraction for program verification
- FunFrog
- CPAchecker
- Predator
- SMTInterpol
- Ultimate Automizer
- Interproc
- Cleaneling
- LLBMC
- NuSMV3
- eVolCheck
- BULL
- ESBMC
- Threader
- LTSA-WS
- CSIsat
- SatAbs
- PAGAI
- PIC2LNT
- IKOS
- Wolverine
- Deciding local theory extensions via E-matching
- c2i
- Coverity
- BOXES
- PKind
- DyTa
- CTIGAR
- GRASShopper
- H-PILoT
- SMACK
- Ultimate
- Klocwork
- Ultimate Taipan
- Cascade
- Model checking boot code from AWS data centers
- Automatically proving termination and memory safety for programs with pointer arithmetic
- CoVEGI
- Integrating topological proofs with model checking to instrument iterative design
- Learning inductive invariants by sampling from frequency distributions
- Leveraging compiler intermediate representation for multi- and cross-language verification
- TOrPEDO
- Automated discovery of simulation between programs
- A unifying view on SMT-based software verification
- The MathSAT5 SMT solver
- TOrPEDO : witnessing model correctness with topological proofs
- SMT-based model checking for recursive programs
- Horn clauses as an intermediate representation for program analysis and transformation
- Loop Invariants from Counterexamples
This page was built for software: UFO
