Verifying Array Manipulating Programs with Full-Program Induction

DOI10.1007/978-3-030-45190-5_2OpenAlexW3013666522MaRDI QIDQ5039501

Divyesh Unadkat, Ashutosh Gupta, Supratik Chakraborty

Publication date: 13 October 2022

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

Mathematics Subject Classification ID

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

Related Items

\textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Lemmaless induction in trace logic ⋮ Interpolation and amalgamation for arrays with MaxDiff

Uses Software

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

Cites Work

• Unnamed Item
• Cell morphing: from array programs to array-free Horn clauses
• The Daikon system for dynamic detection of likely invariants
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• Lifting abstract interpreters to quantified logical domains
• Booster: An Acceleration-Based Verification Framework for Array Programs
• The program dependence graph and its use in optimization
• Aligators for Arrays (Tool Paper)
• Abstraction of Arrays Based on Non Contiguous Partitions
• Verifying Array Manipulating Programs by Tiling
• A framework for numeric analysis of array operations
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Array Abstractions from Proofs
• Invariant Synthesis for Combined Theories
• Bounded model checking using satisfiability solving
• Quantifiers on demand

This page was built for publication: Verifying Array Manipulating Programs with Full-Program Induction