Automated soundness proofs for dataflow analyses and transformations via local rules

DOI10.1145/1040305.1040335zbMath1369.68145OpenAlexW2144540543MaRDI QIDQ5276160

Craig Chambers, Todd D. Millstein, Sorin Lerner, Erika Rice

Publication date: 14 July 2017

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

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.122.5996

zbMATH Keywords

compiler optimizationautomated correctness proofs

Mathematics Subject Classification ID

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

Related Items (7)

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ Proof optimization for partial redundancy elimination ⋮ A formally verified compiler back-end ⋮ Certifying compilers using higher-order theorem provers as certificate checkers ⋮ Relational bytecode correlations ⋮ Relational Decomposition ⋮ Inter-program Properties

This page was built for publication: Automated soundness proofs for dataflow analyses and transformations via local rules