A simple, verified validator for software pipelining

DOI10.1145/1706299.1706311MaRDI QIDQ5255064zbMATH OpenOpenAlexFDO

Authors Jean-Baptiste Tristan, Xavier Leroy

Publication date 11 June 2015

Published in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00529836/document

zbMATH Keywords

software pipeliningsymbolic evaluationtranslation validationverified compilers

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Formal verification of a complex pipelined processor
• Automatic Refinement Checking of Pipelines with Out-of-Order Execution
• scientific article; zbMATH DE number 2079670
• scientific article; zbMATH DE number 50008
• Verification of sequential and concurrent programs
• Computer Aided Verification

Cited in

(5)

• Formal verification of synchronous data-flow program transformations toward certified compilers
• Mechanical certification of loop pipelining transformations: a preview
• scientific article; zbMATH DE number 2112163 (Why is no real title available?)
• Translation validation of loop optimizations and software pipelining in the TVOC framework. In memory of Amir Pnueli
• Translation and run-time validation of loop transformations

Describes a project that uses

Uses Software

• TVOC
• CVT

This page was built for publication: A simple, verified validator for software pipelining

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