What's decidable about program verification modulo axioms?

DOI10.1007/978-3-030-45237-7_10MaRDI QIDQ5164172zbMATH OpenOpenAlexFDO

Authors Umang Mathur, Parthasarathy Madhusudan, Mahesh Viswanathan

Publication date 10 November 2021

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1910.10889

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We consider the decidability of the verification problem of programs emph{modulo axioms} --- that is, verifying whether programs satisfy their assertions, when the functions and relations it uses are assumed to interpreted by arbitrary functions and relations that satisfy a set of first-order axioms. Unfortunately, verification of entirely uninterpreted programs (with the empty set of axioms) is already undecidable. A recent work introduced a subclass of emph{coherent} uninterpreted programs, and showed that they admit decidable verification cite{coherence2019}. We undertake a systematic study of various natural axioms for relations and functions, and study the decidability of the coherent verification problem. Axioms include relations being reflexive, symmetric, transitive, or total order relations, %and their combinations, functions restricted to being associative, idempotent or commutative, and combinations of such axioms as well. Our comprehensive results unearth a rich landscape that shows that though several axiom classes admit decidability for coherent programs, coherence is not a panacea as several others continue to be undecidable.

Recommendations

• Decidable synthesis of programs with uninterpreted functions
• Towards Complete Reasoning about Axiomatic Specifications
• Application of conditional term substitution systems in program verification
• Verification, Model Checking, and Abstract Interpretation
• Reachability modulo theories

Cites work

• Algorithms for algebraic path properties in concurrent systems of constant treewidth components
• Assertion Checking Unified
• Complexity results for classes of quantificational formulas
• Decidability of inferring inductive invariants
• Deductive verification in decidable fragments with Ivy
• EUFORIA: complete software model checking with uninterpreted functions
• Faster algorithms for algebraic path properties in recursive state machines with constant treewidth
• Graph minors. I. Excluding a forest
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• scientific article; zbMATH DE number 1903346 (Why is no real title available?)
• Inductive data flow graphs
• Invariant Checking for Programs with Procedure Calls
• Kleene algebra with equations
• Kleene algebra with hypotheses
• Modular reasoning about heap paths via effectively propositional formulas
• Nested interpolants
• Proof spaces for unbounded parallelism
• Proofs that count
• Recursive unsolvability of a problem of Thue
• Reduced functional consistency of uninterpreted functions
• Refinement of Trace Abstraction
• Reveal: A Formal Verification Tool for Verilog Designs
• Structural Abstraction of Software Verification Conditions
• The tree width of auxiliary storage
• Verification, Model Checking, and Abstract Interpretation

Cited in

(3)

• Decidable synthesis of programs with uninterpreted functions
• Temporal stream logic modulo theories
• Trace Abstraction-Based Verification for Uninterpreted Programs

Describes a project that uses

Uses Software

• Reveal

This page was built for publication: What's decidable about program verification modulo axioms?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5164172)