SmacC: A Retargetable Symbolic Execution Engine

Armin Biere; Jens Knoop; Laura Kovács; Jakob Zwirchmayr

SmacC: A Retargetable Symbolic Execution Engine

Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

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.

Original language	English
Title of host publication	Proc. 11th Intl. Symp. on Automated Technology for Verification and Analysis
Publisher	Springer
Pages	485-486
Number of pages	5
Volume	8172
Publication status	Published - 2013

Publication series

Name	Lecture Notes in Computer Science (LNCS)

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{83c14497c56a41378e8fa9b7e4ce47f0,

title = "SmacC: A Retargetable Symbolic Execution Engine",

abstract = "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.",

author = "Armin Biere and Jens Knoop and Laura Kov{\'a}cs and Jakob Zwirchmayr",

year = "2013",

language = "English",

volume = "8172",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "485--486",

booktitle = "Proc. 11th Intl. Symp. on Automated Technology for Verification and Analysis",

}

TY - GEN

T1 - SmacC: A Retargetable Symbolic Execution Engine

AU - Biere, Armin

AU - Knoop, Jens

AU - Kovács, Laura

AU - Zwirchmayr, Jakob

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

M3 - Conference proceedings

VL - 8172

T3 - Lecture Notes in Computer Science (LNCS)

SP - 485

EP - 486

BT - Proc. 11th Intl. Symp. on Automated Technology for Verification and Analysis

PB - Springer

ER -