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

Other

Other22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013
CountryFrance
CityNancy
Period9/16/139/19/13

Fingerprint

Abstract Machines
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 (abstract). In Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings (Vol. 8123 LNAI, 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

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

Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings. Vol. 8123 LNAI 2013. p. 1-4 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8123 LNAI).

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

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. vol. 8123 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8123 LNAI, pp. 1-4, 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013, Nancy, France, 9/16/13. https://doi.org/10.1007/978-3-642-40537-2_1
Barrett C, Demri S, Deters M. Witness runs for counter machines (abstract). In Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings. Vol. 8123 LNAI. 2013. p. 1-4. (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-40537-2_1
Barrett, Clark ; Demri, Stéphane ; Deters, Morgan. / Witness runs for counter machines (abstract). Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings. Vol. 8123 LNAI 2013. pp. 1-4 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5807a78e064046e98389bc6022f16b5e,
title = "Witness runs for counter machines (abstract)",
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.",
author = "Clark Barrett and St{\'e}phane Demri and Morgan Deters",
year = "2013",
doi = "10.1007/978-3-642-40537-2_1",
language = "English (US)",
isbn = "9783642405365",
volume = "8123 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "1--4",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings",

}

TY - GEN

T1 - Witness runs for counter machines (abstract)

AU - Barrett, Clark

AU - Demri, Stéphane

AU - Deters, Morgan

PY - 2013

Y1 - 2013

N2 - 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 - 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=84885698045&partnerID=8YFLogxK

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

U2 - 10.1007/978-3-642-40537-2_1

DO - 10.1007/978-3-642-40537-2_1

M3 - Conference contribution

SN - 9783642405365

VL - 8123 LNAI

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

SP - 1

EP - 4

BT - Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings

ER -