×

zbMATH — the first resource for mathematics

Witness runs for counter machines. (English) Zbl 1397.68122
Fontaine, Pascal (ed.) et al., Frontiers of combining systems. 9th international symposium, FroCoS 2013, Nancy, France, September 18–20, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40884-7/pbk). Lecture Notes in Computer Science 8152. Lecture Notes in Artificial Intelligence, 120-150 (2013).
Summary: In this paper, we present recent results about the verification of counter machines by using decision procedures for Presburger arithmetic. We recall several known classes of counter machines for which the reachability sets are Presburger-definable as well as temporal logics with arithmetical constraints. We discuss issues related to flat counter machines, path schema enumeration, and the use of SMT solvers.
For the entire collection see [Zbl 1272.68019].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
03F30 First-order arithmetic and fragments
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
z3; TaPAS; SMT-LIB; CVC4
PDF BibTeX XML Cite
Full Text: DOI