Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
From MaRDI portal
Publication:1722642
DOI10.1007/s10817-018-9451-yzbMath1468.68130MaRDI 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
formal software verification; automated software verification; distributed stencil algorithms; loop dependencies; stencil algorithm
68Q60: Specification and verification (program logics, model checking, etc.)
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- 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