×

Smacc

swMATH ID: 14305
Software Authors: Biere, Armin; Knoop, Jens; Kov'acs, Laura; Zwirchmayr, Jakob
Description: Smacc: a retargetable symbolic execution engine. SmacC is a symbolic execution engine for C programs. It can be used for program verification, bounded model checking and generating SMT benchmarks. More recently we also successfully applied SmacC for high-level timing analysis of programs to infer exact loop bounds and safe over-approximations. SmacC uses the logic for bit-vectors with arrays to construct a bit-precise memory-model of a program for path-wise exploration.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-319-02444-8_40
Related Software: r-TuBound; STP; OTAWA; Stony Brook; KLEE; LLVM; lp_solve; Boolector
Cited in: 1 Publication

Standard Articles

1 Publication describing the Software Year
Smacc: a retargetable symbolic execution engine
Biere, Armin; Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob
2013

Citations by Year