Context Pruning for More Robust SMT-based Program Verification

No abstract is available for this paper.

• Publication year

  2024

• Venue

  Formal Methods in Computer-Aided Design

• Publication date

  2024-10-15

• Fields of study

  Computer Science

• Identifiers
  DOI 10.34727/2024/isbn.978-3-85448-065-5_12
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Incremental Proof Development in Dafny with Module-Based Induction

  2024cited by this paper
• Verus: Verifying Rust Programs using Linear Ghost Types

  2023cited by this paper
• Mariposa: Measuring SMT Instability in Automated Program Verification

  2023influential reference
• FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores

  2023cited by this paper
• Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems

  2023cited by this paper
• Linear types for large-scale systems verification

  2022cited by this paper
• Hardening attack surfaces with formally proven binary format parsers

  2022cited by this paper
• Provably-Safe Multilingual Software Sandboxing using WebAssembly

  2022cited by this paper
• cvc5: A Versatile and Industrial-Strength SMT Solver

  2022cited by this paper
• Formally Verifying Industry Cryptography

  2022cited by this paper
• Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3

  2021cited by this paper
• EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider

  2020cited by this paper
• Storage Systems are Distributed Systems (So Verify Them That Way!)

  2020cited by this paper
• HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms)

  2020cited by this paper
• EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats

  2019cited by this paper
• Formal Reasoning About the Security of Amazon Web Services

  2018cited by this paper
• Komodo: Using verification to disentangle secure-enclave hardware from software

  2017cited by this paper
• HACL*: A Verified Modern Cryptographic Library

  2017cited by this paper
• Benchmarking Solvers, SAT-style

  2017cited by this paper
• Trigger Selection Strategies to Stabilize Program Verifiers

  2016cited by this paper
• Dependent types and multi-monadic effects in F*

  2016cited by this paper
• IronFleet: proving practical distributed systems correct

  2015cited by this paper
• Ironclad Apps: End-to-End Security via Automated Full-System Verification

  2014cited by this paper
• Sine Qua Non for Large Theory Reasoning

  2011cited by this paper
• Dafny: An Automatic Program Verifier for Functional Correctness

  2010cited by this paper
• The SMT-LIB Standard Version 2.0

  2010cited by this paper
• Programming with triggers

  2009cited by this paper
• Lightweight relevance filtering for machine-generated resolution problems

  2009cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Using TF-IDF to Determine Word Relevance in Document Queries

  2003cited by this paper
• The TPTP Problem Library

  1994cited by this paper
• First-Order Logic and Automated Theorem Proving

  1990cited by this paper
• Depth-First Iterative-Deepening: An Optimal Admissible Tree Search

  1985cited by this paper
• Techniques for program verification

  1979cited by this paper
• Guarded commands, nondeterminacy and formal derivation of programs

  1975cited by this paper
• An axiomatic basis for computer programming

  1969cited by this paper
• Improving the Stability of Type Soundness Proofs in Dafny

  year unknowncited by this paper

• Formally Verified Cloud-Scale Authorization

  2025cites this paper
• Tunable Automation in Automated Program Verification

  2025cites this paper
• Accelerating Automated Program Verifiers by Automatic Proof Localization

  2025cites this paper
• Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router

  2025cites this paper
• Towards SMT Solver Stability via Input Normalization

  2024cites this paper
• A Conjecture Regarding SMT Instability

  year unknowncites this paper
• Instability Track for SMT-COMP

  year unknowncites this paper