Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms

DOI10.1007/978-3-319-43144-4_11MaRDI QIDQ2829257zbMATH OpenOpenAlexFDO

Authors T. Gregoire, Adam Chlipala

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

Mathematics Subject Classification ID

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

Recommendations

• Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
• Formal Verification of Distributed Algorithms
• Automatic verification for a class of distributed systems
• Automatic verification of determinism for structured parallel programs
• Automating Verification of Loops by Parallelization
• A strategy for automatic verification of stabilization of distributed algorithms
• An automata-theoretic approach to the verification of distributed algorithms
• An automata-theoretic approach to the verification of distributed algorithms
• Formal verification of a programming logic for a distributed programming language

Cites work

• scientific article; zbMATH DE number 5209981 (Why is no real title available?)
• scientific article; zbMATH DE number 5180707 (Why is no real title available?)
• Formal proof of a wave equation resolution scheme: the method error
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• The cache complexity of multithreaded cache oblivious algorithms
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Cited in

(1)

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

Describes a project that uses

Uses Software

• Coq
• PolyLib
• GPUVerify
• GKLEE
• Pochoir

This page was built for publication: Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms

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