What’s Decidable About Program Verification Modulo Axioms?
From MaRDI portal
Publication:5164172
DOI10.1007/978-3-030-45237-7_10zbMath1483.68200arXiv1910.10889OpenAlexW3021960956MaRDI QIDQ5164172
P. Madhusudan, Umang Mathur, Mahesh Viswanathan
Publication date: 10 November 2021
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1910.10889
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Graph minors. I. Excluding a forest
- Complexity results for classes of quantificational formulas
- EUFORIA: complete software model checking with uninterpreted functions
- Kleene algebra with hypotheses
- Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth
- Proof Spaces for Unbounded Parallelism
- Decidability of inferring inductive invariants
- Algorithms for algebraic path properties in concurrent systems of constant treewidth components
- Inductive data flow graphs
- Refinement of Trace Abstraction
- Invariant Checking for Programs with Procedure Calls
- Recursive Unsolvability of a problem of Thue
- Kleene Algebra with Equations
- Nested interpolants
- Proofs that count
- Modular reasoning about heap paths via effectively propositional formulas
- The tree width of auxiliary storage
- Structural Abstraction of Software Verification Conditions
- Assertion Checking Unified
- Reveal: A Formal Verification Tool for Verilog Designs
- Verification, Model Checking, and Abstract Interpretation
- Deductive verification in decidable fragments with Ivy
This page was built for publication: What’s Decidable About Program Verification Modulo Axioms?
