Automating Verification of Loops by Parallelization

DOI10.1007/11916277_23zbMATH Open1165.68405OpenAlexW1557508031MaRDI QIDQ5387902FDOQ5387902

Authors: Tobias Gedell, Reiner Hähnle 

Publication date: 27 May 2008

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11916277_23

Recommendations

• Verification by Parallelization of Parametric Code
• Reasoning about loops using Vampire in KeY
• Synthesizing invariants by solving solvable loops
• Mechanical inference of invariants for FOR-loops
• Proof spaces for unbounded parallelism

Mathematics Subject Classification ID

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

Cited In (5)

• Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
• Verification by Parallelization of Parametric Code
• Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
• Reasoning about loops using Vampire in KeY
• A program logic for dependence analysis

Uses Software

• ESC/Java
• KeY

This page was built for publication: Automating Verification of Loops by Parallelization

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