\textsc{Diffy}: inductive reasoning of array programs using difference invariants

DOI10.1007/978-3-030-81688-9_42MaRDI QIDQ832320zbMATH OpenOpenAlexFDO

Authors Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

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 $N$, 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.

Recommendations

• Verifying array manipulating programs with full-program induction
• Automatic Verification of Integer Array Programs
• Property checking array programs using loop shrinking
• Verifying array manipulating programs by tiling
• Array Abstractions from Proofs

Cites work

• A formalization of programs in first-order logic with a discrete linear order
• A framework for numeric analysis of array operations
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Abstract acceleration of general linear loops
• Abstraction of arrays based on non contiguous partitions
• Array Abstractions from Proofs
• Booster: an acceleration-based verification framework for array programs
• Cell morphing: from array programs to array-free Horn clauses
• Computer Aided Verification
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• Fast acceleration of ultimately periodic relations
• Finite Differencing of Computable Expressions
• Invariant Synthesis for Combined Theories
• Lazy abstraction with interpolants for arrays
• Lifting abstract interpreters to quantified logical domains
• Predicate abstraction for software verification
• Putting the squeeze on array programs: loop verification via inductive rank reduction
• Quantified invariants via syntax-guided synthesis
• Quantifiers on demand
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• Verifying array manipulating programs by tiling
• Verifying array manipulating programs with full-program induction

Cited in

(3)

• Diffy
• Verifying array manipulating programs with full-program induction
• Lemmaless induction in trace logic

Describes a project that uses

Uses Software

• FLATA
• z3
• FunArray
• CoVaC
• Booster

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)