SMT for state-based formal methods: the ASM case study
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F18%3A10374942" target="_blank" >RIV/00216208:11320/18:10374942 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.29007/djdz" target="_blank" >https://doi.org/10.29007/djdz</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.29007/djdz" target="_blank" >10.29007/djdz</a>
Alternative languages
Result language
angličtina
Original language name
SMT for state-based formal methods: the ASM case study
Original language description
State-based transition systems can take advantage of a symbolic representation of the concepts of state and transition in order to automatically solve verification questions that could not be otherwise tackled in terms of explicit representation of the transition system. We report here our experience in developing solutions, approaches and supporting tools of verification problems regarding the Abstract State Machines (ASMs), a transition system which can be considered as an extension of Finite State Machines. We present the symbolic representation of an ASM and of its computational model in terms of the Yices SMT solver. We also discuss two scenarios of verification questions regarding the ASMs for which the symbolic representation helped us to formalize and solve the problem by satisfiability checking, namely automatic proof of correct ASM refinement and runtime verification.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA17-12465S" target="_blank" >GA17-12465S: Verification and Bug Hunting for Advanced Software</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2018
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
Automated Formal Methods
ISBN
—
ISSN
2515-1762
e-ISSN
neuvedeno
Number of pages
18
Pages from-to
1-18
Publisher name
EasyChair
Place of publication
Neuveden
Event location
Moffett Field, CA, USA
Event date
May 19, 2017
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—