Witness Runs for Counter Machines

Witness Runs for Counter Machines” by Clark Barrett, Stephané Demri, and Morgan Deters. In Proceedings of the 9^th International Symposium on Frontiers of Combining Systems (FroCoS '13), (Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, eds.), Sep. 2013, pp. 120-150. Nancy, France.


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 solers.

BibTeX entry:

   author = {Clark Barrett and Stephan{\'e} Demri and Morgan Deters},
   editor = {Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt},
   title = {Witness Runs for Counter Machines},
   booktitle = {Proceedings of the {\it 9^{th}} International Symposium on
	Frontiers of Combining Systems (FroCoS '13)},
   series = {Lecture Notes in Artificial Intelligence},
   volume = {8152},
   pages = {120-150},
   publisher = {Springer Berlin Heidelberg},
   month = sep,
   year = {2013},
   isbn = {978-3-642-40884-7},
   note = {Nancy, France},
   url = {http://www.cs.nyu.edu/~barrett/pubs/BDD13.pdf}

(This webpage was created with bibtex2web.)