Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms

DOI10.1007/s10817-018-9451-yzbMath1468.68130OpenAlexW3022528433MaRDI QIDQ1722642

Adam Chlipala, Thomas Grégoire

Publication date: 18 February 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hdl.handle.net/1721.1/131765

zbMATH Keywords

formal software verificationautomated software verificationdistributed stencil algorithmsloop dependenciesstencil algorithm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• PolyLib
• GPUVerify
• GKLEE
• Pochoir

Cites Work

• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• The cache complexity of multithreaded cache oblivious algorithms
• Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Embedding of Systems of Affine Recurrence Equations in Coq
• Formal Proof of a Wave Equation Resolution Scheme: The Method Error
• Unnamed Item
• Unnamed Item

This page was built for publication: Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms