Detail publikace

Automata-Based Termination Proofs

ROGALEWICZ, A.; IOSIF, R. Automata-Based Termination Proofs. Computing and Informatics, 2013, vol. 2013, no. 4, p. 739-775. ISSN: 1335-9150.
Název česky
Dokazování konečnosti programů založené na automatech
Typ
článek v časopise
Jazyk
anglicky
Autoři
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Radu Iosif
URL
Klíčová slova

Formal verification, Termination, Buchi automata, Tree automata, Programs with pointers

Abstrakt

V tomto článku prezentujeme novou metodu pro dokazování konečnosti programů pracujících nad nekonečně stavovými datovými strukturami. Program je v této metodě simulován buchi automatem takovým, že každý nekonečný běh odpovídá nekonečnému slovu akceptovanému tímto automatem.

Rok
2013
Strany
739–775
Časopis
Computing and Informatics, roč. 2013, č. 4, ISSN 1335-9150
BibTeX 
@article{BUT103496,
  author="Adam {Rogalewicz} and Iosif {Radu}",
  title="Automata-Based Termination Proofs",
  journal="Computing and Informatics",
  year="2013",
  volume="2013",
  number="4",
  pages="739--775",
  issn="1335-9150",
  url="http://www.cai.sk/ojs/index.php/cai/article/view/1970"
}
Nahoru