Data abstraction: a general framework to handle program verification of data structures
type: Item
instance of: scholarly article
title: Data abstraction: a general framework to handle program verification of data structures
zbMATH Open document ID: 1497.68108
DOI: 10.1007/978-3-030-88806-0_11
author: Julien Braine
author: Laure Gonnord
author: David Monniaux
publication date: 2022-06-17T00:00:00Z
full work available at URL: braine al sas2021.pdf
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68P05
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 7543916
zbMATH Keywords: static analysis
zbMATH Keywords: Horn clauses
zbMATH Keywords: abstraction
describes a project that uses: FunArray
describes a project that uses: SeaHorn
describes a project that uses: z3
describes a project that uses: JayHorn
MaRDI profile type: MaRDI publication profile
OpenAlex ID: W3189854873
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: Grammar Analysis and Parsing by Abstract Interpretation
cites work: A parametric segmentation functor for fully automatic and scalable array content analysis
cites work: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
cites work: A framework for numeric analysis of array operations
cites work: Quantifiers on demand
cites work: Putting the squeeze on array programs: loop verification via inductive rank reduction
cites work: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
cites work: Cell morphing: from array programs to array-free Horn clauses
Recommended article: Artificial Intelligence and Symbolic Computation
Recommended article: Abstraction Refinement for Quantified Array Assertions
Recommended article: Formal Methods at the Crossroads. From Panacea to Foundational Support
Recommended article: Predicate abstraction for linked data structures
Recommended article: Computer Aided Verification
description: scientific article; zbMATH DE number 7543916