\textsc{Diffy}: inductive reasoning of array programs using difference invariants
From MaRDI portal
Publication:832320
DOI10.1007/978-3-030-81688-9_42zbMath1493.68101arXiv2105.14748OpenAlexW3183515470MaRDI QIDQ832320
Divyesh Unadkat, Supratik Chakraborty, Ashutosh Gupta
Publication date: 25 March 2022
Full work available at URL: https://arxiv.org/abs/2105.14748
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (2)
Uses Software
Cites Work
- A formalization of programs in first-order logic with a discrete linear order
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- 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
- Lazy Abstraction with Interpolants for Arrays
- Lifting abstract interpreters to quantified logical domains
- Booster: An Acceleration-Based Verification Framework for Array Programs
- Fast Acceleration of Ultimately Periodic Relations
- Finite Differencing of Computable Expressions
- Verifying Array Manipulating Programs with Full-Program Induction
- Abstraction of Arrays Based on Non Contiguous Partitions
- Predicate abstraction for software verification
- Verifying Array Manipulating Programs by Tiling
- A framework for numeric analysis of array operations
- Abstract acceleration of general linear loops
- A parametric segmentation functor for fully automatic and scalable array content analysis
- Array Abstractions from Proofs
- Invariant Synthesis for Combined Theories
- Computer Aided Verification
- Quantifiers on demand
- Quantified invariants via syntax-guided synthesis
This page was built for publication: \textsc{Diffy}: inductive reasoning of array programs using difference invariants
