Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
From MaRDI portal
Publication:2829257
DOI10.1007/978-3-319-43144-4_11zbMath1468.68129OpenAlexW2495204228MaRDI QIDQ2829257
Adam Chlipala, Thomas Grégoire
Publication date: 27 October 2016
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://hdl.handle.net/1721.1/131765
Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
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
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- Formal Proof of a Wave Equation Resolution Scheme: The Method Error
This page was built for publication: Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
