Pages that link to "Item:Q3081445"
From MaRDI portal
The following pages link to Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis (Q3081445):
Displaying 14 items.
- Decision procedures for flat array properties (Q287272) (← links)
- An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
- Multi-parameterised compositional verification of safety properties (Q498394) (← links)
- A unifying view on SMT-based software verification (Q1703012) (← links)
- Superposition as a decision procedure for timed automata (Q1949086) (← links)
- Formal specification and verification of dynamic parametrized architectures (Q2024379) (← links)
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems (Q2031422) (← links)
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning (Q2055851) (← links)
- Combination of uniform interpolants via Beth definability (Q2090132) (← links)
- Parameterized model checking on the TSO weak memory model (Q2208293) (← links)
- On invariant synthesis for parametric systems (Q2305429) (← links)
- Symbolic backward reachability with effectively propositional logic. Application to security policy analysis (Q2441771) (← links)
- SMT-based verification of data-aware processes: a model-theoretic approach (Q5139282) (← links)
- Predicate Abstraction in Program Verification: Survey and Current Trends (Q5240105) (← links)
