Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
From MaRDI portal
Cites work
- A polymorphic intermediate verification language: design and logical encoding
- A Reachability Predicate for Analyzing Low-Level Software
- AVATAR: The Architecture for First-Order Theorem Provers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Dafny: an automatic program verifier for functional correctness
- Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
- E-matching with free variables
- Isabelle/HOL. A proof assistant for higher-order logic
- Modeling in Event B. System and software engineering.
- Resource protection using atomics. Patterns and verification
- Revisiting enumerative instantiation
- Simplify: a theorem prover for program checking
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Towards bit-width-independent proofs in SMT solvers
- Unification theory
- Verification of Equivalent-Results Methods
- Verified software toolchain (invited talk)
- Viper: a verification infrastructure for permission-based reasoning
This page was built for publication: Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6610379)
