Verification of Gap-Order Constraint Abstractions of Counter Systems

DOI10.1007/978-3-642-27940-9_7zbMath1325.68141OpenAlexW1872877151MaRDI QIDQ2891403

Laura Bozzelli, Sophie Pinchinat

Publication date: 15 June 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-27940-9_7

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items (3)

On the Termination of Integer Loops ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Ranking Functions for Linear-Constraint Loops

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A closed-form evaluation for Datalog queries with integer (gap)-order constraints
• An automata-theoretic approach to constraint LTL
• Verification of qualitative \(\mathbb Z\) constraints
• Approximated parameterized verification of infinite-state processes with global conditions
• Verification of gap-order constraint abstractions of counter systems
• Towards a Model-Checker for Counter Systems
• Iterating Octagons
• “Sometimes” and “not never” revisited
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints
• Programs with Lists Are Counter Automata
• Size-Change Termination, Monotonicity Constraints and Ranking Functions

This page was built for publication: Verification of Gap-Order Constraint Abstractions of Counter Systems