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.
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution (2017)
- Biere, Armin; Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Smacc: a retargetable symbolic execution engine (2013)