Data abstraction: a general framework to handle program verification of data structures

DOI10.1007/978-3-030-88806-0_11zbMath1497.68108OpenAlexW3189854873MaRDI QIDQ2145329

Laure Gonnord, Julien Braine, David Monniaux

Publication date: 17 June 2022

Full work available at URL: https://hal.inria.fr/hal-03321868/file/braine_al_sas2021.pdf

zbMATH Keywords

Horn clausesstatic analysisabstraction

Mathematics Subject Classification ID

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

Uses Software

• z3
• FunArray
• SeaHorn
• JayHorn

Cites Work

• 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
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Grammar Analysis and Parsing by Abstract Interpretation
• A framework for numeric analysis of array operations
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Verification, Model Checking, and Abstract Interpretation
• Quantifiers on demand

This page was built for publication: Data abstraction: a general framework to handle program verification of data structures