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 1 article , 1 standard article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Biere, Armin; Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Smacc: a retargetable symbolic execution engine (2013)