TY - GEN
T1 - Witness runs for counter machines
AU - Barrett, Clark
AU - Demri, Stéphane
AU - Deters, Morgan
N1 - Funding Information:
Work partially supported by the EU Seventh Framework Programme under grant agreement No. PIOF-GA-2011-301166 (DATAVERIF).
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84886777819&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84886777819&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40885-4_9
DO - 10.1007/978-3-642-40885-4_9
M3 - Conference contribution
AN - SCOPUS:84886777819
SN - 9783642408847
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 120
EP - 150
BT - Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings
T2 - 9th International Symposium on Frontiers of Combining Systems, FroCoS 2013
Y2 - 18 September 2013 through 20 September 2013
ER -