Verification of Gap-Order Constraint Abstractions of Counter Systems
From MaRDI portal
Publication:2891403
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
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
