Witness runs for counter machines

Clark Barrett, Stéphane Demri, Morgan Deters

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationFrontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings
Number of pages31
StatePublished - 2013
Event9th International Symposium on Frontiers of Combining Systems, FroCoS 2013 - Nancy, France
Duration: Sep 18 2013Sep 20 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8152 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other9th International Symposium on Frontiers of Combining Systems, FroCoS 2013

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Witness runs for counter machines'. Together they form a unique fingerprint.

Cite this