Simplifying the Verification of Quantified Array Assertions via Code Transformation
DOI10.1007/978-3-642-38197-3_13zbMATH Open1394.68087OpenAlexW180202015MaRDI QIDQ2848907FDOQ2848907
Authors: Mohamed Nassim Seghir, Martin Brain 
Publication date: 13 September 2013
Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-38197-3_13
Recommendations
- Verifying Array Programs by Transforming Verification Conditions
- Abstraction Refinement for Quantified Array Assertions
- An assume guarantee approach for checking quantified array assertions
- Transformational Verification of Parameterized Protocols Using Array Formulas
- Artificial Intelligence and Symbolic Computation
- Scaling bounded model checking by transforming programs with arrays
- scientific article; zbMATH DE number 7453193
- A rule-based verification strategy for array manipulating programs
- Putting the squeeze on array programs: loop verification via inductive rank reduction
Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (7)
- \textsc{Diffy}: inductive reasoning of array programs using difference invariants
- Scaling bounded model checking by transforming programs with arrays
- Verifying Array Programs by Transforming Verification Conditions
- Abstraction Refinement for Quantified Array Assertions
- An assume guarantee approach for checking quantified array assertions
- Verifying Array Manipulating Programs with Full-Program Induction
- Title not available (Why is that?)
This page was built for publication: Simplifying the Verification of Quantified Array Assertions via Code Transformation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848907)
