Formal verification of translation validators

DOI10.1145/1328438.1328444zbMath1295.68074OpenAlexW1981899763MaRDI QIDQ3189822

Jean-Baptiste Tristan, Xavier Leroy

Publication date: 12 September 2014

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

Full work available at URL: https://doi.org/10.1145/1328438.1328444

zbMATH Keywords

translation validationthe Coq proof assistantscheduling optimizationsverified compilers

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

Trustworthy variant derivation with translation validation for safety critical product lines ⋮ A formally verified compiler back-end ⋮ Certifying compilers using higher-order theorem provers as certificate checkers ⋮ A verified framework for higher-order uncurrying optimizations ⋮ Relational bytecode correlations

Uses Software

• Coq
• TVOC
• CVT

This page was built for publication: Formal verification of translation validators