Witness runs for counter machines (abstract)

Clark Barrett, Stéphane Demri, Morgan Deters

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

Abstract

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 publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings
Pages1-4
Number of pages4
DOIs
StatePublished - Oct 22 2013
Event22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013 - Nancy, France
Duration: Sep 16 2013Sep 19 2013

Publication series

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

Other

Other22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013
CountryFrance
CityNancy
Period9/16/139/19/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 (abstract). In Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings (pp. 1-4). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8123 LNAI). https://doi.org/10.1007/978-3-642-40537-2_1