Automatic Parallelization and Optimization of Programs by Proof Rewriting

DOI10.1007/978-3-642-03237-0_6MaRDI QIDQ3392920zbMATH OpenOpenAlexFDO

Authors Clément Hurlin

Publication date 18 August 2009

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00380528v2/file/finalversion.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Automatic Parallelization with Separation Logic
• Concurrent separation logic for pipelined parallelization
• Publication:4728226
• Proof optimization for partial redundancy elimination
• Certifiably Sound Parallelizing Transformations

Cites work

• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Automatic Parallelization with Separation Logic
• Certificate Translation for Optimizing Compilers
• Enhancing modular OO verification with separation logic
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 2090288 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• Local Reasoning for Storable Locks and Threads
• Programming Languages and Systems
• Resources, concurrency, and local reasoning
• Separation Logic Contracts for a Java-Like Language with Fork/Join
• Shape Analysis for Composite Data Structures
• The parallel execution of DO loops
• Tools and Algorithms for the Construction and Analysis of Systems
• Variables as resource in separation logic

Cited in

(11)

• The automated proof of a trace transformation for a bitonic sort
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• scientific article; zbMATH DE number 4164183 (Why is no real title available?)
• Automatic Parallelization with Separation Logic
• scientific article; zbMATH DE number 3902008 (Why is no real title available?)
• scientific article; zbMATH DE number 4003499 (Why is no real title available?)
• Concurrent separation logic for pipelined parallelization
• Generating compiler optimizations from proofs
• Formal program optimization in Nuprl using computational equivalence and partial types
• On optimal parallelization of sorting networks
• A formal model of a system for automated program parallelization

Describes a project that uses

Uses Software

• VeriFast
• Isabelle
• jStar
• Smallfoot
• Tom

This page was built for publication: Automatic Parallelization and Optimization of Programs by Proof Rewriting

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