Compiler validation via equivalence modulo inputs

By Vu Le, Mehrdad Afshari, Zhendong Su. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2014

603 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/79bbd54d5bdfd20980e5f9a65480f5e127fc1221

How researchers see this paper

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

In Computational Theory and Mathematics

In Software

Citations in the corpus

Large Language Models Are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models (2022, methodology): “Additionally, TitanFuzz is the rst work to demonstrate that LLMs can perform both generation-based [30, 80] and mutation-based [39, 50] fuzzing studied for decades [84], while being fully automated, generalizable, and applicable to domains challenging for traditional approaches (such as DL systems).”
Coverage-directed differential testing of JVM implementations (2016, methodology): “Fuzz testing has also been employed to ﬁnd issues re-lated to system calls [14, 40], security protocols [11, 36], language compilers [22] and interpreters [19, 32].”
Learning to Fuzz from Symbolic Execution with Application to Smart Contracts (2019, neutral): “Because of its simplicity and practical effectiveness, fuzzing has become one of the main approaches for software testing [21, 30, 38, 68].”
A design and verification methodology for secure isolated regions (2016, background): “However, compilers are large code bases and have been shown to have bugs and produce wrong code at times [6, 23, 26, 29, 46].”
Metamorphic Testing (2018, methodology): “detect hundreds of real-life bugs in two popular compilers [50] is strong evidence that identication of good MRs may not be dicult at all.”
Machine Learning Testing: Survey, Landscapes and Horizons (2019, methodology): “It is a testing oracle for detecting compiler bugs [132].”
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].”
Superion: Grammar-Aware Greybox Fuzzing (2018, positive): “It is worth mentioning that application-speciﬁc fuzzers have been attracting great interests, e.g., compiler fuzzing [16, 18, 39, 40, 44, 60], kernel fuzzing [17, 31, 58], IoT (Internet of Things) fuzzing [14], OS fuzzing [49] and smart contract fuzzing [36].”
Learning to Fuzz: Application-Independent Fuzz Testing with Probabilistic, Generative Models of Input Data (2016, background): “Other work proposes oracles to determine whether a program exposes a bug in the compiler or execution engine [26, 27, 48] and on ranking generated programs [15].”
A Survey on Metamorphic Testing (2016, background): “A closely related idea was presented by Le et al. [119].”
Verdi: a framework for implementing and formally verifying distributed systems (2015, methodology): “The CompCert C compiler [22] was verified in Coq and repeatedly shown to be more reliable than traditionally developed compilers [21, 41].”