Translation validation for an optimizing compiler

By George C. Necula. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2000

570 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Information Systems, Software

View Paper: https://www.semanticscholar.org/paper/011f7da0095ac8c0d4477eeda2728e5f80a35767

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Software

Citations in the corpus

Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation (2023, methodology): “Ideally, we would like to formally verify the correctness of LLM-provided solutions for any input, but verifying domain-specific problems through methods such as translation validation [29, 36, 4] is already challenging enough, let alone building a general verifier with absolute certainty to prove a”
MLIR: Scaling Compiler Infrastructure for Domain Specific Computation (2021, unknown): “A long term goal would be to reproduce the successes of translation validation [11], [12], [13], [14] and modern approaches to compiler testing [15].”
Formal certification of a compiler back-end or: programming a compiler with a proof assistant (2006, methodology): “Going further, whole transformation passes could be performed by untrusted code, then checked for semantic equivalence using Hoare logic and symbolic evaluation as in [24].”
Synthesizing coupling proofs of differential privacy (2017, unknown): “, in translation-validation [37, 38], security problems [18, 43], and Java code [41].”
A design and verification methodology for secure isolated regions (2016, background): “, [32, 35, 41, 42]) is a set of techniques that attempt to prove that compiler optimizations did not change the semantics of the program given as input (after the optimizer run).”
Simple relational correctness proofs for static analyses and program transformations (2004, background): “The work that is most closely related to that presented here has been done in the contexts of credible compilation [24, 25] and translation validation [21, 36].”
Semantics-aware malware detection (2005, methodology): “The translation-validation problem is the problem of determining whether P ′ “simulates” P [31, 32].”
WYSINWYX: What you see is not what you eXecute (2010, background): “For instanc e, the aim oftranslation validation[33, 32] is to verify that compilation does not change the sem antics of a program.”
TASO: optimizing deep learning computation with automatic generation of graph substitutions (2019, background): “In the compiler literature, significant effort has been devoted to formally verifying optimizations [7, 11, 13, 23, 29, 30, 33, 35].”
Compiler validation via equivalence modulo inputs (2014, unknown): “C; H.3.4 [Programming Languages]: Processors—compilers General Terms Algorithms, Languages, Reliability, Verification Keywords Compiler testing, miscompilation, equivalent program variants, automated testing”
The New C Standard (Excerpted material) An Economic and Cultural Commentary (2008, unknown): “Researchers continue to increase the size of the language subsets for which translators have been proved correct.[7, 9, 11] They have also looked at proving some of the components of an existing translator, gcc, correct.[ 8 ]”
Formal verification of a realistic compiler (2009, methodology): “To account for these degrees of freedom in the compiler, we relax deﬁnition (1) as follows: (Here, S safe means that none of the possible behaviors of S is a“going wrong”behavior.)”
Equality saturation: a new approach to optimization (2009, methodology): “Although previous approaches to translation validation have been explored [30, 25, 43, 31], our approach has the advantage that it can perform translation val idation by using the same technique as for program optimization.”
MLIR: A Compiler Infrastructure for the End of Moore's Law (2020, background): “A long term goal would be to reproduce the successes of translation validation [35, 29, 50, 51] and modern approaches to compiler testing [12].”
A Formally Verified Compiler Back-end (2009, methodology): “Validation can be performed in several ways, ranging from symbolic interpretation and static analysis of S and C [76,87,44,93,94] to the generation of verification conditions followed by model checking or automatic theorem proving [83,95,4].”