The verifying compiler: A grand challenge for computing research
By T. Hoare. JACM, 2003
423 citations recorded by the source corpus.
Subfields: Computational Theory and Mathematics, Safety Research
View Paper: https://www.semanticscholar.org/paper/26ecddf52ee82dbe016220fe4bde165bbe4afc02
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
- Dirk Beyer
- Ranjit Jhala
- Rupak Majumdar
- Thomas A. Henzinger
- Benjamin C. Pierce
- Steve Zdancewic
- Dimitrios Vytiniotis
- Joseph Sifakis
In Safety Research
Citations in the corpus
- Stanford Encyclopedia of Philosophy: a dynamic reference work (2003, background): “How to implement bug-free computer systems remains an open research question (Hoare 2003).”
- Building a push-button RESOLVE verifier: Progress and challenges (2011, neutral): “Automation is a fundamental challenge in developing a verifier and eventually realizing the grand challenge of building verified software [ 25 ][26].”
- Compiler validation via equivalence modulo inputs (2014, neutral): “C; H.3.4 [Programming Languages]: Processors—compilers General Terms Algorithms, Languages, Reliability, Verification Keywords Compiler testing, miscompilation, equivalent program variants, automated testing”
- The software model checker Blast (2007, background): “The area has received much research attention in recent years owing to new algorithmic techniques (such as CEGAR) and faster computers, which have renewed the promise of providing automatic tools for checking program correctness and generating counterexamples [51].”
- Mechanized Metatheory for the Masses: The PoplMark Challenge (2005, methodology): “Such challenge problems have been used in the past within the theorem proving community to focus attention on specific areas and to evaluate the relative merits of different tools; these have ranged in scale from benchmark suites and small problems [31,12,5,15,9,21] up to the grand challenges of Flo”
- Formal methods: Practice and experience (2009, neutral): “In 2003, Tony Hoare proposed the Verifying Compiler as a Grand Challenge for Computer Science [Hoare 2003].”
- The Embedded Systems Design Challenge (2006, background): “…advocated challenges for Computer Science research push existing technology to the limits (e.g., the semantic web [4]; the verifying compiler [15]; sensor networks [6]), to new application areas (such as biology [12]), or to a combination of both (e.g., nanotechnologies; quantum computing).”