Automating Verification of Loops by Parallelization

DOI10.1007/11916277_23MaRDI QIDQ5387902zbMATH OpenOpenAlexFDO

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

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

• 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

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

Describes a project that uses

Uses Software

• KeY
• ESC/Java

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)