Verification of Gap-Order Constraint Abstractions of Counter Systems
From MaRDI portal
Publication:2891403
DOI10.1007/978-3-642-27940-9_7zbMath1325.68141MaRDI 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
68Q45: Formal languages and automata
68Q60: Specification and verification (program logics, model checking, etc.)
68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
03B44: Temporal logic
Related Items
Ranking Functions for Linear-Constraint Loops, Computable fixpoints in well-structured symbolic model checking, On the Termination of Integer 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
