Certifiably Sound Parallelizing Transformations

DOI10.1007/978-3-319-03545-1_15MaRDI QIDQ2938050zbMATH OpenOpenAlexFDO

Authors Christian J. Bell

Publication date 13 January 2015

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-03545-1_15

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A class of parallelizing transformation
• scientific article; zbMATH DE number 526062
• scientific article; zbMATH DE number 3978360
• scientific article; zbMATH DE number 3890707
• scientific article; zbMATH DE number 1946645
• scientific article; zbMATH DE number 719843
• Time-bounded parallel rewriting

Cited in

(9)

• Calculating certified compilers for non-deterministic languages
• Synthesizing and verifying multicore parallelism in categories of nested code graphs
• Characterizing contrasimilarity through games, modal logic, and complexity
• A game characterization for contrasimilarity
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Testing parallel variable transformation
• A path construction algorithm for translation validation using PRES+ models
• Translation validation of coloured Petri net models of programs on integers
• One energy game for the spectrum between branching bisimilarity and weak trace semantics

Describes a project that uses

Uses Software

• CompCert
• Coq

This page was built for publication: Certifiably Sound Parallelizing Transformations

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