TY - GEN
T1 - Witness runs for counter machines (abstract)
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). An extended version can be found in [BDD13].
PY - 2013
Y1 - 2013
N2 - 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 - 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=84885698045&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84885698045&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40537-2_1
DO - 10.1007/978-3-642-40537-2_1
M3 - Conference contribution
AN - SCOPUS:84885698045
SN - 9783642405365
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 4
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings
T2 - 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013
Y2 - 16 September 2013 through 19 September 2013
ER -