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
Volume8152 LNAI
DOIs
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Temporal logic
Surface mount technology
Decision Procedures
Temporal Logic
Reachability
Enumeration
Schema
Path
Class

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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 (Vol. 8152 LNAI, 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

Witness runs for counter machines. / Barrett, Clark; Demri, Stéphane; Deters, Morgan.

Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings. Vol. 8152 LNAI 2013. p. 120-150 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8152 LNAI).

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

Barrett, C, Demri, S & Deters, M 2013, Witness runs for counter machines. in Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings. vol. 8152 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8152 LNAI, pp. 120-150, 9th International Symposium on Frontiers of Combining Systems, FroCoS 2013, Nancy, France, 9/18/13. https://doi.org/10.1007/978-3-642-40885-4_9
Barrett C, Demri S, Deters M. Witness runs for counter machines. In Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings. Vol. 8152 LNAI. 2013. p. 120-150. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-40885-4_9
Barrett, Clark ; Demri, Stéphane ; Deters, Morgan. / Witness runs for counter machines. Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings. Vol. 8152 LNAI 2013. pp. 120-150 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{d60b72f7ed504cdc9f4cff75bce74c30,
title = "Witness runs for counter machines",
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.",
author = "Clark Barrett and St{\'e}phane Demri and Morgan Deters",
year = "2013",
doi = "10.1007/978-3-642-40885-4_9",
language = "English (US)",
isbn = "9783642408847",
volume = "8152 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "120--150",
booktitle = "Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings",

}

TY - GEN

T1 - Witness runs for counter machines

AU - Barrett, Clark

AU - Demri, Stéphane

AU - Deters, Morgan

PY - 2013

Y1 - 2013

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

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

UR - http://www.scopus.com/inward/record.url?scp=84886777819&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84886777819&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-40885-4_9

DO - 10.1007/978-3-642-40885-4_9

M3 - Conference contribution

SN - 9783642408847

VL - 8152 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 120

EP - 150

BT - Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings

ER -