Cited in
(only showing first 100 items - show all)- Symbolic memory with pointers
- Connecting program synthesis and reachability: automatic program repair using test-input generation
- Symbolic execution formally explained
- Efficient strategies for CEGAR-based model checking
- Verifying Whiley programs with Boogie
- Constraint programming for dynamic symbolic execution of JavaScript
- Wombit: a portfolio bit-vector solver using word-level propagation
- Algorithm selection for dynamic symbolic execution: a preliminary study
- Symbolic computation via program transformation
- Scalable and precise refinement of cache timing analysis via path-sensitive verification
- Automated formal analysis and verification: an overview
- Efficient loop navigation for symbolic execution
- An introduction to test specification in FQL
- Combining model checking and testing
- Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning
- Beaver
- Boolector
- CUTE
- JMLUnit
- CalFuzzer
- WoLFram
- TVOC
- BLAST
- DiVinE
- MiBench
- SAT competition
- Valgrind
- ISP
- LLVM
- TASS_
- Bogor
- Limmat
- SPARKSkein
- ADL
- DART
- LTSmin
- Euclide
- PathCrawler
- Pex
- CPAchecker
- Predator
- TRACER
- UFO
- Java PathFinder
- MARMOT
- ConTest
- Cetus
- CBMC
- r-TuBound
- libalf
- ns-3
- BitBlaze
- Nighthawk
- SPARK Pro
- JPF-SE
- BAP
- FloPSy
- SatAbs
- YOGI
- Joogie
- Ctrl
- KLOVER
- Snugglebug
- FShell
- Smacc
- Wolverine
- CodeSonar
- Klockwork
- EXPLODE
- LCTD
- JST
- Looper
- Coverity
- VS3
- OTAWA
- CoVaC
- BoogiePL
- BotMiner
- Luck
- Norn
- Sigma*
- SMACK
- BIGNUM
- ANaConDA
- CATG
- KLEE-FP
- Jalangi
- Pixy
- Symbiotic 2
- CIL
- Angelix
- jCUTE
- Klocwork
- SymDIVINE
- BINSEC/SE
- LCT
- ExpoSE
- QEMU
- SymJS
This page was built for software: KLEE
