SMT-based verification of data-aware processes: a model-theoretic approach
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3829877 (Why is no real title available?)
- scientific article; zbMATH DE number 1424027 (Why is no real title available?)
- scientific article; zbMATH DE number 5194318 (Why is no real title available?)
- A model-theoretic characterization of monadic second order logic on infinite words
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- An extension of lazy abstraction with interpolation for programs with arrays
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Booster: an acceleration-based verification framework for array programs
- Combining satisfiability procedures for unions of theories with a shared counting operator
- Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
- Data structures with arithmetic constraints: A non-disjoint combination
- Decidability and complexity of Petri nets with unordered data
- Formal specification and verification of dynamic parametrized architectures
- From model completeness to verification of data aware processes
- Frontiers of Combining Systems
- Generalized property directed reachability
- Interpolation in local theory extensions
- Interpolation, amalgamation and combination (the non-disjoint signatures case)
- Introduction to model theory and to the metamathematics of algebra
- Lazy Abstraction with Interpolants
- Lazy abstraction with interpolants for arrays
- MCMT: a model checker modulo theories
- Model completeness, covers and superposition
- Model theory.
- Model-companions and definability in existentially complete structures
- Model-theoretic methods in combined constraint satisfiability
- Modularity results for interpolation, amalgamation and superamalgamation
- Monadic second order logic as the model companion of temporal logic
- Nets with tokens which carry data
- On the metamathematics of algebra
- Ordering by Divisibility in Abstract Algebras
- Paramodulation-based theorem proving
- Probabilities on finite models
- SAT-Based Model Checking without Unrolling
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Term Rewriting and All That
- The power of well-structured systems
- Towards SMT Model Checking of Array-Based Systems
- Universal graphs and universal functions
- Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
- Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
Cited in
(11)- Object-Centric Replay-Based Conformance Checking: Unveiling Desire Lines and Local Deviations
- Database Theory - ICDT 2005
- Combined covers and Beth definability
- MCMT: a model checker modulo theories
- Aligning event logs to resource-constrained \(\nu \)-Petri nets
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- From model completeness to verification of data aware processes
- Model completeness, covers and superposition
- SMT-based generation of symbolic automata
- Exact and approximated log alignments for processes with inter-case dependencies
- Combination of uniform interpolants via Beth definability
This page was built for publication: SMT-based verification of data-aware processes: a model-theoretic approach
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5139282)
