Abstraction refinement and antichains for trace inclusion of infinite state systems
From MaRDI portal
Publication:5919079
DOI10.1007/s10703-020-00345-1zbMath1506.68046arXiv1410.5056OpenAlexW2997994926MaRDI QIDQ5919079
Tomáš Vojnar, Lukáš Holík, Adam Rogalewicz, Radu Iosif
Publication date: 8 February 2021
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1410.5056
interpolationantichainsdata automatasimulation relationstrace inclusionCEGARgeneric register automata
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A theory of timed automata
- Symbolic model checking for real-time systems
- Finite-memory automata
- On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
- Abstraction refinement for emptiness checking of alternating data automata
- Checking NFA equivalence with bisimulations up to congruence
- Two-variable logic on data words
- Horn Clause Solvers for Program Verification
- Ordered Navigation on Multi-attributed Data Words
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- When Simulation Meets Antichains
- Automatic Verification of Integer Array Programs
- Lazy abstraction
- The MathSAT5 SMT Solver
- What Else Is Decidable about Integer Arrays?
- A Logic of Singly Indexed Arrays
- Antichains: A New Algorithm for Checking Universality of Finite Automata
- Lazy Abstraction with Interpolants
- Abstraction refinement and antichains for trace inclusion of infinite state systems
