1

Gerwin Klein , Tobias Nipkow, Verified bytecode verifiers, Theoretical Computer Science, v.298 n.3, p.583-626, 11 April 2003  [doi>10.1016/S0304-3975(02)00869-1]

2

S. Berghofer, and M. Strecker; Extracting a formally verified, fully executable compiler from a proof assistant; In Proceedings of Compiler Optimization meet Compiler Verification; 2003.

3

Sabine Glesner, and Jan Olaf Blech; Classifying and Formally Verifying Integer Constant Folding; In Proceedings of Compiler Optimization meet Compiler Verification; 2003.

4

Thomas Genet, Thomas Jensen, Vikash Kodati, and David Pichardie; A Java Card CAP Converter in PVS; In Proceedings of Compiler Optimization meet Compiler Verification; 2003.

5

Gerhard Goos; Compiler Verification and Compiler Architecture; Electronic Notes in Theoretical Computer Science, Volume 65, Issue 2, April 2002.

6

Lenore Zuck, Amir Pnueli, Yi Fang and Benjamin Goldberg; VOC: A Translation Validator for Optimizing Compilers; Electronic Notes in Theoretical Computer Science, Volume 65, Issue 2, April 2002.

7

Sabine Glesner, Rubino Geiß and Boris Boesler; Verified Code Generation for Embedded Systems; Electronic Notes in Theoretical Computer Science, Volume 65, Issue 2, April 2002.

8

Carl Christian Frederiksen; Correctness of Classical Compiler Optimizations using CTL; Electronic Notes in Theoretical Computer Science, Volume 65, Issue 2, April 2002.

9

Thi Viet Nga Nguyen and Francois Irigoin; Alias verification for Fortran code optimization; Electronic Notes in Theoretical Computer Science, Volume 65, Issue 2, April 2002.

10

K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor and Gerda Janssens; Geometric Model Checking: An Automatic Verification Technique for Loop and Data Reuse Transformations; Electronic Notes in Theoretical Computer Science, Volume 65, Issue 2, April 2002.

11

Clara Jaramillo, Rajiv Gupta and Mary Lou Soffa; Debugging and Testing Optimizers through Comparison Checking; Electronic Notes in Theoretical Computer Science, Volume 65, Issue 2, April 2002.

12

Wolfgang Goerigk; Towards Acceptability of Optimizations: An Extended View of Compiler Correctness; Electronic Notes in Theoretical Computer Science, Volume 65, Issue 2, April 2002.

13

Martin Strecker, Formal Verification of a Java Compiler in Isabelle, Proceedings of the 18th International Conference on Automated Deduction, p.63-77, July 27-30, 2002

14

Amir Pnueli , Yoav Rodeh , Ofer Strichmann , Michael Siegel, The small model property: how small can it be?, Information and Computation, v.178 n.1, p.279-293, October 10, 2002  [doi>10.1016/S0890-5401(02)93175-5]

15

L. Zuck, A. Pnueli, Y. Fang, B. Goldberg, and Y. Hu; Translation and run-time validation of optimized code; In 2nd Workshop on Runtime Verification, volume 70(4) of Electronic Notes in Theoretical Computer Science, pages 180--201, Copenhagen, Denmark, July 2002.

16

Raya Leviathan , Amir Pnueli, Validating software pipelining optimizations, Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems, October 08-11, 2002, Grenoble, France  [doi>10.1145/581630.581676]

17

Axel Dold , Vincent Vialard, A Mechanically Verified Compiling Specification for a Lisp Compiler, Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science, p.144-155, December 13-15, 2001

18

A. Dold, and V. Vialard; A Mechanically Verified Bootstrap Compiler; Proceedings of Kolloquium Programmiersprachen und Grundlagen der Programmierung Technical report AIB-2001--11, RWTH Aachen, Department of Computer Science, December 2001.

19

Wolfgang Goerigk, and Hans Langmaack; Compiler Implementation Verification and Trojan Horses; Verifix technical report, 2001.

20

L. Zuck , A. Pnueli , R. Leviathan, Validation of Optimizing Compilers,, Weizmann Science Press of Israel, Jerusalem, Israel, 2001

21

Wolfgang Goerigk, Compiler verification revisited, Computer-Aided reasoning: ACL2 case studies, Kluwer Academic Publishers, Norwell, MA, 2000

22

George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada

23

A. Pnueli, L. Zuck, and P. Pandya; Translation validation of optimizing compilers by computational induction; Technical report, Weizmann Institute of Science; 2000.

24

L. Zuck , A. Pnueli , R. Leviathan, Validation of Optimizing Compilers,, Weizmann Science Press of Israel, Jerusalem, Israel, 2001

25

Gerhard Goos , Wolf Zimmermann, Verifying Compilers and ASMs, Proceedings of the International Workshop on Abstract State Machines, Theory and Applications, p.177-202, March 19-24, 2000

26

W. Goerigk, and H. Langmaack; Compiler Implementation Verification and Trojan Horses; In D. Bainov (ed.), Proceedings of the 9th International Colloquium on Numerical Analysis and Computer Sciences with Applications, Plovdiv, Bulgaria, 2000.

27

W. Goerigk; Proving Preservation of Partial Correctness with ACL2: A Mechanical Compiler Source Level Correctness Proof. ; ACL2 Workshop 2000, Austin, Tx. U.S.A, October 2000.

28

T. Gaul, W. Zimmermann, and W. Goerigk; Practical Construction of Correct Compiler Implementations by Run-time Result Verification;In Proceedings of SCI'2000, International Conference on Information Systems Analysis and Synthesis, Orlando, Florida, 2000

29

Markus Müller-Olm , Andreas Wolf, On the Translation of Procedures to Finite Machines, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.290-304, April 02, 2000

30

Robert van Engelen , David B. Whalley , Xin Yuan, Automatic Validation of Code-Improving Transformations, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.206-210, June 18, 2000

31

Gerhard Goos , Wolf Zimmermann, Verification of Compilers, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), p.201-230, January 1999

32

Wolfgang Naraschewski , Tobias Nipkow, Type Inference Verified: Algorithm W in Isabelle/HOL, Journal of Automated Reasoning, v.23 n.3, p.299-318, November 1999  [doi>10.1023/A:1006277616879]

33

A. Wolf; An Exercise in Compiler Verification Revisited -- Preserving Partial Correctness; 02/99 Verifix Report CAU 6.1; 1999.

34

V. Vialard; Local Verification of Parametrized Compilation Rules in a Limited Resource Environment; 01/99 Verifix Report ULM 22.1; 1999.

35

Axel Dold , Vincent Vialard, Formal Verification of a Compiler Back-End Generic Checker Program, Proceedings of the Third International Andrei Ershov Memorial Conference on Perspectives of System Informatics, p.470-480, July 06-09, 1999

36

Th. Gaul, W. Zimmermann, and W. Goerigk; Construction of Verified Software Systems with Program-Checking: An Application To Compiler Back-Ends; In A. Pnueli und P. Traverso (eds.), Proc. FLoC'99 International Workshop on "Runtime Result Verification", Trento, Italy, 1999.

37

Andreas Heberle , Thilo Gaul , Wolfgang Goerigk , Gerhard Goos , Wolf Zimmermann, Construction of Verified Compiler Front-Ends with Program-Checking, Proceedings of the Third International Andrei Ershov Memorial Conference on Perspectives of System Informatics, p.481-492, July 06-09, 1999

38

Markus Müller-Olm , Andreas Wolf, On Excusable and Inexcusable Failures, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, p.1107-1127, September 20-24, 1999

39

Amir Pnueli , Ofer Shtrichman , Michael Siegel, Translation Validation: From SIGNAL to C, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), p.231-255, January 1999

40

Wolf Zimmermann, Andreas Heberle, and Wolfgang Goerigk.; The Verifix Approach Towards the Construction of Correct Compilers; Verifix Technical Report 1999.

41

T. Gaul, M. Spott, M. Riedmiller, and R. Schohknecht; Fuzzy-Neuro-Controlled Verified Instruction Scheduler; Conference Proceedings of NAFIPS'99, New York; 1999.

42

Tobias Nipkow, Verified Lexical Analysis, Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, p.1-15, September 27-October 01, 1998

43

U. Hoffmann; Correct Implementation of Compiler Programs; In R. Berghammer and F. Simon (eds.) Workshop on Programming Languages and Fundamentals of Programming, Avendorf, September 1998

44

U. Hoffmann; Compiler Implementation Verification through Rigorous Syntactical Code Inspection; Ph.D. Thesis, Technical Faculty, CAU Kiel, 1998.

45

A. Heberle, and W. Löwe; On ASM-Based Specification of Programming Language Semantics and Reusable Correct Compilations; Proceedings of the 5th International Workshop on Abstract State Machines; 1998

46

Wolfgang Goerigk , Ulrich Hoffmann, Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct, Proceedings of the International Workshop on Current Trends in Applied Formal Method: Applied Formal Methods, p.122-136, October 07-09, 1998

47

W. Goerigk and F. Simon; Towards Rigorous Compiler Implementation Verification; In: Julian Padget (ed.), Proceedings of the VIM Spring and Winter Workshops, Lecture Notes in Computer Science, Berlin, Heidelberg, New York, 1998. Springer Verlag.; 1998.

48

A.Dold; Correct Compiler Construction in PVS; Verifix Report, ULM 20.1; 1998.

49

David W. J. Stringer-Calvert; Mechanical Verification of Compiler Correctness; Department of Computer Science, University of York; March, 1998.

50

Amir Pnueli , Ofer Shtrichman , Michael Siegel, Translation Validation for Synchronous Languages, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.235-246, July 13-17, 1998

51

Amir Pnueli , Michael Siegel , Eli Singerman, Translation Validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.151-166, March 28-April 04, 1998

52

Ofer Strichman, A. Pnueli and M. Siegel; The Code Validation Tool (CVT) - Automatic Verification of a Compilation Process; in the intl. Journal of Software Tools for Technology Transfer (STTT), Vol 2(2), pp 192--201, 1998.

53

Ofer Strichman, A. Pnueli and M. Siegel; The Code Validation Tool (CVT) - Automatic verification of code generated from synchronous languages; Proceedings of the international. workshop of Software Tools for Technology Transfer (STTT'98), 1998.

54

Amir Pnueli , Ofer Shtrichman , Michael Siegel, Translation Validation for Synchronous Languages, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.235-246, July 13-17, 1998

55

A. Dold, T. Gaul, W. Zimmermann; Mechanized Verification of Compiler Back-Ends; Proceedings of the International Workshop on Software Tools for Technology Transfer STTT '98; 1998.

56

Markus Müller-Olm; Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction.; Lecture Notes in Computer Science (LNCS), Vol. 1283. Springer-Verlag, Heidelberg, Germany.; 1997.

57

Th. Gaul, G. Goos, A. Heberle, W. Zimmermann, and W. Goerigk; An Architecture for Verified Compiler Construction.; In: Joint Modular Languages Conference JMLC'97, Linz, Austria, March 1997.

58

W. Goerigk; Towards Rigorous Compiler Implementation Verification; In: R. Berghammer und F. Simon (eds.), Proc. of the 1997 Workshop on Programming Languages and Fundamentals of Programming, S.\ 118--126, Avendorf, Germany, November 1997.

59

Wolfgang Goerigk, Ulrich Hoffmann, und Hans Langmaack; Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct. Verifix-Arbeitsbericht Verifix/CAU-Ulm/2.6, CAU Kiel, January 1997.

60

T. Gaul, and W. Zimmermann; On the Construction of Correct Compiler Back-Ends: An ASM Approach; Journal of Universal Computer Science, 1997.

61

Axel Dold , Friedrich W. von Henke , Holger Pfeifer , Harald Rueß, Formal Verification of Transformations for Peephole Optimization, Proceedings of the 4th International Symposium of Formal Methods Europe on Industrial Applications and Strengthened Foundations of Formal Methods, p.459-472, September 15-19, 1997

62

Hans Langmaack, Contribution to Goodenough's and Gerhart's Theory of Software Testing and Verification: Relation between Strong Compiler Test and Compiler Implementation Verification, Foundations of Computer Science: Potential - Theory - Cognition, to Wilfried Brauer on the occasion of his sixtieth birthday, p.321-335, January 1997

63

Augusto Sampaio; An Algebraic Approach to Compiler Design; World Scientific; 1997.

64

W. M. Farmer and J. D. Ramsdell; A verified compiler for Multithreaded PreSchemeTechnical Report, 180 pp., The MITRE Corporation, 1996.

65

E. Boerger, and I. Durdanovic; Correctness of compiling Occam to Transputer Code; Computer Journal, vol 39, no 1, pages 52--92, 1996.

66

M. Marcus , Amir Pnueli, Using Ghost Variables to Prove Refinement, Proceedings of the 5th International Conference on Algebraic Methodology and Software Technology, p.226-240, July 01-05, 1996

67

A. Heberle, W. Zimmermann, and G. Goos Specification and Verification of Compiler Front end Tasks: Semantic Analysis; 04/96 Verifix Report UKA 7; 1996.

68

W. Goerigk, A. Dold, Th. Gaul, G. Goos, A. Heberle, F. W. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann; Compiler Correctness and Implementation Verification: The Verifix Approach; In P. Fritzson (ed.), Proceedings of the Poster Session of CC '96 - International Conference on Compiler Construction, S. 65--73, IDA Technical Report LiTH-IDA-R-96-12, Linkøping, Sweden, 1996.

69

A.Dold; Formalization and Verification of Code Generation Rules; 09/96 Verifix Report ULM 16.1; 1996.

70

Joshua D. Guttman , John D. Ramsdell , Vipin Swarup, The VLISP verified Scheme system, Lisp and Symbolic Computation, v.8 n.1-2, p.33-110, March 1995  [doi>10.1007/BF01128407]

71

E. Boerger, and I. Durdanovic; Correctness of compiling Occam to Transputer Code, in Evolving Algebra Mini Course, BRICS, Basic Research in Computer Science, Notes Series NS-95-4, ISSN 0909--3206, pages 153--194, University of Aarhus, 1995.

72

Markus Müller-Olm; An Exercise in Compiler Verification.; Proceedings of the 8th Workshop of the RWTH Aachen, CAU Kiel, and TU München on "Programming Languages and Foundations of Programming", Adalbert-Stifter-Haus, Altreichenau (Germany). MIP-Bericht (9519), pp. 48--54. Fakultät für Mathematik und Informatik, Universität Passau, 1995.

73

W. Goerigk; On the Correctness of Compilers and Compiler Implementations.; In Workshop "Alternative Konzepte für Sprachen und Rechner", Bad Honnef, 1995.

74

Markus Müller-Olm; Modular Compiler Verification. Christian-Albrechts-Universität, Kiel, Kiel MMO 15/1, Germany. ProCoS Technical Report. August 1995,

75

Manfred Broy , Ursula Hinkel , Tobias Nipkow , Christian Prehofer , Birgit Schieder, Interpreter Verification for a Functional Language, Proceedings of the 14th Conference on Foundations of Software Technology and Theoretical Computer Science, p.77-88, December 15-17, 1994

76

Martin Fränzle , Markus Müller-Olm, Towards Provably Correct Code Gneration for a Hard Real-Time Programming Language, Proceedings of the 5th International Conference on Compiler Construction, p.294-308, April 07-09, 1994

77

Theodore S. Norvell, Machine Code Programs are Predicates Too; Proceeding of the 6th Refinement Workshop, January 1994, David Till (Ed.), Workshops in Computing, Springer-Verlag, 1994.

78

Theodore Stevens Norvell , Eric C. Hehner, A predicative theory of machine languages and its application to compiler correctness, 1994

79

Egon Börger , Igor Durdanovic , Dean Rosenzweig, Occam: Specification and Compiler Correctness - Part I: The Primary Model, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi, p.489-508, June 06-10, 1994

80

R. W. S. Hale; Program compilation; In J. Bowen, editor, Towards Verified Systems, volume 2 of Real-Time Safety Critical Systems, chapter 7, pages 131--146. Elsevier, 1994.

81

David Steven Gladstein, Compiler correctness for concurrent languages, Northeastern University, Boston, MA, 1995

82

John Hannan, Searching for semantics, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.1-12, June 14-16, 1993, Copenhagen, Denmark  [doi>10.1145/154630.154631]

83

C. A. R. Hoare , He Jifeng , A. Sampaio, Normal form approach to compiler design, Acta Informatica, v.30 n.9, p.701-739, Nov. 1993

84

John Hannan, and Frank Pfenning; Compiler Verification in LF; Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, edited by Andre Scedrov, IEEE Computer Society Press, 407--418, 1992.

85

H. Langmaack; On Programming Languages Interpreters - Total Correctness; in: H. Langmaack, E. Neuhold, M. Paul (Hrsg.) "Software Construction - Foundation and Application", Seminar-Report, Int. Begegn.- u. Forschzentr. f. Informatik, Schloß Dagstuhl, Deutschland, 1992.

86

Bettina Buth , Karl-Heinz Buth , Martin Fränzle , Burghard von Karger , Yassine Lakhnech , Hans Langmaack , Markus Müller-Olm, Provably Correct Compiler Development and Implementation, Proceedings of the 4th International Conference on Compiler Construction, p.141-155, October 05-07, 1992

87

Markus Müller-Olm; Total Correctness of an Interpreter.; Proceedings of the 6th Workshop of the RWTH Aachen, CAU Kiel, and TU München on "Programmiersprachen - Methoden, Semantik, Implementierungen", Landhaus Rothenberge (Germany). (eds.: W.-M. Lippe, G. Stroth), Technischer Bericht (7/92-I), pp. 141--155. Institut für Angewandte Mathematik und Informatik, Universität Münster, 1992.

88

Markus Müller-Olm; Total Correctness of an Interpreter. Christian-Albrechts-Universität, Kiel, Kiel MMO 4/1, Germany. ProCoS Technical Report. March 1992,

89

Fabio Q B da Silva; Observational Equivalence and Compiler Correctness; LFCS report ECS-LFCS-92-240, September 1992.

90

Fabio Q B da Silva; Correctness Proofs of Compilers and Debuggers: an Approach Based on Structural Operational Semantics; LFCS report ECS-LFCS-92-241 (also published as CST-95-92); 1992.

91

Hans Langmaack, M. Fränzle, and M. Müller-Olm; Development of Proven Correct Compilers in ProCoS; ProCoS Project Doc., Kiel MF7; 1990.

92

A. Sampaio; A Comparative Study of Theorm Provers: Proving Correctness of Compiling Specifications; Technical Report PRG-20-90, Oxford University, Computing Laboratory, 1990. Also as ProCoS Document {OU AS 90/1}, 1990.

93

W. Young, Verified compilation in micro-Gypsy, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.20-26, December 13-15, 1989, Key West, Florida, United States

94

H. Langmaack, and M. Müller-Olm; First Steps in Proven Correct Compiler Development in ProCoS.; Christian-Albrechts-Universität zu Kiel, {Kiel HL 1/2}, Germany. ProCoS Technical Report; October 1989.

95

J. Strother Moore, A mechanically verified language implementation, Journal of Automated Reasoning, v.5 n.4, p.461-492, Dec. 1989

96

Joëlle Despeyroux, Proof of translation in Natural Semantics, first Symp. on Logic In Computer Science, LICS, Cambridge, Ma, USA, June 1986. Also appears as INRIA research report RR 514, April 1986

97

James W. Thatcher, Eric G. Wagner and Jesse B. Wright; More on advice on structuring compilers and proving them correct; Theoretical Computer Science, Volume 15, Issue 3, 1981, Pages 223--249; 1981.

98

Wolfgang Polak, Compiler Specification and Verification, Springer-Verlag New York, Inc., Secaucus, NJ, 1981

99

F. Lockwood Morris, Advice on structuring compilers and proving them correct, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.144-152, October 01-03, 1973, Boston, Massachusetts  [doi>10.1145/512927.512941]

100

John McCarthy, and James Painter; Correctness Of A Compiler For Arithmetic Expression; Proceedings Symposium in Applied Mathematics, Vol 19, Mathematical Aspects of Computer Science, 1967.

Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, ACM SIGPLAN Notices, v.41 n.1, p.42-54, January 2006

Ingo Stürmer , Daniela Weinberg , Mirko Conrad, Overview of existing safeguarding techniques for automatically generated code, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005

Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006

Lee Pike , Mark Shields , John Matthews, A verifying core for a cryptographic language compiler, Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, August 15-16, 2006, Seattle, Washington

Adam Chlipala, A certified type-preserving compiler from lambda calculus to assembly language, ACM SIGPLAN Notices, v.42 n.6, June 2007

Adam Chlipala, Parametric higher-order abstract syntax for mechanized semantics, ACM SIGPLAN Notices, v.43 n.9, September 2008

David Aspinall , Lennart Beringer , Alberto Momigliano, Optimisation Validation, Electronic Notes in Theoretical Computer Science (ENTCS), v.176 n.3, p.37-59, July, 2007

Jean-Baptiste Tristan , Xavier Leroy, Formal verification of translation validators: a case study on instruction scheduling optimizations, ACM SIGPLAN Notices, v.43 n.1, January 2008

Dirk Leinenbach , Elena Petrova, Pervasive Compiler Verification -- From Verified Programs to Verified Systems, Electronic Notes in Theoretical Computer Science (ENTCS), 217, p.23-40, July, 2008

Ingo Stuermer , Mirko Conrad , Heiko Doerr , Peter Pepper, Systematic Testing of Model-Based Code Generators, IEEE Transactions on Software Engineering, v.33 n.9, p.622-634, September 2007

Nick Benton , Nicolas Tabareau, Compiling functional types to relational specifications for low level imperative code, Proceedings of the 4th international workshop on Types in language design and implementation, January 24-24, 2009, Savannah, GA, USA

Xavier Leroy, Formal verification of a realistic compiler, Communications of the ACM, v.52 n.7, July 2009

Bartira Dantas , David Déharbe , Stephenson Galvão , Anamaria Martins Moreira , Valério Medeiros, Júnior, Verified Compilation and the B Method: A Proposal and a First Appraisal, Electronic Notes in Theoretical Computer Science (ENTCS), 240, p.79-96, July, 2009