SMT-based verification of data-aware processes: a model-theoretic approach
From MaRDI portal
Publication:5139282
DOI10.1017/S0960129520000067zbMath1495.68129OpenAlexW3014139035MaRDI QIDQ5139282
Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Andrey Rivkin, Marco Montali
Publication date: 8 December 2020
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129520000067
database theorysatisfiability modulo theoriesmodel completenesswell-quasi-ordersverification of data-aware processes
Database theory (68P15) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Applications of model theory (03C98)
Related Items
Aligning event logs to resource-constrained \(\nu \)-Petri nets ⋮ SMT-based generation of symbolic automata ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Model completeness, covers and superposition ⋮ Combination of uniform interpolants via Beth definability ⋮ Combined covers and Beth definability ⋮ Object-Centric Replay-Based Conformance Checking: Unveiling Desire Lines and Local Deviations
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- An extension of lazy abstraction with interpolation for programs with arrays
- Decidability and complexity of Petri nets with unordered data
- Model-theoretic methods in combined constraint satisfiability
- Model theory.
- Model-companions and definability in existentially complete structures
- Interpolation, amalgamation and combination (the non-disjoint signatures case)
- Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
- Formal specification and verification of dynamic parametrized architectures
- From model completeness to verification of data aware processes
- Model completeness, covers and superposition
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- Introduction to model theory and to the metamathematics of algebra
- Modularity results for interpolation, amalgamation and superamalgamation
- On the metamathematics of algebra
- On Interpolation and Symbol Elimination in Theory Extensions
- The Power of Well-Structured Systems
- Generalized Property Directed Reachability
- Lazy Abstraction with Interpolants for Arrays
- SAT-Based Model Checking without Unrolling
- Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
- Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator
- Booster: An Acceleration-Based Verification Framework for Array Programs
- Towards SMT Model Checking of Array-Based Systems
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Interpolation in local theory extensions
- Data Structures with Arithmetic Constraints: A Non-disjoint Combination
- Probabilities on finite models
- Monadic second order logic as the model companion of temporal logic
- Term Rewriting and All That
- Frontiers of Combining Systems
- Universal graphs and universal functions
- Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
- A MODEL-THEORETIC CHARACTERIZATION OF MONADIC SECOND ORDER LOGIC ON INFINITE WORDS
- MCMT: A Model Checker Modulo Theories
- Lazy Abstraction with Interpolants
- Ordering by Divisibility in Abstract Algebras
