Cited in
(only showing first 100 items - show all)- Finding and fixing faults
- Loop summarization using state and transition invariants
- Abstract semantic diffing of evolving concurrent programs
- Transfer function synthesis without quantifier elimination
- Compositional sequentialization of periodic programs
- Efficient SAT-based bounded model checking for software verification
- Verifying Whiley programs with Boogie
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
- Not all bugs are created equal, but robust reachability can tell the difference
- Quantifying software reliability via model-counting
- Verified cryptographic code for everybody
- Translating Xd-C programs to MSVL programs
- Loop Summarization Using Abstract Transformers
- A taxonomy of exact methods for partial Max-SAT
- SATenstein: automatically building local search SAT solvers from components
- Exploiting binary floating-point representations for constraint propagation
- Tools and Algorithms for the Construction and Analysis of Systems
- Symbolic computation via program transformation
- An automatic method for the dynamic construction of abstractions of states of a formal model
- Shape neutral analysis of graph-based data-structures
- Information theory and security: Quantitative information flow
- Scalable and precise refinement of cache timing analysis via path-sensitive verification
- On black-box optimization in divide-and-conquer SAT solving
- Fairness modulo theory: a new approach to LTL software model checking
- Matching multiplications in bit-vector formulas
- Symbolic predictive analysis for concurrent programs
- An extension of lazy abstraction with interpolation for programs with arrays
- Deciding floating-point logic with abstract conflict driven clause learning
- A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
- Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
- Verification by gambling on program slices
- Sequentialization using timestamps
- Transfer of model checking to industrial practice
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- CPBPV
- CUTE
- MPI-CHECK
- APS-1
- FocusCheck
- Zing
- SatEx
- DiVer
- veriSoft
- PSATO
- BLAST
- HOL/SPIN
- SLAM
- NuSMV
- RuleBasePE
- QingTing1
- SAT competition
- Valgrind
- ARMC
- KLEE
- LLVM
- Dagger
- SCRATCH
- Bogor
- Limmat
- bv2epr
- SPARKSkein
- DART
- GATeL
- PathCrawler
- Cseq
- CPAchecker
- Predator
- SMTInterpol
- Ultimate Automizer
- visualSTATE
- UFO
- Bandera
- Java PathFinder
- TACO
- SystemC
- CESAR
- Bebop
- Gauss
- APS
- RunLim
- HECTOR
- SPEED
- Velodrome
- SMCHR
- Jerusat
- LLBMC
- AutoMOTGen
- Rhapsody
- eVolCheck
- Checkfence
- ESBMC
- URBiVA
- YASM
- SingleTrack
- SCOOT
- MOPS
- JFLAP
- Threader
- UMM
- SIMGRID
This page was built for software: CBMC
