Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057431" target="_blank" >RIV/00216224:14330/12:00057431 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-642-32469-7_14" target="_blank" >http://dx.doi.org/10.1007/978-3-642-32469-7_14</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-32469-7_14" target="_blank" >10.1007/978-3-642-32469-7_14</a>
Alternative languages
Result language
angličtina
Original language name
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution
Original language description
We introduce a novel technique for checking properties described by finite state machines. The technique is based on a synergy of three well-known methods: instrumentation, program slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various properties. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program to find real violations of the checked properties, i.e. real bugs. Depending on the kind of symbolic execution, the technique can be applied as a stand-alone bug finding technique, or to weed out some false positives from an output of another bug-finding tool. We provide several examples demonstrating the practical applicability of our technique.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Formal Methods for Industrial Critical systems: 17th International Workshop, FMICS 2012
ISBN
9783642324680
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
207-221
Publisher name
Springer
Place of publication
Berlin, Heidelberg
Event location
Paris, France
Event date
Jan 1, 2012
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—