Detail výsledku

Automated formal analysis and verification: an overview

VOJNAR, T.; KŘENA, B. Automated formal analysis and verification: an overview. INTERNATIONAL JOURNAL OF GENERAL SYSTEMS, 2013, vol. 2013, no. 42, p. 335-365. ISSN: 0308-1079.
Typ
článek v časopise
Jazyk
anglicky
Autoři
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Křena Bohuslav, Ing., Ph.D., UITS (FIT)
Abstrakt

This paper provides an overview of various existing approaches to automated formal analysis and verification. The most space is devoted to the approach of model checking, including its basic principles as well as the different techniques that have been proposed for dealing with the state space explosion problem in model checking. This paper, however, includes a brief discussion of theorem proving and static analysis too. All of the discussed approaches are introduced mostly on an informal level, with an attempt to provide the reader with their basic ideas and references to works where more details can be found.

Klíčová slova

formal analysis and verification; model checking; state space explosion; theorem proving; static analysis

URL
Rok
2013
Strany
335–365
Časopis
INTERNATIONAL JOURNAL OF GENERAL SYSTEMS, roč. 2013, č. 42, ISSN 0308-1079
DOI
10.1080/03081079.2012.757437
BibTeX 
@article{BUT103472,
  author="Tomáš {Vojnar} and Bohuslav {Křena}",
  title="Automated formal analysis and verification: an overview",
  journal="INTERNATIONAL JOURNAL OF GENERAL SYSTEMS",
  year="2013",
  volume="2013",
  number="42",
  pages="335--365",
  doi="10.1080/03081079.2012.757437",
  issn="0308-1079",
  url="http://www.tandfonline.com/eprint/jVBdnCqNINZHmymMCrpj/full"
}
Projekty
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, zahájení: 2010-01-01, ukončení: 2012-12-31, řešení
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, zahájení: 2012-01-01, ukončení: 2014-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru