source: LTS/paper/ccexec.bib @ 3594

Last change on this file since 3594 was 3594, checked in by sacerdot, 3 years ago

Old stuff never committed is now committed

File size: 25.9 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
144@techreport{report,
145  title = {{CerCo Report n. D4.4, Back-end Correctness Proof}},
146  author = {Jaap Boender and Dominic P. Mulligan and Mauro Piccolo and
147Claudio Sacerdoti Coen and Paolo Tranquilli},
148  key = {CerCo D4.4},
149  institution = {University of Bologna},
150  year = {2013},
151  type = {Technical Report of the EU Project CerCo},
152  url = {http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_4.pdf},
153}
154
155
156Entry made up.
157
158@article{compcert1,
159  author = {Xavier Leroy},
160  title = {Formal verification of a realistic compiler},
161  journal = {Communications of the ACM},
162  year = 2009,
163  volume = 52,
164  number = 7,
165  pages = {107--115},
166  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
167  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
168  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
169  pubkind = {journal-int-mono},
170  abstract = {This paper reports on the development and formal verification (proof
171of semantic preservation) of CompCert, a compiler from Clight (a
172large subset of the C programming language) to PowerPC assembly code,
173using the Coq proof assistant both for programming the compiler and
174for proving its correctness.  Such a verified compiler is useful in
175the context of critical software and its formal verification: the
176verification of the compiler guarantees that the safety properties
177proved on the source code hold for the executable compiled code as
178well.}
179}
180
181@article{compcert2,
182  title = {Formal Verification of a {C}-like Memory Model and Its Uses for Verifying Program Transformations},
183  author = {Xavier Leroy and Sandrine Blazy},
184  journal = {Journal of Automated Reasoning},
185  year = 2008,
186  volume = 41,
187  number = 1,
188  pages = {1--31},
189  doi = {10.1007/s10817-008-9099-0}
190}
191
192@article{compcert3,
193  author = {Xavier Leroy},
194  title = {A formally verified compiler back-end},
195  journal = {Journal of Automated Reasoning},
196  volume = 43,
197  number = 4,
198  pages = {363--446},
199  year = 2009,
200  url = {http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf},
201  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
202  hal = {http://hal.inria.fr/inria-00360768/},
203  pubkind = {journal-int-mono}
204}
205
206
207Entry from ACM Digital Library with obvious correction.
208
209@inproceedings{Yang:2011:FUB:1993498.1993532,
210 author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
211 title = {Finding and understanding bugs in {C} compilers},
212 booktitle = {Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation},
213 series = {PLDI '11},
214 year = {2011},
215 isbn = {978-1-4503-0663-8},
216 location = {San Jose, California, USA},
217 pages = {283--294},
218 numpages = {12},
219 url = {http://doi.acm.org/10.1145/1993498.1993532},
220 doi = {http://doi.acm.org/10.1145/1993498.1993532},
221 acmid = {1993532},
222 publisher = {ACM},
223 address = {New York, NY, USA},
224 keywords = {automated testing, compiler defect, compiler testing, random program generation, random testing},
225}
226
227Entry made up.
228
229@inproceedings{cil02,
230  title  = {{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs},
231  author = {George C. Necula and Scott McPeak and Shree P. Rahul and Westley Weimer},
232  booktitle = {Compiler Construction: 11th International Conference (CC 2002)},
233  pages = {213--228},
234  year   = 2002,
235  editor = {R. Nigel Horspool},
236  volume = 2304,
237  series = {Lecture Notes in Computer Science},
238  publisher = {Springer},
239  doi = {10.1007/3-540-45937-5_16}
240}
241
242Entry made up.
243
244@manual{gccint4.4,
245  title = {{GNU} {Compiler} {Collection} {(GCC)} Internals},
246  note = {Version 4.4.3},
247  organization = {Free Software Foundation},
248  year = 2008
249}
250
251Entry from ACM Digital Library with corrected accent, capital.
252
253@inproceedings{Ellison:2012:EFS:2103656.2103719,
254 author = {Ellison, Chucky and Ro{\c s}u, Grigore},
255 title = {An executable formal semantics of {C} with applications},
256 booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
257 series = {POPL '12},
258 year = {2012},
259 isbn = {978-1-4503-1083-3},
260 location = {Philadelphia, PA, USA},
261 pages = {533--544},
262 numpages = {12},
263 url = {http://doi.acm.org/10.1145/2103656.2103719},
264 doi = {10.1145/2103656.2103719},
265 acmid = {2103719},
266 publisher = {ACM},
267 address = {New York, NY, USA},
268 keywords = {C, k, semantics},
269} 
270
271Entry from Springerlink. Note -> DOI.
272
273@Inproceedings{clockfunctions,
274  author    = "S. Ray and J S. Moore",
275  title     = "{Proof Styles in Operational Semantics}",
276  editor    = "A. J. Hu and A. K. Martin",
277  booktitle = "{Proceedings of the $5$th International Conference on
278                Formal Methods in Computer-Aided Design (FMCAD 2004)}",
279  series    = "{LNCS}",
280  volume    = "3312",
281  address   = "{Austin, TX}",
282  publisher = "{Springer}",
283  month     = nov,
284  pages     = "67-81",
285  year      = 2004
286}
287
288@article {piton,
289   author = {Moore, J Strother},
290   title = {A mechanically verified language implementation},
291   journal = {Journal of Automated Reasoning},
292   publisher = {Springer Netherlands},
293   issn = {0168-7433},
294   keyword = {Computer Science},
295   pages = {461-492},
296   volume = {5},
297   issue = {4},
298   url = {http://dx.doi.org/10.1007/BF00243133},
299   doi = {10.1007/BF00243133},
300   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.},
301   year = {1989}
302}
303
304Entry from Springerlink, plus accent fix and doi changed to doi rather than
305note. And capital.
306
307@incollection {springerlink:10.1007/978-3-642-22863-6_17,
308   author = {Lochbihler, Andreas and Bulwahn, Lukas},
309   affiliation = {Karlsruher Institut f{\"{u}}r Technologie, Germany},
310   title = {Animating the Formalised Semantics of a {J}ava-Like Language},
311   booktitle = {Interactive Theorem Proving},
312   series = {Lecture Notes in Computer Science},
313   editor = {van Eekelen, Marko and Geuvers, Herman and Schmaltz, Julien and Wiedijk, Freek},
314   publisher = {Springer Berlin / Heidelberg},
315   isbn = {978-3-642-22862-9},
316   keyword = {Computer Science},
317   pages = {216-232},
318   volume = {6898},
319   url = {http://dx.doi.org/10.1007/978-3-642-22863-6_17},
320   doi = {10.1007/978-3-642-22863-6_17},
321   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.},
322   year = {2011}
323}
324
325Entry from ACM Digital Library (I've only searched it for testing, not read it).
326
327@article{Klein:2006:MMJ:1146809.1146811,
328 author = {Klein, Gerwin and Nipkow, Tobias},
329 title = {A machine-checked model for a {Java}-like language, virtual machine, and compiler},
330 journal = {ACM Trans. Program. Lang. Syst.},
331 issue_date = {July 2006},
332 volume = {28},
333 number = {4},
334 month = jul,
335 year = {2006},
336 issn = {0164-0925},
337 pages = {619--695},
338 numpages = {77},
339 url = {http://doi.acm.org/10.1145/1146809.1146811},
340 doi = {10.1145/1146809.1146811},
341 acmid = {1146811},
342 publisher = {ACM},
343 address = {New York, NY, USA},
344 keywords = {Java, operational semantics, theorem proving},
345} 
346
347Entry from sciencedirect. Remove dodgy number and note.
348
349@article{Leinenbach200823,
350title = "Pervasive Compiler Verification – From Verified Programs to Verified Systems",
351journal = "Electronic Notes in Theoretical Computer Science",
352volume = "217",
353pages = "23 - 40",
354year = "2008",
355issn = "1571-0661",
356doi = "10.1016/j.entcs.2008.06.040",
357url = "http://www.sciencedirect.com/science/article/pii/S1571066108003836",
358author = "Dirk Leinenbach and Elena Petrova",
359keywords = "Compiler Verification",
360keywords = "Theorem Proving",
361keywords = "System Verification",
362keywords = "HOL",
363keywords = "Hoare Logic",
364abstract = "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."
365}
366
367@book{while,
368 author = {Nielson, Flemming and Nielson, Hanne R. and Hankin, Chris},
369 title = {Principles of Program Analysis},
370 year = {1999},
371 isbn = {3540654100},
372 publisher = {Springer-Verlag New York, Inc.},
373 address = {Secaucus, NJ, USA},
374}
375
376@incollection{easylabelling,
377year={2012},
378isbn={978-3-642-32468-0},
379booktitle={Formal Methods for Industrial Critical Systems},
380volume={7437},
381series={Lecture Notes in Computer Science},
382editor={Stoelinga, Mariëlle and Pinger, Ralf},
383doi={10.1007/978-3-642-32469-7_3},
384title={Certifying and Reasoning on Cost Annotations in {C} Programs},
385url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
386publisher={Springer Berlin Heidelberg},
387author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann},
388pages={32-46}
389}
390
391@incollection{functionallabelling,
392year={2012},
393isbn={978-3-642-32494-9},
394booktitle={Foundational and Practical Aspects of Resource Analysis},
395volume={7177},
396series={Lecture Notes in Computer Science},
397editor={Peña, Ricardo and Eekelen, Marko and Shkaravska, Olha},
398doi={10.1007/978-3-642-32495-6_5},
399title={Certifying and Reasoning on Cost Annotations of Functional Programs},
400url={http://dx.doi.org/10.1007/978-3-642-32495-6_5},
401publisher={Springer Berlin Heidelberg},
402author={Amadio, RobertoM. and R\'egis-Gianas, Yann},
403pages={72-89},
404note={Extended version to appear in Higher Order and Symbolic Computation, 2013}
405}
406
407@inproceedings{framaC,
408 author = {Cuoq, Pascal and Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
409 title = {Frama-C: a software analysis perspective},
410 booktitle = {Proceedings of the 10th international conference on Software Engineering and Formal Methods},
411 series = {SEFM'12},
412 year = {2012},
413 isbn = {978-3-642-33825-0},
414 location = {Thessaloniki, Greece},
415 pages = {233--247},
416 numpages = {15},
417 url = {http://dx.doi.org/10.1007/978-3-642-33826-7_16},
418 doi = {10.1007/978-3-642-33826-7_16},
419 acmid = {2404250},
420 publisher = {Springer-Verlag},
421 address = {Berlin, Heidelberg},
422} 
423
424@article{cerco,
425  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
426                  B. Campbell and D. Mulligan and R. Pollack and
427                  Y. R{\'e}gis-Gianas and C. {Sacerdoti Coen} and I.
428                  Stark},
429  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
430                  Brian Campbell and Dominic Mulligan and Randy Pollack and
431                  Yann R{\'e}gis-Gianas and Claudio {Sacerdoti Coen} and Ian
432                  Stark},
433  title     = {Certified Complexity},
434  journal   = {Procedia Computer Science},
435  volume    = 7,
436  year      = 2011,
437  pages     = {175--177},
438  doi       = {10.1016/j.procs.2011.09.054}
439}
440
441Entry from springerlink with accent corrections.
442
443@incollection {springerlink:10.1007/978-3-642-11970-5_13,
444   author = {Rideau, Silvain and Leroy, Xavier},
445   affiliation = {{\'{E}}cole Normale Sup{\'{e}}rieure 45 rue d’Ulm 75005 Paris France},
446   title = {Validating Register Allocation and Spilling},
447   booktitle = {Compiler Construction},
448   series = {Lecture Notes in Computer Science},
449   editor = {Gupta, Rajiv},
450   publisher = {Springer Berlin / Heidelberg},
451   isbn = {978-3-642-11969-9},
452   keyword = {Computer Science},
453   pages = {224-243},
454   volume = {6011},
455   url = {http://dx.doi.org/10.1007/978-3-642-11970-5_13},
456   doi = {10.1007/978-3-642-11970-5_13},
457   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.},
458   year = {2010}
459}
460
461Entry from springerlink with accent and title corrections.
462
463@incollection {springerlink:10.1007/978-3-642-28869-2_20,
464   author = {Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and Leroy, Xavier},
465   affiliation = {{\'{E}}cole Normale Sup{\'{e}}rieure, France},
466   title = {Validating {LR(1)} Parsers},
467   booktitle = {Programming Languages and Systems},
468   series = {Lecture Notes in Computer Science},
469   editor = {Seidl, Helmut},
470   publisher = {Springer Berlin / Heidelberg},
471   isbn = {978-3-642-28868-5},
472   keyword = {Computer Science},
473   pages = {397-416},
474   volume = {7211},
475   url = {http://dx.doi.org/10.1007/978-3-642-28869-2_20},
476   doi = {10.1007/978-3-642-28869-2_20},
477   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.},
478   year = {2012}
479}
480
481
482@misc{fopara,
483  author = {R.~M. Amadio and N.~Ayache and F.~Bobot and J.~P. Boender and B.~Campbell and I.~Garnier and A.~Madet and J.~McKinna and D.~P. Mulligan and M.~Piccolo and R.~Pollack and Y.~R\'egis-Gianas and C.~Sacerdoti Coen and I.~Stark and P.~Tranquilli},
484  title = {Certified Complexity (CerCo)},
485  note = {Submitted to FOPARA 2013},
486  year = 2013
487}
488
489@techreport{EDI-INF-RR-1412,
490  author = {Brian Campbell and Randy Pollack},
491  title = {Executable Formal Semantics of {C}},
492  institution = {School of Informatics, University of Edinburgh},
493  year = 2010,
494  number = {EDI-INF-RR-1412}
495}
496
497Entry from springerlink, with obvious capitalisation correction and note -> doi.
498
499@incollection {springerlink:10.1007/3-540-49519-3_22,
500   author = {Strother Moore, J.},
501   affiliation = {The University of Texas at Austin Department of Computer Sciences Austin TX 78712-1188},
502   title = {Symbolic Simulation: An {ACL2} Approach},
503   booktitle = {Formal Methods in Computer-Aided Design},
504   series = {Lecture Notes in Computer Science},
505   editor = {Gopalakrishnan, Ganesh and Windley, Phillip},
506   publisher = {Springer Berlin / Heidelberg},
507   isbn = {978-3-540-65191-8},
508   keyword = {Computer Science},
509   pages = {530-530},
510   volume = {1522},
511   url = {http://dx.doi.org/10.1007/3-540-49519-3_22},
512   doi = {10.1007/3-540-49519-3_22},
513   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 .},
514   year = {1998}
515}
516
517
518Entry from springerlink. Note -> doi.
519
520@incollection {springerlink:10.1007/978-3-642-03359-9_11,
521   author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
522   affiliation = {Technische Universitüt München Institut für Informatik Boltzmannstraße 3 85748 Garching Germany},
523   title = {Turning Inductive into Equational Specifications},
524   booktitle = {Theorem Proving in Higher Order Logics},
525   series = {Lecture Notes in Computer Science},
526   editor = {Berghofer, Stefan and Nipkow, Tobias and Urban, Christian and Wenzel, Makarius},
527   publisher = {Springer Berlin / Heidelberg},
528   isbn = {978-3-642-03358-2},
529   keyword = {Computer Science},
530   pages = {131-146},
531   volume = {5674},
532   url = {http://dx.doi.org/10.1007/978-3-642-03359-9_11},
533   doi = {10.1007/978-3-642-03359-9_11},
534   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.},
535   year = {2009}
536}
537
538@inproceedings{loopoptimizations,
539  author    = {Paolo Tranquilli},
540  title     = {Indexed Labels for Loop Iteration Dependent Costs},
541  booktitle = {Proceedings 11th International Workshop on Quantitative
542               Aspects of Programming Languages and Systems, QAPL 2013},
543  series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
544  year      = {2013},
545  pages     = {19-33},
546  ee        = {http://dx.doi.org/10.4204/EPTCS.117.2},
547  bibsource = {DBLP, http://dblp.uni-trier.de}
548}
549
550@incollection{matita1,
551year={2011},
552isbn={978-3-642-22437-9},
553booktitle={Automated Deduction – CADE-23},
554volume={6803},
555series={Lecture Notes in Computer Science},
556editor={Bjørner, Nikolaj and Sofronie-Stokkermans, Viorica},
557doi={10.1007/978-3-642-22438-6_7},
558title={The Matita Interactive Theorem Prover},
559url={http://dx.doi.org/10.1007/978-3-642-22438-6_7},
560publisher={Springer Berlin Heidelberg},
561author={Asperti, Andrea and Ricciotti, Wilmer and Sacerdoti Coen, Claudio and Tassi, Enrico},
562pages={64-69}
563}
564
565@article{matita2,
566year={2007},
567issn={0168-7433},
568journal={Journal of Automated Reasoning},
569volume={39},
570issue={2},
571doi={10.1007/s10817-007-9070-5},
572title={User Interaction with the Matita Proof Assistant},
573url={http://dx.doi.org/10.1007/s10817-007-9070-5},
574publisher={Springer Netherlands},
575keywords={Proof assistant; Interactive theorem proving; Digital libraries; XML; Mathematical knowledge management; Authoring},
576author={Asperti, Andrea and Sacerdoti Coen, Claudio and Tassi, Enrico and Zacchiroli, Stefano},
577pages={109-139},
578language={English}
579}
Note: See TracBrowser for help on using the repository browser.