Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
From MaRDI portal
Publication:6610379
DOI10.1145/3571748MaRDI QIDQ6610379
Arshavir Ter-Gabrielyan, Alexandra Bugariu, Peter K. Müller
Publication date: 25 September 2024
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Cites Work
- Unnamed Item
- Isabelle/HOL. A proof assistant for higher-order logic
- Counterexample-guided quantifier instantiation for synthesis in SMT
- Towards bit-width-independent proofs in SMT solvers
- Revisiting enumerative instantiation
- Unification theory
- Resource Protection Using Atomics
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- Dependent types and multi-monadic effects in F*
- E-Matching with Free Variables
- AVATAR: The Architecture for First-Order Theorem Provers
- Verified Software Toolchain
- Dafny: An Automatic Program Verifier for Functional Correctness
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Simplify: a theorem prover for program checking
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Verification of Equivalent-Results Methods
- A Reachability Predicate for Analyzing Low-Level Software
This page was built for publication: Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
