\textsc{Diffy}: inductive reasoning of array programs using difference invariants
From MaRDI portal
Publication:832320
DOI10.1007/978-3-030-81688-9_42zbMATH Open1493.68101arXiv2105.14748OpenAlexW3183515470MaRDI QIDQ832320FDOQ832320
Authors: Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat 
Publication date: 25 March 2022
Abstract: We present a novel verification technique to prove interesting properties of a class of array programs with a symbolic parameter N denoting the size of arrays. The technique relies on constructing two slightly different versions of the same program. It infers difference relations between the corresponding variables at key control points of the joint control-flow graph of the two program versions. The desired post-condition is then proved by inducting on the program parameter , wherein the difference invariants are crucially used in the inductive step. This contrasts with classical techniques that rely on finding potentially complex loop invaraints for each loop in the program. Our synergistic combination of inductive reasoning and finding simple difference invariants helps prove properties of programs that cannot be proved even by the winner of Arrays sub-category from SV-COMP 2021. We have implemented a prototype tool called diffy to demonstrate these ideas. We present results comparing the performance of diffy with that of state-of-the-art tools.
Full work available at URL: https://arxiv.org/abs/2105.14748
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Computer Aided Verification
- A parametric segmentation functor for fully automatic and scalable array content analysis
- Booster: an acceleration-based verification framework for array programs
- A formalization of programs in first-order logic with a discrete linear order
- A framework for numeric analysis of array operations
- Lazy abstraction with interpolants for arrays
- Array Abstractions from Proofs
- Invariant Synthesis for Combined Theories
- Fast acceleration of ultimately periodic relations
- Predicate abstraction for software verification
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- Finite Differencing of Computable Expressions
- Lifting abstract interpreters to quantified logical domains
- Abstraction of arrays based on non contiguous partitions
- Verifying array manipulating programs with full-program induction
- Putting the squeeze on array programs: loop verification via inductive rank reduction
- Cell morphing: from array programs to array-free Horn clauses
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Simplifying the Verification of Quantified Array Assertions via Code Transformation
- Verifying array manipulating programs by tiling
- Abstract acceleration of general linear loops
- Quantifiers on demand
- Quantified invariants via syntax-guided synthesis
Cited In (3)
Uses Software
This page was built for publication: \textsc{Diffy}: inductive reasoning of array programs using difference invariants
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832320)
