source: Papers/cpp-exec-2012/ccexec.bib @ 3456

Last change on this file since 3456 was 2381, checked in by campbell, 7 years ago

Executable semantics paper as it was in the first submission.

File size: 19.8 KB
Line 
1Entry made up
2
3@article{MilnerWeyhrauch72,
4  title = {Proving compiler correctness in a mechanized logic},
5  author = {R. Milner and R. Weyhrauch},
6  journal = {Machine Intelligence},
7  year = 1972,
8  volume = 7,
9  pages = {51--70},
10  editors = {Bernard Meltzer and Donald Michie},
11  publisher = {Edinburgh University Press}
12}
13
14Entry from ACM Digital Library.
15
16@inproceedings{Tatlock:2010:BEV:1806596.1806611,
17 author = {Tatlock, Zachary and Lerner, Sorin},
18 title = {Bringing extensibility to verified compilers},
19 booktitle = {Proceedings of the 2010 ACM SIGPLAN conference on Programming language design and implementation},
20 series = {PLDI '10},
21 year = {2010},
22 isbn = {978-1-4503-0019-3},
23 location = {Toronto, Ontario, Canada},
24 pages = {111--121},
25 numpages = {11},
26 url = {http://doi.acm.org/10.1145/1806596.1806611},
27 doi = {http://doi.acm.org/10.1145/1806596.1806611},
28 acmid = {1806611},
29 publisher = {ACM},
30 address = {New York, NY, USA},
31 keywords = {compiler optimization, correctness, extensibility},
32}
33
34Entry from ACM Digitial Library.  (With name fixup)
35
36@inproceedings{Sevcik:2011:RCV:1926385.1926393,
37 author = {\v{S}ev\v{c}\'{i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
38 title = {Relaxed-memory concurrency and verified compilation},
39 booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
40 series = {POPL '11},
41 year = {2011},
42 isbn = {978-1-4503-0490-0},
43 location = {Austin, Texas, USA},
44 pages = {43--54},
45 numpages = {12},
46 url = {http://doi.acm.org/10.1145/1926385.1926393},
47 doi = {http://doi.acm.org/10.1145/1926385.1926393},
48 acmid = {1926393},
49 publisher = {ACM},
50 address = {New York, NY, USA},
51 keywords = {relaxed memory models, semantics, verifying compilation},
52}
53
54Entry from ACM Digital Library.
55
56@article{Leroy:2009:FVR:1538788.1538814,
57 author = {Leroy, Xavier},
58 title = {Formal verification of a realistic compiler},
59 journal = {Commun. ACM},
60 issue_date = {July 2009},
61 volume = {52},
62 issue = {7},
63 month = jul,
64 year = {2009},
65 issn = {0001-0782},
66 pages = {107--115},
67 numpages = {9},
68 url = {http://doi.acm.org/10.1145/1538788.1538814},
69 doi = {http://doi.acm.org/10.1145/1538788.1538814},
70 acmid = {1538814},
71 publisher = {ACM},
72 address = {New York, NY, USA},
73}
74
75Entry from ACM Digital Library.
76
77@inproceedings{1328444,
78 author = {Jean-Baptiste Tristan and Xavier Leroy},
79 title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
80 booktitle = {POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
81 year = {2008},
82 isbn = {978-1-59593-689-9},
83 pages = {17--27},
84 location = {San Francisco, California, USA},
85 doi = {http://doi.acm.org/10.1145/1328438.1328444},
86 publisher = {ACM},
87 address = {New York, NY, USA},
88 }
89
90Entry made up.
91
92@inproceedings{coqextr02,
93  title  = {A New Extraction for {C}oq},
94  author = {Pierre Letouzey},
95  booktitle = {Types for Proofs and Programs (TYPES 2002)},
96  year   = 2003,
97  volume = 2646,
98  series = {Lecture Notes in Computer Science},
99  pages  = {200--219},
100  publisher = {Springer-Verlag},
101  doi    = {10.1007/3-540-39185-1_12}
102}
103
104Entry from Springerlink with obvious corrections.
105
106@article {springerlink:10.1007/s10817-009-9148-3,
107   author = {Blazy, Sandrine and Leroy, Xavier},
108   affiliation = {ENSIIE 1 square de la Résistance 91025 Evry cedex France},
109   title = {Mechanized Semantics for the {Clight} Subset of the {C} Language},
110   journal = {Journal of Automated Reasoning},
111   publisher = {Springer Netherlands},
112   issn = {0168-7433},
113   keyword = {Computer Science},
114   pages = {263-288},
115   volume = {43},
116   issue = {3},
117   url = {http://dx.doi.org/10.1007/s10817-009-9148-3},
118   doi = {10.1007/s10817-009-9148-3},
119   abstract = {This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, struct and union types, C loops and structured switch statements. Clight is the source language of the CompCert verified compiler. The formal semantics of Clight is a big-step operational semantics that observes both terminating and diverging executions and produces traces of input/output events. The formal semantics of Clight is mechanized using the Coq proof assistant. In addition to the semantics of Clight, this article describes its integration in the CompCert verified compiler and several ways by which the semantics was validated.},
120   year = {2009}
121}
122
123Entry made up
124
125@manual{coq83,
126  title = {The {Coq} Proof Assistant: Reference Manual, Version 8.3},
127  author = {The Coq Development Team},
128  organization = {INRIA},
129  year = 2010,
130  url = {http://coq.inria.fr/distrib/8.3pl2/refman/}
131}
132
133Entry made up
134
135@techreport{c99,
136  title = {Programming languages --- {C}},
137  key = {C99},
138  institution = {ISO},
139  year = {1999},
140  type = {International standard},
141  number = {ISO/IEC 9899:1999}
142}
143
144Entry made up.
145
146@article{compcert-mm08,
147  title = {Formal Verification of a {C}-like Memory Model and Its Uses for Verifying Program Transformations},
148  author = {Xavier Leroy and Sandrine Blazy},
149  journal = {Journal of Automated Reasoning},
150  year = 2008,
151  volume = 41,
152  number = 1,
153  pages = {1--31},
154  doi = {10.1007/s10817-008-9099-0}
155}
156
157Entry from ACM Digital Library with obvious correction.
158
159@inproceedings{Yang:2011:FUB:1993498.1993532,
160 author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
161 title = {Finding and understanding bugs in {C} compilers},
162 booktitle = {Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation},
163 series = {PLDI '11},
164 year = {2011},
165 isbn = {978-1-4503-0663-8},
166 location = {San Jose, California, USA},
167 pages = {283--294},
168 numpages = {12},
169 url = {http://doi.acm.org/10.1145/1993498.1993532},
170 doi = {http://doi.acm.org/10.1145/1993498.1993532},
171 acmid = {1993532},
172 publisher = {ACM},
173 address = {New York, NY, USA},
174 keywords = {automated testing, compiler defect, compiler testing, random program generation, random testing},
175}
176
177Entry made up.
178
179@inproceedings{cil02,
180  title  = {{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs},
181  author = {George C. Necula and Scott McPeak and Shree P. Rahul and Westley Weimer},
182  booktitle = {Compiler Construction: 11th International Conference (CC 2002)},
183  pages = {213--228},
184  year   = 2002,
185  editor = {R. Nigel Horspool},
186  volume = 2304,
187  series = {Lecture Notes in Computer Science},
188  publisher = {Springer},
189  doi = {10.1007/3-540-45937-5_16}
190}
191
192Entry made up.
193
194@manual{gccint4.4,
195  title = {{GNU} {Compiler} {Collection} {(GCC)} Internals},
196  note = {Version 4.4.3},
197  organization = {Free Software Foundation},
198  year = 2008
199}
200
201Entry from ACM Digital Library with corrected accent, capital.
202
203@inproceedings{Ellison:2012:EFS:2103656.2103719,
204 author = {Ellison, Chucky and Ro{\c s}u, Grigore},
205 title = {An executable formal semantics of {C} with applications},
206 booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
207 series = {POPL '12},
208 year = {2012},
209 isbn = {978-1-4503-1083-3},
210 location = {Philadelphia, PA, USA},
211 pages = {533--544},
212 numpages = {12},
213 url = {http://doi.acm.org/10.1145/2103656.2103719},
214 doi = {10.1145/2103656.2103719},
215 acmid = {2103719},
216 publisher = {ACM},
217 address = {New York, NY, USA},
218 keywords = {C, k, semantics},
219} 
220
221Entry from Springerlink. Note -> DOI.
222
223@article {springerlink:10.1007/BF00243133,
224   author = {Moore, J Strother},
225   title = {A mechanically verified language implementation},
226   journal = {Journal of Automated Reasoning},
227   publisher = {Springer Netherlands},
228   issn = {0168-7433},
229   keyword = {Computer Science},
230   pages = {461-492},
231   volume = {5},
232   issue = {4},
233   url = {http://dx.doi.org/10.1007/BF00243133},
234   doi = {10.1007/BF00243133},
235   abstract = {This paper briefly describes a programming language, its implementation on a microprocessor via a compiler and link-assembler, and the mechanically checked proof of the correctness of the implementation. The programming language, called Piton, is a high-level assembly language designed for verified applications and as the target language for high-level language compilers. It provides executeonly programs, recursive subroutine call and return, stack based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate results, and seven abstract data types including integers, data addresses, program addresses and subroutine names. Piton is formally specified by an interpreter written for it in the computational logic of Boyer and Moore. Piton has been implemented on the FM8502, a general purpose microprocessor whose gate-level design has been mechanically proved to implement its machine code interpreter. The FM8502 implementation of Piton is via a function in the Boyer-Moore logic which maps a Piton initial state into an FM8502 binary core image. The compiler and link-assembler are both defined as functions in the logic. The implementation requires approximately 36K bytes and 1400 lines of prettyprinted source code in the Pure Lisp-like syntax of the logic. The implementation has been mechanically proved correct. In particular, if a Piton state can be run to completion without error, then the final values of all the global data structures can be ascertained from an inspection of an FM8502 core image obtained by running the core image produced by the compiler and link-assembler. Thus, verified Piton programs running on FM8502 can be thought of as having been verified down to the gate level.},
236   year = {1989}
237}
238
239Entry from Springerlink, plus accent fix and doi changed to doi rather than
240note. And capital.
241
242@incollection {springerlink:10.1007/978-3-642-22863-6_17,
243   author = {Lochbihler, Andreas and Bulwahn, Lukas},
244   affiliation = {Karlsruher Institut f{\"{u}}r Technologie, Germany},
245   title = {Animating the Formalised Semantics of a {J}ava-Like Language},
246   booktitle = {Interactive Theorem Proving},
247   series = {Lecture Notes in Computer Science},
248   editor = {van Eekelen, Marko and Geuvers, Herman and Schmaltz, Julien and Wiedijk, Freek},
249   publisher = {Springer Berlin / Heidelberg},
250   isbn = {978-3-642-22862-9},
251   keyword = {Computer Science},
252   pages = {216-232},
253   volume = {6898},
254   url = {http://dx.doi.org/10.1007/978-3-642-22863-6_17},
255   doi = {10.1007/978-3-642-22863-6_17},
256   abstract = {Considerable effort has gone into the techniques of extracting executable code from formal specifications and animating them. We show how to apply these techniques to the large JinjaThreads formalisation. It models a substantial subset of multithreaded Java source and bytecode in Isabelle/HOL and focuses on proofs and modularity whereas code generation was of little concern in its design. Employing Isabelle’s code generation facilities, we obtain a verified Java interpreter that is sufficiently efficient for running small Java programs. To this end, we present refined implementations for common notions such as the reflexive transitive closure and Russell’s definite description operator. From our experience, we distill simple guidelines on how to develop future formalisations with executability in mind.},
257   year = {2011}
258}
259
260Entry from ACM Digital Library (I've only searched it for testing, not read it).
261
262@article{Klein:2006:MMJ:1146809.1146811,
263 author = {Klein, Gerwin and Nipkow, Tobias},
264 title = {A machine-checked model for a {Java}-like language, virtual machine, and compiler},
265 journal = {ACM Trans. Program. Lang. Syst.},
266 issue_date = {July 2006},
267 volume = {28},
268 number = {4},
269 month = jul,
270 year = {2006},
271 issn = {0164-0925},
272 pages = {619--695},
273 numpages = {77},
274 url = {http://doi.acm.org/10.1145/1146809.1146811},
275 doi = {10.1145/1146809.1146811},
276 acmid = {1146811},
277 publisher = {ACM},
278 address = {New York, NY, USA},
279 keywords = {Java, operational semantics, theorem proving},
280} 
281
282Entry from sciencedirect. Remove dodgy number and note.
283
284@article{Leinenbach200823,
285title = "Pervasive Compiler Verification – From Verified Programs to Verified Systems",
286journal = "Electronic Notes in Theoretical Computer Science",
287volume = "217",
288pages = "23 - 40",
289year = "2008",
290issn = "1571-0661",
291doi = "10.1016/j.entcs.2008.06.040",
292url = "http://www.sciencedirect.com/science/article/pii/S1571066108003836",
293author = "Dirk Leinenbach and Elena Petrova",
294keywords = "Compiler Verification",
295keywords = "Theorem Proving",
296keywords = "System Verification",
297keywords = "HOL",
298keywords = "Hoare Logic",
299abstract = "We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties from the C0 layer to the assembler and hardware layers. The compiler verification is split into two parts: the correctness of the compiling specification (which can be translated to executable ML code via Isabelle's code generator) and the correctness of a C0 implementation of this specification. We also sketch a method to solve the boot strap problem, i.e., how to obtain a trustworthy binary of the C0 compiler from its C0 implementation. Ultimately, this allows to prove pervasively the correctness of compiled C0 programs in the real system."
300}
301
302@article{Amadio2011175,
303  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
304                  B. Campbell and D. Mulligan and R. Pollack and
305                  Y. R{\'e}gis-Gianas and C. Sacerdoti Coen and I.
306                  Stark},
307  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
308                  Brian Campbell and Dominic Mulligan and Randy Pollack and
309                  Yann R{\'e}gis-Gianas and Claudio Sacerdoti Coen and Ian
310                  Stark},
311  title     = {Certified Complexity},
312  journal   = {Procedia Computer Science},
313  volume    = 7,
314  year      = 2011,
315  pages     = {175--177},
316  doi       = {10.1016/j.procs.2011.09.054}
317}
318
319Entry from springerlink with accent corrections.
320
321@incollection {springerlink:10.1007/978-3-642-11970-5_13,
322   author = {Rideau, Silvain and Leroy, Xavier},
323   affiliation = {{\'{E}}cole Normale Sup{\'{e}}rieure 45 rue d’Ulm 75005 Paris France},
324   title = {Validating Register Allocation and Spilling},
325   booktitle = {Compiler Construction},
326   series = {Lecture Notes in Computer Science},
327   editor = {Gupta, Rajiv},
328   publisher = {Springer Berlin / Heidelberg},
329   isbn = {978-3-642-11969-9},
330   keyword = {Computer Science},
331   pages = {224-243},
332   volume = {6011},
333   url = {http://dx.doi.org/10.1007/978-3-642-11970-5_13},
334   doi = {10.1007/978-3-642-11970-5_13},
335   abstract = {Following the translation validation approach to high-assurance compilation, we describe a new algorithm for validating a posteriori the results of a run of register allocation. The algorithm is based on backward dataflow inference of equations between variables, registers and stack locations, and can cope with sophisticated forms of spilling and live range splitting, as well as many architectural irregularities such as overlapping registers. The soundness of the algorithm was mechanically proved using the Coq proof assistant.},
336   year = {2010}
337}
338
339Entry from springerlink with accent and title corrections.
340
341@incollection {springerlink:10.1007/978-3-642-28869-2_20,
342   author = {Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and Leroy, Xavier},
343   affiliation = {{\'{E}}cole Normale Sup{\'{e}}rieure, France},
344   title = {Validating {LR(1)} Parsers},
345   booktitle = {Programming Languages and Systems},
346   series = {Lecture Notes in Computer Science},
347   editor = {Seidl, Helmut},
348   publisher = {Springer Berlin / Heidelberg},
349   isbn = {978-3-642-28868-5},
350   keyword = {Computer Science},
351   pages = {397-416},
352   volume = {7211},
353   url = {http://dx.doi.org/10.1007/978-3-642-28869-2_20},
354   doi = {10.1007/978-3-642-28869-2_20},
355   abstract = {An LR (1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar and an automaton , checks that and agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct . The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.},
356   year = {2012}
357}
358
359
360@techreport{EDI-INF-RR-1412,
361  author = {Brian Campbell and Randy Pollack},
362  title = {Executable Formal Semantics of {C}},
363  institution = {School of Informatics, University of Edinburgh},
364  year = 2010,
365  number = {EDI-INF-RR-1412}
366}
367
368Entry from springerlink, with obvious capitalisation correction and note -> doi.
369
370@incollection {springerlink:10.1007/3-540-49519-3_22,
371   author = {Strother Moore, J.},
372   affiliation = {The University of Texas at Austin Department of Computer Sciences Austin TX 78712-1188},
373   title = {Symbolic Simulation: An {ACL2} Approach},
374   booktitle = {Formal Methods in Computer-Aided Design},
375   series = {Lecture Notes in Computer Science},
376   editor = {Gopalakrishnan, Ganesh and Windley, Phillip},
377   publisher = {Springer Berlin / Heidelberg},
378   isbn = {978-3-540-65191-8},
379   keyword = {Computer Science},
380   pages = {530-530},
381   volume = {1522},
382   url = {http://dx.doi.org/10.1007/3-540-49519-3_22},
383   doi = {10.1007/3-540-49519-3_22},
384   abstract = {Executable formal specification can allow engineers to test (or simulate ) the specified system on concrete data before the system is implemented. This is beginning to gain acceptance and is just the formal analogue of the standard practice of building simulators in conventional programming languages such as C. A largely unexplored but potentially very useful next step is symbolic simulation , the “execution” of the formal specification on indeterminant data. With the right interface, this need not require much additional training of the engineers using the tool. It allows many tests to be collapsed into one. Furthermore, it familiarizes the working engineer with the abstractions and notation used in the design, thus allowing team members to speak clearly to one another. We illustrate these ideas with a formal specification of a simple computing machine in ACL2. We sketch some requirements on the interface, which we call a symbolic spreadsheet .},
385   year = {1998}
386}
387
388
389Entry from springerlink. Note -> doi.
390
391@incollection {springerlink:10.1007/978-3-642-03359-9_11,
392   author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
393   affiliation = {Technische Universitüt München Institut für Informatik Boltzmannstraße 3 85748 Garching Germany},
394   title = {Turning Inductive into Equational Specifications},
395   booktitle = {Theorem Proving in Higher Order Logics},
396   series = {Lecture Notes in Computer Science},
397   editor = {Berghofer, Stefan and Nipkow, Tobias and Urban, Christian and Wenzel, Makarius},
398   publisher = {Springer Berlin / Heidelberg},
399   isbn = {978-3-642-03358-2},
400   keyword = {Computer Science},
401   pages = {131-146},
402   volume = {5674},
403   url = {http://dx.doi.org/10.1007/978-3-642-03359-9_11},
404   doi = {10.1007/978-3-642-03359-9_11},
405   abstract = {Inductively defined predicates are frequently used in formal specifications. Using the theorem prover Isabelle , we describe an approach to turn a class of systems of inductively defined predicates into a system of equations using data flow analysis; the translation is carried out inside the logic and resulting equations can be turned into functional program code in SML , OCaml or Haskell using the existing code generator of Isabelle . Thus we extend the scope of code generation in Isabelle from functional to functional-logic programs while leaving the trusted foundations of code generation itself intact.},
406   year = {2009}
407}
Note: See TracBrowser for help on using the repository browser.