Witness runs for counter machines

Clark Barrett, Stéphane Demri, Morgan Deters

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

Abstract

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
Pages120-150
Number of pages31
DOIs
StatePublished - Nov 6 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

Other

Other9th International Symposium on Frontiers of Combining Systems, FroCoS 2013
CountryFrance
CityNancy
Period9/18/139/20/13

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Barrett, C., Demri, S., & Deters, M. (2013). Witness runs for counter machines. In Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings (pp. 120-150). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8152 LNAI). https://doi.org/10.1007/978-3-642-40885-4_9