Cited in
(42)- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Generalized rewrite theories, coherence completion, and symbolic methods
- Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
- SMT-based verification of data-aware processes: a model-theoretic approach
- Decision procedures for flat array properties
- A new acceleration-based combination framework for array properties
- An extension of lazy abstraction with interpolation for programs with arrays
- Search-space partitioning for parallelizing SMT solvers
- Parameterized model checking on the TSO weak memory model
- Combined covers and Beth definability
- RBAC-PAT
- TLA
- ASASP
- PlusCal
- Memorax
- InvA
- FunArray
- Cubicle
- EUREKA
- ByMC
- CTIGAR
- SAFARI
- Booster
- VERIFAS
- Verification of composed array-based systems with applications to security-aware workflows
- scientific article; zbMATH DE number 7566058 (Why is no real title available?)
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Lazy abstraction with interpolants for arrays
- Definability of accelerated relations in a theory of arrays and its applications
- MCMT: a model checker modulo theories
- Finite reasons for safety. Parameterized verification by finite model finding
- Satisfiability modulo theories
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- From model completeness to verification of data aware processes
- Analysis of a clock synchronization protocol for wireless sensor networks
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Rewriting modulo SMT and open system analysis
- Model completeness, covers and superposition
- Sally
- Btor2Tools
- Property-directed inference of universal invariants or proving their absence
- Combination of uniform interpolants via Beth definability
This page was built for software: Mcmt
