Array abstraction with symbolic pivots

DOI10.1007/978-3-319-30734-3_9MaRDI QIDQ2026786zbMATH OpenOpenAlexFDO

Authors Reiner Hähnle, Nathan Wasser, Richard Bubel

Publication date 20 May 2021

Full work available at URL https://doi.org/10.1007/978-3-319-30734-3_9

zbMATH Keywords

abstract interpretationarray abstractionloop-invariant generationprogram verification

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

• Lazy abstraction with interpolants for arrays
• Array Abstractions from Proofs
• scientific article; zbMATH DE number 1979540
• An extension of lazy abstraction with interpolation for programs with arrays
• Abstracting symbolic matrices
• A symbolic treatment of Riordan arrays
• Abstraction Refinement of Linear Programs with Arrays
• Checking array bounds by abstract interpretation and symbolic expressions
• Abstraction of arrays based on non contiguous partitions

Cited in

(2)

• A variation of van der Meulen diagrams for array manipulation
• Maximal and compositional pattern-based loop invariants

This page was built for publication: Array abstraction with symbolic pivots

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