Verifying array manipulating programs with full-program induction

DOI10.1007/978-3-030-45190-5_2MaRDI QIDQ5039501zbMATH OpenOpenAlexFDO

Authors Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat

Publication date 13 October 2022

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/2002.09857

Mathematics Subject Classification ID

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

Recommendations

• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Verifying array manipulating programs by tiling
• Automatic Verification of Integer Array Programs
• Analyzing Array Manipulating Programs by Program Transformation
• A rule-based verification strategy for array manipulating programs

Cites work

• A framework for numeric analysis of array operations
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Abstraction of arrays based on non contiguous partitions
• Aligators for Arrays (Tool Paper)
• Array Abstractions from Proofs
• Booster: an acceleration-based verification framework for array programs
• Bounded model checking using satisfiability solving
• Cell morphing: from array programs to array-free Horn clauses
• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• Invariant Synthesis for Combined Theories
• Lifting abstract interpreters to quantified logical domains
• Quantifiers on demand
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• The Daikon system for dynamic detection of likely invariants
• The program dependence graph and its use in optimization
• Verifying array manipulating programs by tiling

Cited in

(8)

• Interpolation and amalgamation for arrays with MaxDiff
• Property checking array programs using loop shrinking
• Verifying Array Programs by Transforming Verification Conditions
• scientific article; zbMATH DE number 6687732 (Why is no real title available?)
• Verifying array manipulating programs by tiling
• Lemmaless induction in trace logic
• Putting the squeeze on array programs: loop verification via inductive rank reduction
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants

Describes a project that uses

Uses Software

• FunArray
• z3
• Booster
• Houdini
• VeriFast
• Daikon
• Aligators

This page was built for publication: Verifying array manipulating programs with full-program induction

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