%--------------------------------------------------------------------------- % Datei: verifix.bib % Autor: Wolfgang Goerigk % Beschreibung: Alle Verifix-Zitate, alphabetisch sortiert % Stand: 23.02.95 %--------------------------------------------------------------------------- % $Revision: 1.71 $ % $Id: verifix.bib,v 1.71 1999/02/22 12:12:18 wg Exp $ %--------------------------------------------------------------------------- % % Anleitung: % ~~~~~~~~~~ % % 1. Schluesselbezeichnung: % ~~~~~~~~~~~~~~~~~~~~~~ % a. bei einem Autor: Name und Jahreszahl und eventuell % Kleinbuchstaben, um verschiedene Arbeiten zu % unterscheiden. Beispiel: \cite{Assmann93d}. % b. bei zwei Autoren: Name1/Name2, sonst wie in a. Beispiel: % \cite{Buth/Mueller-Olm93}. % c. bei mehr als zwei Autoren: Name des ersten Autors, ein "+" und % die Jahreszahl. Beispiel: \cite{Buth+92}. % % - In den Schluesselbezeichnungen fuer die Umlaute ae, Ae, ... , Ue % und ss benutzen. % % 2. Ergaenzungen % ~~~~~~~~~~~~ % - Zitat nach Schluesselbezeichnung alphabetisch einsortieren. % - \cite{...} mit Kommentar alphabetisch in die Liste der % enthaltenen Schluessel einsortieren. % - Email an mich ( wg ) mit kommentiertem Zitat und BibTeX-Eintrag. % % 2. Sonstiges % ~~~~~~~~~ % - TeX-Umlaute durch \"a, ... bzw. {\ss} darstellen (wg. engl. Texte). % - Month: jan, feb, mar, apr, may, jun, % jul, aug, sep, oct, nov, dec % (ohne geschweifte Klammern!). % - bitte keine LaTeX2e-Befehle (z.B. \mathit{...}) benutzen % %--------------------------------------------------------------------------- % % Enthaltene Schluessel: % ~~~~~~~~~~~~~~~~~~~~~~ % % \cite{Abecker+95} % Exploring and Validating Declarative Knowledge % \cite{Abelson+86} % Revised^3 Report on Scheme % \cite{Ackermann+88} % Wissensbasiskompilation: Institutsbericht % \cite{Ackermann+89} % Wissensbasiskompilation in Christaller+89 % \cite{Ackermann+91} % Wissensbasiskompilation: KI-Artikel % \cite{Ackermann+92} % Knowledge Base Compilation: in Christaller+92 % \cite{Ackermann/Goerigk87a} % Das Projekt: Uebersetzung von Wissensbasen % \cite{Ackermann/Goerigk87b} % Uebersetzung von PROLOG nach LISP % \cite{Ackermann91} % Dissertation Dieter Ackermann % \cite{Assmann93d} % Edge Addition Rewrite Systems % \cite{Assmann94a} % Konfluente Graphersetzungssysteme % \cite{Attardi95} % The Embeddable Common Lisp % % \cite{Baker90} % The NIMBLE Project % \cite{Bibel87} % Automated Theorem Proving % \cite{Birtwistle+73} % Simula Begin % \cite{Bittel91} % Ein tableaubasierter Theorembeweiser % \cite{Bjoerner+93} % ProCoS: Provably Correct Systems % \cite{Bjoerner91} % Final Report ProCoS % \cite{Blum+89} % Program Result Checking Against Adaptive Programs % \cite{Blum+90} % Self-Testing/Correcting % \cite{Blum/Kannan89} % Program Correctness Checking % \cite{Blum/Kannan95} % Designing Programs that Check Their Work % \cite{Boerger+94} % Occam: Specification and Compiler Correctness % \cite{Boerger96} % Correctness of Compiling Occam to Transputer % \cite{Boerger/Rosenzweig92} % The WAM-definition and Compiler Correctness % \cite{Boley92b} % RELFUN: Extended Logic-plus-Functional Programming % \cite{Bowen+90} % Verifiable compiling Specification % \cite{Bowen92} % Logic Programming in Compilation % \cite{Bowen+94} % Hardware Compilation % \cite{Boyer/Moore77} % Correctness of a simple optimizing compiler % \cite{Boyer/Moore79} % A Computational Logic % \cite{Brauer93} % KI auf dem Weg in die Normalitaet % \cite{Bretthauer+92} % APPLY: KI-Artikel % \cite{Bretthauer+94} % APPLY: Abschlussbericht des BMFT-Projektes % \cite{Brown+92} % Actress % \cite{Broy92} % Software Specification, Larch Proof Assistant % \cite{BSI94} % BSI-Zertifizierung % \cite{Burghardt93} % Eine feinkoernige Sortendisziplin % \cite{Burkart+91} % CLiCC % \cite{Burkart91} % Diplomarbeit Olaf Burkart % \cite{Burn+86} % Strictness analysis for higher order functions % \cite{Burstall/Landin69} % Programs and their proofs: an algebraic approach % \cite{Buth+92} % Provably correct compiler development % \cite{Buth/Mueller-Olm93} % Provably Correct Compiler Implementation % \cite{Buth92b} % Using SOS Definitions in Term Rewriting Proofs % % \cite{Cardelli84} % A Semantics of Multiple Inheritance % \cite{Chirica/Martin86} % Towards Compiler Implementation Correctness Proofs % \cite{Christaller+89} % Die KI-Werkbank BABYLON % \cite{Christaller+92} % The AI workbench BABYLON % \cite{Cohn79a} % High Level Proof in LCF % \cite{Cohn79b} % Machine Assisted Proofs of Recursion Implement. % \cite{Constable+86} % Nuprl Book % \cite{Cooper72a} % Theorem Proving in arithmetic % \cite{Coquand+94} % Type Theory and Programming % \cite{Coquand/Huet88} % The Calculus of Constructions % \cite{Cousot/Cousot77} % Abstract interpretation % \cite{Curzon93a} % Deriving Correctness Properties from Compiled Code % \cite{Curzon94} % The Verified Compilation of Vista Programs % % \cite{Davidson/Fraser80} % Retargetable Peephole Optimizer % \cite{Dershowitz/Jouanaud90} % Rewrite Systems % \cite{Diehl96} % Diss Semantics-Directed Compiler Generation % \cite{Dijkstra98} % R. Dijkstra: Computation Calculus % \cite{Dijkstra76} % A Discipline of Programming % \cite{Dijkstra/Scholten90}% Predicate Calculus and Program Semantics % \cite{Dold+92} % Korso Aufgabe: Implementierung von Mengen % \cite{Dold93} % Formalisierung Schematischer Algorithmen % \cite{Dold94} % Program Development with Specification Operators % \cite{Dold+95} % Verifying Peephole Optimizations war: \cite{DHPR95} % \cite{Dold+96} % Erhaltung partieller Korrektheit und Formalisierung % \cite{Dold+96b} % Zwischenbericht Verifix % \cite{Drossopoulou+82} % An Attribute Grammar for Ada % \cite{Dybjer85} % Domain Algebras to prove compiler correctness % % \cite{Emmelmann+88} % BEG % \cite{Emmelmann92} % Code Selection and term rewriting % % \cite{Farmer+91} % Little Theories % \cite{Farmer+93} % IMPS: An Interactive Mathematical Proof System % \cite{Frank90} % Diplomarbeit Karsten Frank % % \cite{GMD87} % BABYLON-Referenzhandbuch % \cite{Gallier92} % Constructive Logics, Typed Lambda-Calculus % \cite{Garland/Guttag91} % A Guide to LP, The LARCH Prover % \cite{Gaudel95} % Formal Approaches for Ul. High Dependability % \cite{Gaul+96} % An Architecture for Verified Compiler Construction % \cite{Gentzen34} % Untersuchungen ueber das logische Schliessen % \cite{Goodenough/Gerhart75} % Toward a Theory of Test Data Selection % \cite{Goerigk/Hoffmann96} % ComLisp (engl.) (VERIFIX/CAU/1.7) % \cite{Goerigk/Hoffmann97} % Compiling Specification (Institutsbericht) % \cite{Goerigk/Hoffmann98} % Rigorous Compiler ... FM-TRENDS'98, LNCS % \cite{Goerigk/Hoffmann98b}% Compiler Construction to ComLisp (Institutsbericht) % \cite{Goerigk/Mueller-Olm96} % Beweisskizze Erhalt. part. Korrektheit % \cite{Goerigk/Simon91} % Zielsetzungen im Verbundvorhaben APPLY % \cite{Goerigk/Simon93} % KI'93 Workshop: Migration und Kompilation % \cite{Goerigk/Simon98} % Towards Rigorous ... Proceedings VIM Workshops % \cite{Goerigk89a} % Semantik und Uebersetzung obj.-or. WR-Sprachen % \cite{Goerigk89b} % Uebersetzerkorrektheit, Hirschegg 89 % \cite{Goerigk93} % Dissertation Wolfgang Goerigk % \cite{Goerigk95} % Correctness if Compilers and Implementations % \cite{Goerigk95b} % Transputer Machine Code and Boot Program % \cite{Goerigk96a} % Compiler Implementation Verification SAFECOMP'96 % \cite{Goerigk96b} % ACL2: An Exercise in Program Verification % \cite{Goerigk97b} % A Denotational Semantics for ComLisp and SIL % \cite{Goerigk97c} % Towards Rigorous ... Honnef 97 % \cite{Goerigk97d} % Towards Rigorous ... Avendorf, Fehmarn 97 % \cite{Goerigk+96} % CC '96 (Poster Session) % \cite{Goerigk+96b} % KI-Artikel: Komplettkompilation von Lisp ... % \cite{Goerigk+96c} % Verifix-Arbeitspapier Bootloader-Korrektheit % \cite{Goerigk+97a} % Rigorous Compiler Implementation Correctness % \cite{Goerigk+98} % Correct Programs without Proof, Malente-WS % \cite{Goerigk+98b} % Praktikable Konstruktion korrekter Uebersetzer ST'98 % \cite{Goldberg/Robson83} % Smalltalk-80 % \cite{Goos/Winterstein80} % Towards a Compiler Front-End for Preliminary Ada % \cite{Goos81} % Problems in Compiling Ada % \cite{Goos+94} % Verifix-Projektantrag % \cite{Grosch/Emmelmann90} % A toolbox for compiler construction % \cite{Gurevich91} % Evolving Algebras; A Tutorial Introduction % \cite{Gurevich95} % Evolving Algebras; Lipari Guide % \cite{Gurevich/Huggins93} % Semantics of C % \cite{Guttman+92} % A Guide to VLisp, A Verified Programming ... % % \cite{Habel92} % Hyperedge Replacement: Grammars and Languages % \cite{Hannan94} % Operational Semantics-Directed Compilers % \cite{Hannan/Pfenning92} % Compiler Verification in LF % \cite{Heberle+98} % submitted to PSI'99 % \cite{He+93} % He Jifeng et al: Correct Hardware Design % \cite{Hennessey92} % Wade Common Lisp % \cite{Hoare/Lauer74} % Consistent and Complementary Formal Theories % \cite{Hoare69} % An axiomatic basis for computer programming % \cite{Hoare91} % Refinement algebra % \cite{Hoare+93} % Normal form approach % \cite{Huet+93} % The Coq Proof Assistant, User's Guide % \cite{Hoffmann95a} % Ueberblick ComLisp->TC (VERIFIX/CAU/1.1) % \cite{Hoffmann95b} % ComLisp (VERIFIX/CAU/1.2) % \cite{Hoffmann95c} % Cop (VERIFIX/CAU/1.3) % \cite{Hoffmann95d} % intermediateC (VERIFIX/CAU/1.4) % \cite{Hoffmann95e} % TASM (VERIFIX/CAU/1.5) % \cite{Hoffmann96a} % C -> TASM Compiling Specification (VERIFIX/CAU/1.6) % \cite{Hoffmann96b} % ComLisp -> Cop Compiling Spec (VERIFIX/CAU/1.8) % \cite{Hoffmann96c} % Cop -> C Compiling Spec (VERIFIX/CAU/1.9) % \cite{Hoffmann96d} % Ueber d. korrekte Impl. v. Comp. (VERIFIX/CAU/3.1) % \cite{Hoffmann96f} % ComLisp -> Cop Programm % \cite{Hoffmann96g} % Cop -> intermediateC Programm % \cite{Hoffmann96h} % Korrekte Programmkonstruktion in ComLisp % \cite{Hoffmann96i} % IntermediateC -> Tasm Programm % \cite{Hoffmann96j} % Tasm -> TC Programm % \cite{Hoffmann97} % Arbeitstagung Programmiersprachen % \cite{Hoffmann97b} % Correct Implementation of Compiler Programs Avendorf % \cite{Hoffmann98} % Towards a Trusted Tool-Chain... Malente % \cite{Hoffmann98b} % Dissertation U.Hoffmann % \cite{Hoffmann/Pfeifer96} % Formalisierung intermediateC -> Tasm % % \cite{Inmos88} % Transputer instruction set % % \cite{Jensen/Wirth75} % PASCAL % \cite{Jones90} % Systematic Software Development Using VDM % \cite{Jones/Schmidt80} % Compiler generation from denotational semantics % \cite{Joyce89} % A verified compiler for a Verified Microprocessor % \cite{Joyce90} % Totally Verified Systems: Linking ... % % \cite{Kamin88} % Denotational Semantics for Smalltalk % \cite{Karger92} % Distinguishing Divergence from Chaos % \cite{Karger93} % Algebraic Compiler Verification % \cite{Kastens80} % Ordered Attribute Grammars % \cite{Kaufmann/Moore94} % Design Goals of ACL2 % \cite{Keene89} % CLOS Programming % \cite{Kernighan/Ritchie78} % The C Programming Language % \cite{Kernighan/Ritchie83} % Programmieren in C % \cite{Kersten95} % Sicherheit in der Informationstechnik % \cite{Knemeyer/Schulenburg93} % Expertensysteme in der Versicherungswirtsch. % \cite{Knoop+92} % Lazy code motion % \cite{Knoop+93a} % Optimal Code Motion: Theory and Practice % \cite{Knoop+93b} % Lazy Strength Reduction % \cite{Knoop+94} % Partial Dead Code Elimination % \cite{Knoop/Steffen92a} % The Interprocedural Coincidence Theorem % \cite{Knoop/Steffen92b} % Optimal interproc. partial redundancy elimination % \cite{Knoop/Steffen92c} % Optimal Interprocedural Data Flow Analysis % \cite{Knoop93} % Dissertation Jens Knoop % \cite{Knoop94} % Higher Order Data Flow Analysis % \cite{Knutzen91} % Diplomarbeit Heinz Knutzen % \cite{Kock92} % Verifikation von Optimierungsalgorithmen % % \cite{Landwehr+82} % Automatic Code Generator Generator % \cite{Lange+96} % Pets-Papier: Test Generation % \cite{Langmaack89} % Vollst. operat. adaequate den. Semantiken % \cite{Langmaack96a} % The ProCoS Approrach to Correct Systems % \cite{Langmaack96b} % Softwareengineering zum Zertifizieren (Verifix/CAU/4.1) % \cite{Langmaack97c} % Ein Beitrag zu Goodenoughs und Gerahrts Theorie % \cite{Langmaack97a} % Softwareengineering zur Zertifizierung % \cite{Langmaack97b} % Theoretische Informatik ist Grundlage ... % \cite{Langmaack/Goerigk95} % VerComp-DFG-Projektantrag % \cite{Lee89} % Realistic Compiler Generation % \cite{Lippe/Simon90} % Applikative Programmierung in Vorb. % \cite{Littlewood/Strigini95} % Validation of Ultra-High Dependability % \cite{Loeckx/Sieber87} % Foundations of Program Verification % \cite{Luo/Pollack92} % LEGO Proof Development System: User's Manual % \cite{Luo90} % An Extended Calculus of Constructions % \cite{Luo91a} % A Higher-Order Calculus and Theory Abstraction % \cite{Luo91b} % Program Spec. and Data Refinement in Type Theory % % \cite{Marriott93} % Frameworks for abstract interpretation % \cite{McCarthy/Painter67} % Correctness of a Compiler % \cite{McCarthy60} % Lisp % \cite{McCarthy62} % LISP 1.5 Programmer's Manual % \cite{Meijer92} % Calculating Compilers % \cite{Mertens+93} % Betriebliche Expertensystem-Anwendungen % \cite{Michelsen98} % Diplomarbeit Dagobert Michelsen % \cite{Milner+90} % Standard ML % \cite{Mohnberg90} % Diplomarbeit Andreas Mohnberg % \cite{Moore/Kaufmann96} % ACL2: An Industrial Strength Version of Nqthm % \cite{Moore88} % Piton: A Verified Assembly Level Language % \cite{Moore89} % A mechanically verified language implementation % \cite{Moore92} % The Acl2-Project % \cite{Moore96} % Piton, A Mechanically Verified ... % \cite{Morris74} % Compiler Correctness % \cite{Mosses79} % SIS - semantics implementation system % \cite{Mosses82} % Abstract semantic algebras % \cite{Mosses92} % Action Semantics % \cite{Mueller-Olm90} % Korrektheit einer "Ubersetzung ... % \cite{Mueller-Olm93} % ProCoS: Compiling Specification SubLisp to PL % \cite{Mueller-Olm95} % An Exercise in Compiler Verification % \cite{Mueller-Olm96} % Modular Compiler Verification (Dissertation) % \cite{Mueller-Olm96b} % Three Views ... % % \cite{Nagl90} % Softwaretechnik % \cite{Nagl91} % ADA % \cite{Necula97} % Proof-Carrying Code % \cite{Necula/Lee98} % Certifying Compilers % \cite{Nelson/Oppen80} % Congruence closures % \cite{Nielson82} % A denotational framework for data flow analysis % \cite{Nuprl93} % Nuprl Manual % % \cite{ODonnell85} % Equational Logic as a Programming Language % \cite{Oliva/Wand92} % A Verified Compiler for Pure PreScheme % \cite{Oppacher/Suen88} % HARP: A Tableau-Based Theorem Prover % \cite{Owre+92} % PVS: A Prototype Verification System % \cite{Owre+93} % Formal verification, fault-tolerant architectures % % \cite{Palsberg92} % Generated Ada Compiler % \cite{Parnas94} % Inspection of Safety Critical Software % \cite{Partsch90} % Specification and Transformation of Programs % \cite{Paulson81} % A compiler generator for semantic grammars % \cite{Persch+83} % Ada Compiler Karlsruhe Overview % \cite{Pettersson95} % Compiling Natural Semantics % \cite{Pfeifer94} % Reflexion von QED in QED % \cite{Pfeifer96a} % Supporting Refinement Calculus Proofs in PVS % \cite{Pfeifer+96} % Mechanized Semantics of Simple ... (Ulmer IB) % \cite{Pfeifer+96a} % Mechanized Semantics of Simple ... (Verifix AB) % \cite{Pofahl95} % Inspecting Safety Relevant Software} % \cite{Polak81} % Compiler Specification and Verification % \cite{Pym/Wallen90a} % proof-search,first-order dependent function types % % \cite{Randell+95} % Proc. PDCS'95 % \cite{Reddy88} % Objects as Closures % \cite{Robinson96} % Formal and Informal Proof % \cite{Rubinfeld90} % Self-Checking, Self-Testing and Self-Correcting % \cite{Ruehle98} % Diplomarbeit Juergen Ruehle % \cite{Ruess93} % Specification Language QED % \cite{Rushby+91} % Verification Using Ehdm, Tutorial % \cite{Rushby/vHenke93} % Formal verif. of algorithms for critical systems % \cite{Rushby94} % Proof Movie II: A Proof with PVS % % \cite{Sampaio91} % A Comparative Study of Theorem Provers % \cite{Sampaio93} % An Algebraic Approach to Compiler Design % \cite{Schmidt85} % Detecting global variables in denot. specif. % \cite{Schmidt88} % Detecting stack-based env. in denot. definitions % \cite{Schroeer88} % Districts: Suppression of Partial Redundancies % \cite{Schroeer88b} % Das GMD Modula-2 Entwicklungssystem % \cite{Schuerr91} % Operat. Spezifizieren mit Graphersetzungssystemen % \cite{Schwarz+88} % An Optimizer for Ada % \cite{Schwier93a} % Semantik von QED % \cite{Schwier93b} % Formale Programmentwicklung in QED % \cite{Shankar91} % Proof Search in Intuitionistic Sequent Calculus % \cite{Shostak79a} % Arithmetic with Function Symbols % \cite{Simpson90} % Compiler Specification for the SECD Machine % \cite{Sites92} % Alpha Architecture Reference Manual % \cite{Smith82} % Reflection and Semantics % \cite{Smith84} % Reflection and Semantics in Lisp % \cite{Smith87} % Structure and Desing of Global Search Algorithms % \cite{Steele84} % Common Lisp: The Language % \cite{Steele90} % Common Lisp: The Language 2. Edition % \cite{Steffen+89} % The Value Flow Graph % \cite{Steffen+90} % The Value Flow Graph % \cite{Steffen+91} % Efficient Code Motion and Strength Reduction % \cite{Steffen/Knoop89} % Finite Constants % \cite{Steffen/Knoop91} % Finite Constants % \cite{Steffen87a} % Optimal Run Time Optimization % \cite{Steffen87b} % Institutsbericht: Optimalitaet bei Optimierern % \cite{Steffen89} % Optimal Data Flow Analysis % \cite{Stoy77} % Denotational Semantics % \cite{Symbolics85} % Reference guide to Symbolics LISP % \cite{Symbolics86} % Symbolics Common Lisp: Language Concepts % % \cite{Taiichi/Masami86} % Kyoto Common Lisp Report % \cite{Tarditi+90} % Compiling Standard ML to C % \cite{Thatcher+81} % Structuring Compilers and Proving them Correct % \cite{Thompson84} % Reflections on Trusting Trust % % \cite{Uhl86} % Spezifikation von Programmierspr. u. Uebersetzern % % \cite{Vollmer/Hoffart92} % Modula-P % % \cite{Waite/Goos84} % Compiler Construkction % \cite{Wallace95} % The Semantics of C++ % \cite{Wallen90} % Automated proof search in non-classical logics % \cite{Wand/Friedman86} % Reflection % \cite{Wand84} % A semantic prototyping system % \cite{Wand87} % Complete Type Inference for Simple Objects % \cite{Wasserman/Blum97} % Software reliability via run-time result-checking % \cite{Weber-Wulff93} % Proof Movie, Boyer-Moore prover % \cite{Weber91} % Meta Calculus for Formal System Development % \cite{Weule93} % Expertensysteme im industriellen Einsatz % \cite{Wolf99a} % An Exercise ... Revisited % \cite{Wolf99b} % The Adequacy of a Loop's Definition % \cite{Woodcock/Morgan90} % VDM90: Refinement of State Based Conc. Systems % % \cite{Yellin95} % Bytecode Verification % \cite{Young88} % A Verified Code Generator for a Subset of Gypsy % % \cite{Zimmermann90} % Automatische Komplexitaetsanalyse % \cite{Zimmermann/Gaul96} % Correct Compiler Back-Ends: An ASM Approach % % \cite{ZSI89} % IT-Sicherheitskriterien % \cite{ZSI90} % IT-Evaluationshandbuch % % \cite{diPrimio+85} % BABYLON als Werkzeug % % \cite{vHenke+94} % Arbeitsbericht Korso, LNCS % % % Karlsruher Technische Berichte Verifix % -------------------------------------- % \cite{Verifix95:ISinformell} % \cite{Verifix95:SemIS} % \cite{Verifix96:MIS1} % \cite{Verifix95:Alpha} % \cite{Verifix96:MIS1toAlphaSimple} % \cite{Verifix96:MIStoAlpha} % \cite{Verifix96:SemAnalyse0} % \cite{Verifix96:IS0toMIS} % \cite{Verifix96:IS0toMISproofDA} % \cite{ZDG:96} % \cite{Verifix96:Bench} % \cite{} % % %--------------------------------------------------------------------------- % % Vorgenommene Schluesselaenderungen % ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % % Im folgenden sind die Aenderungen verzeichnet, die in dem Original % verifix.tex des Verifix-Antrages (Datum 23.12.96) vorgenommen werden % muessen. um es mit dieser Version von verifix.bib zu prozessieren. % % BoergerEgo1994a -> Boerger+94 % Dijkstra76:Disc -> Dijkstra76 % WaiteGoos:84:Compiler -> Waite/Goos84 % Gurevich-Huggins93 -> Gurevich/Huggins93 % Jensen-Wirth:Pascal75 -> Jensen/Wirth75 % WallaceC++95 -> Wallace95 % Sites:Alpha92 -> Sites92 % Goerick-et-al:CC96 -> Goerigk+96 % GGGHZ:96 -> Gaul+96 % Zimmer-Gaul:96 -> Zimmermann/Gaul96 % % Im folgenden sind die Aenderungen verzeichnet, die in dem Original % Verifix.tex des Verifix-Antrages (Datum 7.4.94) vorgenommen werden % muessen. um es mit dieser Version von verifix.bib zu prozessieren. % % Ackermann90 -> Ackermann91 % Ada88 -> Schwarz+88 % ALF -> Coquand+94 % assmann.93d -> Assmann93d % assmann.94a -> Assmann94a % % babylon87 -> GMD87 % babylonbook -> Christaller+89 % Bibel:1987 -> Bibel87 % Bjorner+93 -> Bjoerner+93 % Bjorner91 -> Bjoerner91 % Blum89a -> Blum/Kannan89 % Blum89b -> Blum+89 % Blum90 -> Blum+90 % BM77 -> Boyer/Moore77 % BM79 -> Boyer/Moore79 % BoergerRosenzweig92 -> Boerger/Rosenzweig92 % Bowen90 -> Bowen+90 % Brown92 -> Brown+92 % Bro92 -> Broy92 % bur91 -> Burkart91 % Burn86 -> Burn+86 % Burstall69 -> Burstall/Landin69 % Buth93 -> Buth/Mueller-Olm93 % ButhOlm93 -> Buth/Mueller-Olm93 % % card84 -> Cardelli84 % CH88 -> Coquand/Huet88 % clos -> Keene89 % Coh79a -> Cohn79a % Coh79b -> Cohn79b % Cooper:72a -> Cooper72a % Coq -> Huet+93 % Cousot77 -> Cousot/Cousot77 % % Davidson80 -> Davidson/Fraser80 % DerJou90 -> Dershowitz/Jouanaud90 % DHRSS92 -> Dold+92 % diprimio85 -> diPrimio+85 % Dol93 -> Dold93 % Dol94 -> Dold94 % Dross82 -> Drossopoulou+82 % Dybjer -> Dybjer85 % % EHDM:tutorial:91 -> Rushby+91 % Emmelmann88 -> Emmelmann+88 % % Farmer:91 -> Farmer+91 % Farmer:93 -> Farmer+93 % FME:93 -> Owre+93 % fra90 -> Frank90 % % Gallier:ConstrLog1 -> Gallier92 % Gentzen:34 -> Gentzen34 % GG91 -> Garland/Guttag91 % Goos80 -> Goos/Winterstein80 % Grosch -> Grosch/Emmelmann90 % % HANNAN92 -> Hannan/Pfenning92 % HenryBaker90 -> Baker90 % Hoare90 -> Hoare91 % INMOS:Assembler -> Inmos88 % % Jones80 -> Jones/Schmidt80 % Joy89 -> Joyce89 % % kamin88 -> Kamin88 % kcl86 -> Taiichi/Masami86 % KernRitch -> Kernighan/Ritchie83 % KernRitch78 -> Kernighan/Ritchie78 % Knemeyer93 -> Knemeyer/Schulenburg93 % Knphd -> Knoop93 % Knprocomet94 -> Knoop94 % knu91 -> Knutzen91 % KRSjpldi93 -> Knoop+93b % KRSpldi92 -> Knoop+92 % KRSpldi94 -> Knoop+94 % KRStoplas93 -> Knoop+93a % KScc92a -> Knoop/Steffen92a % KScc92b -> Knoop/Steffen92b % KSdagstuhl92 -> Knoop/Steffen92c % % Landwehr82 -> Landwehr+82 % LEGO:92 -> Luo/Pollack92 % lisi90 -> Lippe/Simon90 % LNCSpaper -> vHenke+94 % Luo:91a -> Luo91a % Luo:91b -> Luo91b % % mccarthy60 -> McCarthy60 % mccarthy62 -> McCarthy62 % McCarthy67 -> McCarthy/Painter67 % Mertens93 -> Mertens+93 % MilnerTofteHarper90 -> Milner+90 % ML2C -> Tarditi+90 % Modula2 -> Schroeer88b % moh90 -> Mohnberg90 % Moo88 -> Moore88 % Morgan:VDM90 -> Woodcock/Morgan90 % % NelsonOppen:80 -> Nelson/Oppen80 % Nuprl:Book:86 -> Constable+86 % Nuprl:Manual:93 -> Nuprl93 % % ODo85 -> ODonnell85 % Olm:SIL -> Mueller-Olm93 % OppacherSuen:88 -> Oppacher/Suen88 % % Persch83 -> Persch+83 % Pfe94 -> Pfeifer94 % Pol81 -> Polak81 % Pro93 -> Bjoerner+93 % PVS:Overview:92 -> Owre+92 % Pym:90a -> Pym/Wallen90a % % reddy88 -> Reddy88 % Rue93 -> Ruess93 % Rus94 -> Rushby94 % Rushby:vHenke:TSE93 -> Rushby/vHenke93 % % Sampaio:93 -> Sampaio93 % Sch93a -> Schwier93a % Sch93b -> Schwier93b % scheme86 -> Abelson+86 % Schurr92 -> Schuerr91 % Shankar:1991 -> Shankar91 % Shostak:79a -> Shostak79a % Sim90 -> Simpson90 % simula -> Birtwistle+73 % SKmfcs89 -> Steffen/Knoop89 % skr89 -> Steffen+89 % SKResop90 -> Steffen+90 % SKRtapsoft91 -> Steffen+91 % SKtcs91 -> Steffen/Knoop91 % smalltalk80 -> Goldberg/Robson83 % Smi87 -> Smith87 % steele -> Steele84 % steele90 -> Steele90 % stoy -> Stoy77 % symbolics85 -> Symbolics85 % symbolics86 -> Symbolics86 % % Thatcher81 -> Thatcher+81 % % Vollmer92 -> Vollmer/Hoffart92 % % Wallen:90 -> Wallen90 % wand87 -> Wand87 % WW93 -> Weber-Wulff93 % % Yo88 -> Young88 % % Zimm90 -> Zimmermann90 % %--------------------------------------------------------------------------- % % Benutzbare String-Abkuerzungen % ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ % @STRING{ LNCS = {Lecture Notes in Computer Science}} @STRING{ CACM = {Communications of the ACM}} @STRING{ HONNEF = {Work\-shop {\sl ``Alternative Konzepte f\"ur Sprachen und Rechner''}}} @STRING{ CAUIfIuPM = {Institut f\"ur Informatik, CAU}} @STRING{ AW = {Addison--Wesley}} @STRING{ SPRINGER = {Springer-Verlag}} @STRING{ POPL = {Proceedings of POPL}} @STRING{ TOPLAS = {ACM Transactions on Programming Languages and Systems}} @STRING{ SIGPLANNOT = {{ACM SIGPLAN} Notices}} @STRING{ JPLDI = {Journal of Programming Languages}} @STRING{ PLDI = {{ACM SIGPLAN} Conference on Programming Language Design and Implementation}} @STRING{ ESOP = {European Symposium on Programming (ESOP)}} @STRING{ TAPSOFT = {International Joint Conference on the Theory and Practice of Software Development (TAPSOFT)}} @STRING{ CC = {Conference on Compiler Construction (CC)}} @STRING{ MFCS = {Conference on the Mathematical Foundations of Computer Science (MFCS)}} % %--------------------------------------------------------------------------- % @TechReport{Abecker+95, Author = {Andreas Abecker and Harold Boley and Knut Hinkelmann and Holger Wache and Franz Schmalhofer}, Institution = {DFKI GmbH}, Month = nov, Title = {{An Environment for Exploring and Validating Declarative Knowledge}}, Type = {{DFKI Technical Memo TM-95-03}}, Note = {Also in: Proc. Workshop on Logic Programming Environments at ILPS'95, Portland, Oregon, Dec. 1995}, Year = {1995} } @Booklet{Abelson+86, Author = {{Abelson, H. et. al.}}, Title = {$\mbox{Revised}^3\,\mbox{Report}$ on the {A}lgorithmic {L}anguage {SCHEME}}, Howpublished = {J.~Rees, W.~ Clinger (Hrsg.)}, Year = 1986 } @TechReport{Ackermann+88, Author = {Ackermann, D. and Goerigk, W. and Simon, F.}, Title = {Kompilation von {Wissensrepr\"asentationssprachen} am {Beispiel} von {BABYLON}}, Institution = CAUIfIuPM, Note = {Ebenfalls erschienen als Kapitel 8 in \cite{Christaller+89}}, Type = {Institutsbericht}, Number = {Nr. 8810}, Address = {Kiel}, Year = 1988 } @Inproceedings{Ackermann+89, Author = {Ackermann, D. and Goerigk, W. and Simon, F.}, Editor = {Christaller, Th. and diPrimio, F. and Vo{\ss}, A.}, Title = {{W}issensbasiskompilation}, BookTitle = {Die {KI--W}erkbank {BABYLON}}, Publisher = AW, Address = {Bonn}, Year = 1989 } @Article{Ackermann+91, Author = {Ackermann, D. and Goerigk, W. and Simon, F.}, Title = {{W}issensbasiskompilation: {KI}-{T}echnik in industrieller {A}nwendung}, Journal = {KI}, Year = 1991, Volume = 91, Number = 2, Pages = {93-96}, Address = {{B}aden {B}aden}, Month = jun } @Inproceedings{Ackermann+92, Author = {Ackermann, D. and Goerigk, W. and Simon, F.}, Editor = {Thomas Christaller and Franco diPrimio and Uwe Schnepf and Angi Vo{\ss}}, Title = {{Knowledge Base Compilation}}, BookTitle = {{The {AI-Workbench BABYLON} --- an Open and Portable Development Environment for Expert Systems}}, Publisher = {Academic Press}, Address = {New York, USA}, Year = 1992 } @Inproceedings{Ackermann/Goerigk87a, Author = {Ackermann, D. and Goerigk, W.}, Title = {Das {Projekt}: {\"Ubersetzung} von {Wissensbasen}}, BookTitle = HONNEF, Address = {Bad Honnef}, Year = 1987 } @Inproceedings{Ackermann/Goerigk87b, Author = {Ackermann, D. and Goerigk, W.}, Title = {{\"Ubersetzung} von {PROLOG} nach {LISP}}, BookTitle = HONNEF, Address = {Bad Honnef}, Year = 1987 } @PhDThesis{Ackermann91, Author = {Ackermann, D.}, Title = {{A}nalyse {p}olymorpher {T}ypen {b}ei {l}ogischen {P}rogrammiersprachen {m}ittels {S}ubstitutionsgrammatiken}, School = {Math.--Nat. Fakult\"at der Christian-Albrechts-Universit\"at}, Address = {{K}iel}, Note = {Institutsbericht Nr. 9101 des Instituts f\"ur Informatik und Prakt. Mathematik der CAU Kiel}, Year = 1991 } @TechReport{Assmann93d, Author = {A{\ss}mann, Uwe}, Title = {Edge Addition Rewrite Systems And Their Relevance to Program Analysis}, Institution = {GMD Forschungsstelle Karlsruhe}, Type = {{I}nterner {B}ericht}, Year = {1993} } @PhDThesis{Assmann94a, Author = {A{\ss}mann, Uwe}, Title = {Konfluente Graphersetzungssysteme und ihre Anwendung auf Programmoptimierung}, school = {Universit\"at Karlsruhe}, Year = {1994}, Address = {Kaiserstr. 12, 7500 Karlsruhe, Germany}, Month = {}, Note = {In Vorbereitung} } @Article{Attardi95, Author = {Giuseppe Attardi}, Title = {{The Embeddable Common Lisp}}, Journal = {LISP Pointers}, Volume = {VIII}, Number = {1}, Pages = {30-41}, Publisher = {ACM Press}, Year = 1995 } @Inproceedings{Baker90, Author = {Baker, H.}, Title = {{T}he {NIMBLE} {P}roject -- {A}n {A}pplications {C}ompiler for {R}eal-{T}ime {C}ommon {L}isp}, BookTitle = {Proceedings of the InfoJapan '90 Conf.}, Publisher = {Info. Proc. Soc. Japan}, Address = {Tokyo}, Year = 1990 } @Book{Bibel87, Author = {Wolfgang Bibel}, Edition = {Second}, Publisher = {Vieweg}, Title = {Automated Theorem Proving}, Year = {1987} } @Book{Birtwistle+73, Author = {Birtwistle, G. and Dahl, {O.J.} and Myhrhaug, B. and Nygaard, K.}, Title = {{SIMULA} {BEGIN}}, Publisher = {Auerbach}, Address = {Philadelphia}, Year = 1973 } @Book{Bittel91, Author = {O. Bittel}, Title = {Ein tableaubasierter Theorembeweiser f{\"u}r intuitonistische Logik}, Series = {GMD--Berichte}, Publisher = {Oldenbourg-Verlag}, Volume = {198}, Year = {1991} } @Article{Bowen+96, Author = {J. Bowen and {C. A. R.} Hoare and H. Langmaack and {E.-R.} Olderog and {A. P.} Ravn}, Title = {{A ProCoS II Project Final Report: ESPRIT Basic Reserach Project 7071}}, Journal = {EATCS-Bulletin}, Year = {1996} } @Book{Bjoerner+93, Editor = {Dines {Bj\o rner} and Hans Langmaack and {C.A.R.} Hoare}, Title = {{P}rovably {C}orrect {S}ystems -- {ProCoS}, {ESPRIT BRA 3104}}, Publisher = {Dep.\ of\ Computer Science, Techn. Univ. of Denmark}, Year = {1993}, Note = {Monograph, Final Deliverable} } @Book{Bjoerner91, Key = {Bjo}, Author = {Dines Bj{\o rner}}, Title = {{F}inal {R}eport {ProCoS} - {P}rovably {C}orrect {S}ystems, {ESPRIT BRA 3104}}, Publisher = {Dep.\ of\ Computer Science, Techn. Univ. of Denmark}, Year = {1991} } @Inproceedings{Blum+89, Author = {M. Blum and M. Luby and R. Rubinfeld}, Title = {Program Result Checking Against Adaptive Programs and in Cryptographic Settings}, BookTitle = {DIMACS Workshop on Distributed Computing and Crypthography}, Year = {1989} } @Inproceedings{Blum+90, Author = {M. Blum and M. Luby and R. Rubinfeld}, Title = {Self--Testing/Correcting with Applications to Numerical Problems}, BookTitle = {Proceedings 22nd Symposium on Theory of Computing}, Year = {1990} } @Inproceedings{Blum/Kannan89, Author = {M. Blum and S. Kannan}, Title = {Program Correctness Checking $\ldots$ and the Design of Programs that check their Work}, BookTitle = {Proceedings 21st Symposium on Theory of Computing}, Year = {1989} } @Article{Blum/Kannan95, Title = "Designing Programs that Check Their Work", Author = "Manuel Blum and Sampath Kannan", Area = "Programming Languages and Methodology", Pages = "269--291", Journal = "Journal of the ACM", Month = jan, Year = "1995", Volume = "42", Number = "1", } @InProceedings{Boerger+94, Author = {Egon Boerger and Igor Durdanovic and Dean Rosenzweig}, Booktitle = {Proc. Procomet'94 (IFIP TC2 Working Conference on Programming Concepts, Methods and Calculi)}, Title = {{O}ccam: {S}pecification and {C}ompiler {C}orrectness.{P}art {I}: {T}he {P}rimary {M}odel}, Year = 1994, Abstract-Url = {ftp://ftp.di.unipi.it/pub/Papers/boerger/01ABSTRACTS}, Url = {ftp://ftp.di.unipi.it/pub/Papers/boerger/310occam1.ps.Z}, Editor = {U. Montanari and E.-R. Olderog}, Publisher = {North-Holland}, Scope = {occam}, } @Article{Boerger96, Author = {E. B\"orger and I. Durdanovic}, Title = {{C}orrectness of {C}ompiling {O}ccam to {T}ransputer code}, Journal = {The Computer Journal}, Year = {1996}, Volume = {39}, Pages = {52-93} } @TechReport{Boerger/Rosenzweig92, Author = {B\"orger, E. and Rosenzweig, D.}, Title = {{T}he {WAM}-definition and {C}ompiler {C}orrectness}, Institution = {Dip.~di informatica}, Year = {1992}, Number = {TR-14/92}, Address = {Univ.~Pisa, Italy} } @inproceedings{Boley92b, Author = {Harold Boley}, Booktitle = {Proceedings of the 2nd International Workshop on Extensions of Logic Programming, ELP '91, Stockholm 1991}, Publisher = {Springer}, Series = {LNAI}, Title = {{Extended Logic-plus-Functional Programming}}, Volume = {596}, Year = {1992}, Editor = {Eriksson, Lars-Henrik and Halln{\"a}s, Lars and Schroeder-Heister, Peter} } @Inproceedings{Bowen+90, Author = {J. Bowen and H. Jifeng and P. Pandya}, Title = {An Approach to verifiable compiling Specification and Prototyping}, BookTitle = {Proceedings of PLILP 90}, Series = {Lecture Notes in Computer Science 456}, Year = {1990}, Publisher = SPRINGER } @Inproceedings{Bowen92, Author = {Jonathan P.~Bowen}, Title = {{F}rom {P}rograms to {O}bject {C}ode {U}sing {L}ogic and {L}ogic {P}rogramming}, Editor = {R.~Giegerich and S.~Graham}, BookTitle = {Proceedings CODE '91 International Workshop on Code Generation}, Series = {Workshops in Computing}, Year = {1992}, Publisher = SPRINGER, Address = {Schlo\ss\ Dagstuhl} } @InCollection{Bowen+94, Author = {{J. P.} Bowen and {He Jifeng} and I. Page}, Title = {Hardware Compilation}, Editor = {J. P. Bowen}, Booktitle = {Towards Verified Systems}, Publisher = {Elsevier}, Series = {Real-Time Safety Critical Systems}, Volume = {2}, Year = {1994}, Chapter = {10}, Pages = {193--207} } @TechReport{Boyer/Moore77, Author = {{R.S.} Boyer and {J S.} Moore}, Institution = {SRI International}, Number = {5}, Title = {A computer proof of the correctness of a simple optimizing compiler for expressions}, Year = {1977} } @Book{Boyer/Moore79, Author = {{R.S.} Boyer and {J S.} Moore}, Publisher = {Academic Press Inc.}, Title = {A Computational Logic}, Year = {1979} } @Article{Brauer93, Author = {Brauer, Wilfried}, Title = {{KI} auf dem {W}eg in die {N}ormalit\"at}, Journal = {KI}, Year = 1993, Volume = {Sonderheft}, Pages = {85-91}, Month = aug } @Article{Bretthauer+92, Author = {Bretthauer, Harry and Christaller, Thomas and Friedrich, Horst and Goerigk, Wolfgang and Heicking, Winfried and Hoffmann, Ulrich and Hovekamp, Dieter and Knutzen, Heinz and Kopp, J\"urgen and Kriegel, {E. Ulrich} and Mohr, Ingo and Rosenm\"uller, Rainer and Simon, Friedemann}, Title = {{D}as {V}erbundvorhaben {APPLY}: {E}in modernes und bedarfsgerechtes {L}isp}, Journal = {KI}, Year = 1992, Volume = 2, Pages = {50-54}, Month = jun } @techreport{Bretthauer+94, Author = {Bretthauer, Harry and Christaller, Thomas and Friedrich, Horst and Goerigk, Wolfgang and Heicking, Winfried and Hoffmann, Ulrich and Kind, Andreas and Klude, Bert and Knutzen, Heinz and Kopp, J\"urgen and Kriegel, E. Ulrich and Mohr, Ingo and Rosenm\"uller, Rainer and Simon, Friedemann}, Title = {{V}on der {APPLY}-{M}ethodik zum {S}ystem}, Institution = {CAU/GMD/ISST/VW-GEDAS}, Type = {Abschlu\ss bericht des BMFT-Projektes APPLY}, Number = {APPLY/XIII/10}, Address = {Sankt Augustin}, Year = 1994, Month = jun } @Inproceedings{Brown+92, Author = {D. F. Brown and H. Moura and D. A. Watt}, Title = {Actress: an Action Semantics Directed Compiler Generator}, Series = {Lecture Notes in Computer Science}, Volume = {641}, BookTitle = {Compiler Compilers 92}, Year = {1992} } @TechReport{Broy92, Author = {M. Broy}, Institution = {Digital Systems Research Center}, Title = {Experiences with Software Specification and Verification using {LP}, the Larch Proof Assistant}, Number = {93}, Address = {Palo Alto}, Month = jul, Year = {1992} } @Misc{BSI94, Author = {{BSI-Bundesamt f\"ur Sicherheit in der Informationstechnik}}, Title = {{BSI-Zertifizierung}}, Howpublished = {BSI 7119, Bonn}, Year = {1994} } @BOOK{Burghardt93, Author = {J. Burghardt}, Title = {Eine feink{\"o}rnige Sortendisziplin und ihre Anwendung in der Programmkonstruktion}, Series = {GMD--Berichte}, Volume = {212}, Publisher = {Oldenbourg-Verlag}, Year = {1993} } @Inproceedings{Burkart+91, Author = {Burkart, O. and Goerigk, W. and Knutzen, H.}, Title = {{CLiCC}: {A} {N}ew {A}pproach to the {C}ompilation from {C}ommon {L}isp {P}rograms to {C}}, BookTitle = HONNEF, Address = {Bericht Nr.\ 8/91-I des Instituts f\"ur angewandte Mathematik und Informatik der Univ.\ M\"unster}, Year = 1991 } @MastersThesis{Burkart91, Author = {Burkart, Olaf}, Title = {{D}as {F}rontend {e}ines {C}ompilers {v}on {Common Lisp} {n}ach {C}}, School = CAUIfIuPM, Address = {{K}iel}, Year = 1991 } @Article{Burn+86, Author = {Burn, G. and Hankin, C. and Abramsky, S}, Title = {Strictness analysis for higher order functions}, Journal = {Sci. Comput. Programm.}, Volume = {7}, Pages = {249--278}, Year = {1986} } @INCOLLECTION{Burstall/Landin69, Author = {R. M. Burstall and P.J. Landin}, Title = {Programs and their proofs: an algebraic approach}, BookTitle = {Machine Intelligence 4}, Editor = {B. Meltzer and D. Michie}, Publisher = {Edinburgh University Press}, Year = {1969} } @Inproceedings{Buth+92, Author = {B. Buth and K.-H. Buth and M. Fr\"anzle and {B. v.} Karger and Y. Lakhneche and H. Langmaack and M. M\"uller-Olm}, Title = {Provably correct compiler development and implementation}, Editor = {U. Kastens and P. Pfahler}, BookTitle = {Compiler Construction}, Series = LNCS, Volume = {641}, Publisher = SPRINGER, Year = {1992} } @Inproceedings{Buth/Mueller-Olm93, Author = {Bettina Buth and Markus M\"uller-Olm}, Title = {{P}rovably {C}orrect {C}ompiler {I}mplementation}, Pages = {451--465}, BookTitle = {{T}utorial {M}aterial -- {F}ormal {M}ethods {E}urope '93}, Year = 1993, Organization = {IFAD Odense Teknikum}, Address = {Denmark}, Month = apr } @InCollection{Buth92b, Author = {{K.-H.} Buth}, Title = {Using SOS Definitions in Term Rewriting Proofs}, BookTitle = {First International Workshop on Larch, Dedham 1992}, Publisher = SPRINGER, Editor = {Ursula Martin and Jeanette M. Wing}, Year = {1993}, Series = {Workshops in Computing}, Pages = {36--54} } @Inproceedings{Cardelli84, Author = {Cardelli, L.}, Editor = {Kahn, G. and MacQueen, {D.B.} and Plotkin, G.}, Title = {A {S}emantics of {M}ultiple {I}nheritance}, BookTitle = {Intern. Symposium on Semantics of Data Types, Lecture Notes in Computer Science No. 173}, Publisher = SPRINGER, Pages = {51--68}, Address = {Berlin, Heidelberg, New York}, Year = 1984 } @Article{Chirica/Martin86, Author = {Chirica, {L.M.} and Martin, {D.F.}}, Title = {{Toward Compiler Implementation Correctness Proofs}}, Journal = {ACM Transactions on Programming Languages and Systems}, Volume = {8}, Number = {2}, Month = apr, Pages = {185--214}, Year = 1986 } @Book{Christaller+89, Editor = {Christaller, Th. and diPrimio, F. and Vo{\ss}, A.}, Title = {Die {KI--W}erkbank {BABYLON}}, Publisher = AW, Address = {Bonn}, Year = 1989 } @Book{Christaller+92, Author = {Thomas Christaller and Franco di Primio and Uwe Schnepf and Angi Vo{\ss}}, Title = {The {AI-Workbench BABYLON} --- an Open and Portable Development Environment for Expert Systems}, Publisher = {Academic Press}, Address = {New York, USA}, Year = 1992 } @Inproceedings{Cohn79a, Author = {A. Cohn}, BookTitle = {Proceedings of the Fifth Symposium on Automated Deduction}, Title = {High Level Proof in LCF}, Year = {1979} } @PhDThesis{Cohn79b, Author = {A. Cohn}, School = {University of Edinburgh}, Title = {Machine Assisted Proofs of Recursion Implementation}, Year = {1979} } @Book{Constable+86, Author = {R. L. {Constable et al.}}, Publisher = {Prentice-Hall}, Title = {Implementing Mathematics with the Nuprl Proof Development System}, Year = {1986} } @Article{Cooper72a, Author = {D.C. Cooper}, Journal = {Machine Intelligence}, Pages = {91-99}, Title = {Theorem Proving in arithmetic without multiplication}, Volume = {7}, Year = {1972}, Category = {DecisionProcedures} } @Article{Coquand+94, Author = {T. Coquand and B. Nordstr\"om and J.M. Smith and B. von Sydow}, Journal = {EATCS}, Note = {FTP: waldorf.cs.chalmers.se}, Title = {Type Theory and Programming}, Year = {1994} } @Article{Coquand/Huet88, Author = {T. Coquand and G. Huet}, Journal = {Information and Computation}, Number = {2/3}, Pages = {95--120}, Title = {The {C}alculus of {C}onstructions}, Volume = {76}, Year = {1988} } @Inproceedings{Cousot/Cousot77, Author = {P. Cousot and R. Cousot}, Title = {Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints}, Booktitle = {Proceedings 4th ACM Symposium Principles of Programming Languages}, Pages = {238--252}, Year = {1977} } @Article{Curzon93a, Author = {Paul Curzon}, Title = {{D}eriving {C}orrectness {P}roperties of {C}ompiled {C}ode}, Journal = {Formal Methods in System Design}, Volume = 3, Pages = {83--115}, Month = aug, Year = 1993 } @Unpublished{Curzon94, Author = {Paul Curzon}, Title = {{T}he {V}erified {C}ompilation of {V}ista {P}rograms}, Note = {Internal Report, Computer Laboratory, University of Cambridge}, Address = {Cambridge, UK}, Year = 1994, Month = jan } @Article{Davidson/Fraser80, Author = {Davidson, J. W. and Fraser, C. W.}, Title = {The Design and Application of a Retargetable Peephole Optimizer}, Journal = {ACM Transactions on Programming Languages and Systems}, Volume = {2}, Number = {2}, Month = apr, Year = {1980}, Pages = {191--202} } @Incollection{Dershowitz/Jouanaud90, Author = {N. Dershowitz and {J.-P.} Jouanaud}, Title = {Rewrite Systems}, BookTitle = {Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics}, Editor = {J. van Leeuwen}, Publisher = {Elsevier}, Year = {1990}, Pages = {245--320} } @PhDThesis{Diehl96, Author = {Diehl, Stephan}, Title = {{Semantics-Directed Generation of Compilers and Abstract Machines}}, School = {Universit\"at des Saarlandes}, Address = {Saarbr\"ucken}, Year = 1996 } @InProceedings{Dijkstra98, Author = {{Rutger M.} Dijkstra}, Title = "Computation Calculus -- Bridging a formalisation gap", Publisher = "Springer Verlag", Year = 1998, Editor = {J. Jeurig}, Series = LNCS, Volume = {1422}, BookTitle = {Proceedings Mathematics of Program Construction '98} } @Book{Dijkstra76, Author = "Edsger W. Dijkstra", Title = "A Discipline of Programming", Publisher = "Prentice-Hall", Year = 1976 } @Book{Dijkstra/Scholten90, Author = {Edsger W. Dijkstra and {Carol S.} Scholten}, Title = "Predicate Calculus and Program Semantics", Publisher = "Springer Verlag", Address = {Berlin, Heidelberg, New York}, Series = {Texts and Monographs in Computer Science}, Year = 1990 } @TechReport{Dold+92, Author = {A. Dold and {F.W. von} Henke and H. Rue{\ss} and D. Schwier and M. Strecker}, Institution = {Universit{\"a}t Ulm}, Number = {93--06}, Title = {Korso {A}ufgabe: {I}mplementierung von {M}engen mit {H}ilfe von {S}equenzen}, Type = {Korso Study Note}, Year = {1993} } @TechReport{Dold93, Author = {A. Dold}, Institution = {Universit{\"a} Ulm}, Number = {93--2}, Title = {Formalisierung {S}chematischer {A}lgorithmen}, Type = {Korso Study Note}, Year = {1993} } @TechReport{Dold94, Author = {A. Dold}, Institution = {Universit{\"a}t Ulm}, Number = {94-01}, Title = {Program {D}evelopment with {S}pecification {O}perators}, Type = {Korso Study Note}, Year = {1994} } @TechReport{Dold+95, Author = {Axel Dold and {F.W. von} Henke and H. Pfeifer and H. Rue{\ss}}, Title = {{A Generic Specification for Verifying Peephole Optimizations}}, Institution = {Universit{\"a}t Ulm}, Year = {1995}, Number = {95-14}, Type = {Ulmer Informatik-Berichte} } @TechReport{Dold+96, Author = {Dold, Axel and Goerigk, Wolfgang and M\"uller-Olm, Markus and R\"uhle, J\"urgen}, Title = {{Erhaltung partieller Korrektheit bei Maschinenressourcenbeschr\"ankungen: Korrektheitsbeweis und Formalisierung in PVS}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU-Ulm/2.3}, Year = {1996}, Note = {In Vorbereitung} } @TechReport{Dold+96b, Author = {Dold, Axel and Gaul, Thilo and Goerigk, Wolfgang and Goos, Gerhard and Heberle, Andreas and {von Henke}, Friedrich and Hoffmann, Ulrich and Langmaack, Hans and M\"uller-Olm, Markus and Pfeifer, Holger and Rue{\ss}, Harald and Zimmermann, Wolf}, Title = {{Zwischenbericht Verifix}}, Institution = {Uni Karlsruhe, Kiel, Ulm}, Number = {Verifix/UKA/1.60}, Year = {1996}, } @Inproceedings{Drossopoulou+82, Author = {Sophia Drossopoulou and Gerhard Goos and Guido Persch and Manfred Dausmann and Georg Winterstein}, Title = {An Attribute Grammar for Ada}, Year = {1982}, Volume = {17:6}, BookTitle = {Compiler Construction Conference}, Pages = {334 -- 349} } @Inproceedings{Dybjer85, Author = {Dybjer, P.}, Title = {Using Domain Algebras to prove the correctness of a compiler}, BookTitle = {2nd Annual Symposium on Theoretical Aspects of Computer Science STACS}, Series = LNCS, Volume = {182}, Pages = {98--108}, Year = {1985} } @Inproceedings{Emmelmann+88, Author = {H. Emmelmann and F.-W. Schr\"oer and R. Landwehr}, Title = {BEG - a Generator for Efficient Back Ends}, BookTitle = {ACM Proceedings of the Sigplan Conference on Programming Language Design and Implementation}, Month = jun, Year = {1989} } @Inproceedings{Emmelmann92, Author = {H. Emmelmann}, Title = {Code Selection by regularly controled term rewriting}, Editor = {R. Giegerich and S.L. Graham}, BookTitle = {Code Generation - Concepts, Tools, Techniques}, Series = {Workshops in Computing}, Publisher = SPRINGER, Year = {1992} } @Inproceedings{Farmer+91, Author = {William M. Farmer and Joshua D. Guttman and F. Javier Thayer}, BookTitle = {CADE-11}, Publisher = {Springer LNCS 607}, Title = {Little Theories}, Year = {1991} } @Article{Farmer+93, Author = {William M. Farmer and Joshua D. Guttman and F. Javier Thayer}, Journal = {J. of Automated Reasoning}, Pages = {213-248}, Title = {{IMPS}: An Interactive Mathematical Proof System}, Volume = {11}, Year = {1993} } @MastersThesis{Frank90, Author = {Frank, Karsten}, Title = {{E}ine {g}emeinsame {A}bstrakte {M}aschine {f}\"ur {PROLOG} {u}nd {LISP}}, School = CAUIfIuPM, Address = {{K}iel}, Year = 1990 } @TechReport{GMD87, Author = {GMD, Forschungsgruppe ``Expertensysteme''}, Title = {{BABYLON}--{R}eferenzhandbuch {V.} 1.1/1}, Institution = {Gesellschaft f\"ur Mathematik und Datenverarbeitung (F3)}, Address = {St. Augustin}, Year = 1987 } @TechReport{Gallier92, Author = {Jean Gallier}, Address = {From: ftp.cis.upenn.edu}, Institution = {University of Pensylvania}, Title = {Constructive Logics. Part I: A Tutorial on Proof Systems and Typed Lambda-Calculus}, Year = {1992} } @TechReport{Garland/Guttag91, Author = {{S.J.} Garland and {J.V.} Guttag}, Institution = {Digital systems Research 'Center}, Number = {SRC Report 82}, Pages = {137--151}, Publisher = SPRINGER, Title = {A Guide to LP, The LARCH Prover}, Year = {1991} } @Inproceedings{Gaudel95, Author = {{M.-C.} Gaudel}, Title = {{A}dvantages and {L}imits of {F}ormal {A}pproaches for {U}ltra-{H}igh {D}ependability}, BookTitle = {Proc. Predictably Dependable Computing Systems, Esprit Basic Research Series}, Editor = {B. Randell and {J.-C.} Laprie and H. Kopetz and B. Littlewood}, Publisher = SPRINGER, Pages = {241--252}, Year = 1995 } @InProceedings{Gaul+96, Author = {Th. Gaul and G. Goos and A. Heberle and W. Zimmermann and W. Goerigk}, Title = {{An Architecture for Verified Compiler Construction}}, Address = {Linz, Austria}, BookTitle = {{J}oint {M}odular {L}anguages {C}onference JMLC'97}, Month = mar, Year = 1997 } @Book{Gentzen34, Author = {Gerhard Gentzen}, Publisher = {Wissenschaftliche Buchgesellschaft Darmstadt}, Title = {Untersuchungen \"uber das logische Schlie{\ss}en}, Year = {1934} } @Article{Goodenough/Gerhart75, Author = {{J.B.} Goodenough and {S.L.} Gerhart}, Title = {{T}oward a {T}heory of {T}est {D}ata {S}election}, Journal = {SIGPLAN Notices}, Number = 6, Volume = 10, Month = jun, Pages = {493--510}, Year = 1975 } @TechReport{Goerigk/Hoffmann97, Author = {Goerigk, Wolfgang and Hoffmann, Ulrich}, Title = {{The Compiling Specification from ComLisp to Executable Machine Code}}, Type = {Technical Report}, Institution = CAUIfIuPM, Number = {Nr. 9713}, Year = 1998, Month = dec, Address = {Kiel} } @TechReport{Goerigk/Hoffmann96, Author = {Goerigk, Wolfgang and Hoffmann, Ulrich}, Title = {{T}he {C}ompiler {I}mplementation {L}anguage {ComLisp}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/1.7}, Year = {1996}, Month = jun, } @TechReport{Goerigk/Mueller-Olm96, Author = {Goerigk, Wolfgang and M\"uller-Olm, Markus}, Title = {{Erhaltung partieller Korrektheit bei beschr\"ankten Maschinenressourcen. -- Eine Beweisskizze --}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/2.5}, Year = {1996}, } @Inproceedings{Goerigk/Simon91, Author = {Goerigk, W. and Simon, F.}, Title = {{Z}ielsetzungen im {V}erbundvorhaben {APPLY}}, BookTitle = HONNEF, Address = {Bericht Nr.\ 8/91-I des Instituts f\"ur angewandte Mathematik und Informatik der Univ.\ M\"unster}, Year = 1991 } @Article{Goerigk/Simon93, Author = {Goerigk, Wolfgang and Simon, Friedemann}, Title = {{M}igration und {K}ompilation in {L}isp: {E}in {W}eg von {P}rototypen zu {A}nwendungen}, Journal = {Proc. Workshop ``Neuere Entwicklungen der deklarativen KI-Programmierung''}, Year = 1993, Volume = {DFKI Research Report RR-93-35}, Pages = {31-52}, Month = sep } @Inproceedings{Goerigk/Simon98, Author = {Goerigk, Wolfgang and Simon, Friedemann}, Title = {{Towards Rigorous Compiler Implementation Verification}}, BookTitle = {Proceedings of the VIM Spring and Winter Workshops}, Editor = {Julian Padget}, Year = 1998, Publisher = {Springer Verlag}, Address = {Berlin, Heidelberg, New York}, Series = {Lecture Notes in Computer Science}, Note = {To appear} } @Inproceedings{Goerigk89a, Author = {Goerigk, W.}, Title = {Semantik {und \"U}bersetzung {o}bjektorientierter {W}issensrepr\"asentationssprachen}, BookTitle = HONNEF, Address = {Bad Honnef}, Year = 1989 } @Inproceedings{Goerigk89b, Author = {Goerigk,W.}, Editor = {Dosch, W.}, Title = {Zur {K}orrektheit {eines \"U}bersetzers f\"ur {o}bjektorientierte {S}prachen: {E}in {B}eweisansatz}, BookTitle = {Arbeitstreffen {\em {F}unktionale und logische {P}rogrammierung -- {S}prachen, {M}ethoden, {I}mplementationen}}, Address = {{I}nstitut f\"ur {M}athematik der {U}niversit\"at {A}ugsburg}, Pages = {8--20}, Year = 1989 } @PhDThesis{Goerigk93, Author = {Goerigk, Wolfgang}, Title = {{K}orrektheit {der \"U}bersetzung {o}bjektorientierter {W}issensrepr\"asentationssprachen {m}it {s}tatischer {V}ererbung}, School = {Math.-Nat. Fakult\"at der Christian-Albrechts-Universit\"at zu Kiel}, Address = {{K}iel}, Year = 1993 } @Inproceedings{Goerigk95, Author = {Wolfgang Goerigk}, Title = {{O}n the {C}orrectness of {C}ompilers and {C}ompiler {I}mplementations}, BookTitle = HONNEF, Address = {Bad Honnef}, Year = 1995 } @TechReport{Goerigk95b, Author = {Goerigk, Wolfgang}, Title = {{Transputer State and Instruction Set Specification and Initial Boot Protocol}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/2.1}, Year = {1995}, Month = jul, } @Misc{Goerigk96a, Author = {Wolfgang Goerigk}, Title = {{C}ompiler {I}mplementation {V}erification: {T}owards {C}orrectness of {B}inary {M}achine {P}rograms}, Address = {Wien}, Howpublished = {submitted to SAFECOMP'96 International Conference on Computer Safety, Reliability and Security}, Year = 1996 } @TechReport{Goerigk96b, Author = {Goerigk, Wolfgang}, Title = {{An Exercise in Program Verification: The ACL2 Correctness Proof of a Simple Theorem Prover Executable}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/2.4}, Year = {1996}, } @TechReport{Goerigk97b, Author = {Goerigk, Wolfgang}, Title = {{A Denotational Semantics for ComLisp and SIL}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/2.8}, Month = dec, Year = {1997}, } @Inproceedings{Goerigk97c, Author = {Wolfgang Goerigk}, Title = {{Towards Rigorous Compiler Implementation Verification}}, BookTitle = HONNEF, Pages = {28 -- 36}, Address = {Bad Honnef}, Year = 1997 } @Inproceedings{Goerigk97d, Author = {Wolfgang Goerigk}, Title = {{Towards Rigorous Compiler Implementation Verification}}, BookTitle = {Proc. of the 1997 Workshop on Programming Languages and Fundamentals of Programming}, Editor = {Rudolf Berghammer and Friedemann Simon}, Pages = {118 -- 126}, Address = {Avendorf, Germany}, Month = nov, Year = 1997 } @InProceedings{Goerigk+96, Author = {Wolfgang Goerigk and Axel Dold and Thilo Gaul and Gerhard Goos and Andreas Heberle and {Friedrich W. von} Henke and Ulrich Hoffmann and Hans Langmaack and Holger Pfeifer and Harald Ruess and Wolf Zimmermann}, Title = {{C}ompiler {C}orrectness and {I}mplementation {V}erification: {T}he {{\em {V}erifix}} {A}pproach}, Editor = {P. Fritzson}, Address = {IDA Technical Report LiTH-IDA-R-96-12, Link{\o}ping, Sweden}, BookTitle = {Proceedings of the Poster Session of CC '96 -- International Conference on Compiler Construction}, Pages = {65 -- 73}, Year = 1996 } @Article{Goerigk+96b, Author = {Wolfgang Goerigk and Harold Boley and Ulrich Hoffmann and Markus Perling and Michael Sintek}, Title = {{Komplettkompilation von Lisp: Eine Studie zur \"Ubersetzung von Lisp-Software f\"ur C-Umgebungen}}, Journal = {KI}, Number = {2}, Volume = {10}, Publisher = {Interdata Verlags GmbH}, Year = {1996} } @TechReport{Goerigk+96c, Author = {Goerigk, Wolfgang and Meyer, Thies and Pfeifer, Holger and R\"uhle, J\"urgen}, Title = {{Boot Loader Correctness: The Transputer Boot Program and its Correctness Proof in PVS}}, Institution = {CAU Kiel, Universit\"at Ulm}, Type = {Technical Report}, Number = {Verifix/CAU-Ulm/2.2}, Year = {1996}, Note = {In Vorbereitung} } @TechReport{Goerigk+97a, Author = {Goerigk, Wolfgang and Hoffmann, Ulrich and Langmaack, Hans}, Title = {{Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU-Ulm/2.6}, Year = {1997}, Month = jan, } @InProceedings{Goerigk+98, Author = {Goerigk, Wolfgang and Gaul, Thilo and Zimmermann, Wolf}, Title = {{Correct Programs without Proof? On Checker-Based Program Verification}}, Year = {1998}, Address = {Malente}, Booktitle = {Proceedings ATOOLS'98 Workshop on ``Tool Support for System Specification, Development, and Verification''}, Series = {Advances in Computing Science}, Publisher = {Springer Verlag} } @InProceedings{Goerigk+98b, Author = {Goerigk, Wolfgang and Zimmermann, Wolf and Gaul, Thilo and Heberle, Andreas and Hoffmann, Ulrich}, Title = {{Praktikable Konstruktion {korrekter \"U}bersetzer}}, Series = {Softwaretechnik-Trends}, Volume = {18(3)}, Pages = {26 -- 34}, Year = {1998}, Address = {Paderborn}, Booktitle = {Proceedings Softwaretechnik ST'98} } @InProceedings{Goerigk/Hoffmann98, Author = {Goerigk, Wolfgang and Hoffmann, Ulrich}, Title = {{Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct}}, Year = {1998}, Series = LNCS, Address = {Boppard}, BookTitle = {Proceedings FM-TRENDS'98 International Workshop on Current Trends in Applied Formal Methods}, Note = {To appear} } @TechReport{Goerigk/Hoffmann98b, Author = {Goerigk, Wolfgang and Hoffmann, Ulrich}, Title = {{Compiling ComLisp to Executable Machine Code: Compiler Construction}}, Type = {Technical Report}, Institution = CAUIfIuPM, Number = {Nr. 9812}, Year = 1998, Month = oct } @Book{Goldberg/Robson83, Author = {Goldberg, A. and Robson, D.}, Title = {Smalltalk--80: The {L}anguage and its {I}mplementation}, Publisher = AW, Address = {Reading, MA}, Year = 1983 } @Article{Goos/Winterstein80, Author = {Gerhard Goos and Georg Winterstein}, Title = {Towards a Compiler Front-End for Preliminary Ada}, Year = {1980}, Journal = {SIGPLAN Notices}, Volume = {15}, Number = {11}, Pages = {36 -- 46} } @Article{Goos81, Author = {Gerhard Goos}, Title = {Problems in Compiling Ada}, Year = {1981}, Journal = {|LNCS|}, Volume = {123}, Pages = {173 -- 199} } @Misc{Goos+94, Author = {Gerhard Goos and Hans Langmaack and {F.W. von} Henke and Wolfgang Goerigk and Wolf Zimmermann}, Title = {{Verifizierte \"U}bersetzer ({{\em {Verifix}\/}})}, Year = {1994}, Address = {Karlsruhe, Kiel, Ulm}, Howpublished = {DFG-Projektantrag. Karlsruhe, Kiel, Ulm} } @Inproceedings{Grosch/Emmelmann90, Author = {J. Grosch and H. Emmelmann}, Title = {A toolbox for compiler construction}, BookTitle = {Compiler Compilers}, Year = {1990}, Series = LNCS, Volume = {477}, Publisher = SPRINGER } @Article{Gurevich91, Author = {Y. Gurevich}, Title = {{E}volving {A}lgebras; {A} {T}utorial {I}ntroduction}, Journal = {Bulletin EATCS}, Year = {1991}, Volume = {43}, Pages = {264--284} } @Inproceedings{Gurevich95, Author = {Y. Gurevich}, Title = {{E}volving {A}lgebras: {L}ipari {G}uide}, Editor = {E. B\"orger}, BookTitle = {Specification and Validation Methods}, Publisher = {Oxford University Press}, Year = {1995}, } @Inproceedings{Gurevich/Huggins93, Author = {Y. Gurevich and J. Huggins}, Title = {{T}he {S}emantics of the {C} {P}rogramming {L}anguage}, Volume = 702, Series = {LNCS}, Pages = {274--308}, BookTitle = {{CSL} '92}, Publisher = Springer, Year = 1993 } @TechReport{Guttman+92, Author = {{J. D.} Guttman and {L. G.} Monk and {J. D.} Ramsdell and {W. M.} Farmer and V. Swarup}, Title = {{A} {G}uide to {VLisp}, {A} {V}erified {P}rogramming {L}anguage {I}mplementation}, Institution = {The MITRE Corporation}, Type = {Technical Report}, Number = {M92B091}, Address = {Bedford, MA}, Month = sep, Year = 1992 } @PhDThesis{Habel92, Author = {Annegret Habel}, Title = {Hyperedge Replacement: Grammars and Languages}, school = {{Universit\"at Bremen}}, Year = {1992}, note = {Springer Verlag. LNCS 643} } @Article{Hannan94, Author = {Hannan, John}, Title = {{Operational Semantics-Directed Compilers and Machine Architectures}}, Journal = {ACM Transactions on Programming Languages and Systems}, Volume = {16}, Number = {4}, Month = jul, Pages = {1215-1247}, Year = 1994 } @Inproceedings{Hannan/Pfenning92, Author = {John Hannan and Frank Pfenning}, Address = {Santa Cruz, California}, BookTitle = {Seventh Annual {IEEE} Symposium on Logic in Computer Science}, Key = {Hannan92}, Month = jun, Note = {Preliminary version available as {POP} Report 91--003, School of Computer Science, Carnegie Mellon University}, Pages = {407--417}, Publisher = {IEEE Computer Society Press}, Title = {Compiler Verification in {LF}}, Year = {1992} } @Misc{Heberle+98, Author = {Andreas Heberle and Thilo Gaul and Wolfgang Goerigk and Gerhard Goos and Wolf Zimmermann}, Title = {{Construction of Verified Compiler Front-Ends with Program-Checking}}, Howpublished = {submitted to PSI'99 International Conference on Perspectives of System Informatics}, Year = 1999 } @InProceedings{He+93, Author = {{He Jifeng} and I. Page and J. P. Bowen}, Title = {{Towards a provably correct hardware implementation of {Occam}}}, Editor = {{G. J.} Milne and L. Pierre}, Booktitle = {Correct Hardware Design and Verification Methods (CHARME'93)}, Other = {Proc.\ IFIP WG10.2 Advanced Research Working Conference}, Location = {Arles, France, 24--26 May 1993}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Volume = {683}, Pages = {214--225}, Year = {1993}, Other = {Based on ProCoS document [OU HJF 9]} } @Inproceedings{Hennessey92, Author = {Hennessey, W.}, Title = {{WCL}: {D}elivering {E}fficient {C}ommon {L}isp {A}pplications under {U}nix}, BookTitle = {Proc. of the 1992 ACM Conference on Lisp and Functional Programming}, Pages = {260-269}, Address = {San Francisco, CA}, Year = 1992 } @Article{Hoare/Lauer74, Author = {{C.A.R.} Hoare and {P.E.} Lauer}, Title = {Consistent and Complementary Formal Theories of the Semantics of Programming Languages}, Journal = {Acta Informatica}, Year = {1974}, Volume = {3}, Pages = {135-154} } @Article{Hoare69, Author = {C. A. R. Hoare}, Title = {An axiomatic basis for computer programming}, Journal = CACM, Volume = {12}, Pages = {576--583}, Year = {1969} } @Inproceedings{Hoare91, Author = {C. A. R. Hoare}, Title = {Refinement algebra proves correctness of compiling specifications}, Editor = {{C.C.} Morgan and {J.C.P.} Woodcock}, BookTitle = {3rd Refinement Workshop}, Publisher = SPRINGER, Pages = {33--48}, Year = {1991} } @Article{Hoare+93, Author = {{C.A.R.} Hoare and He Jifeng and A. Sampaio}, Title = {{N}ormal {F}orm {A}pproach to {C}ompiler {D}esign}, Journal = {Acta Informatica}, Volume = {30}, Pages = {701--739}, Year = {1993} } @manual{Huet+93, Author = {G. {Huet et al.}}, Edition = {5.8}, Key = {Coq93}, Month = nov, Note = {FTP: von ftp.inria.fr}, Organization = {INRIA-Rocquencourt}, Title = {The {Coq} Proof Assistant, User's Guide}, Year = {1993} } @TechReport{Hoffmann95a, Author = {Hoffmann, Ulrich}, Title = {{\"Uberblick \"uber die \"Ubersetzung von der Compiler-Implementierungssprache {\sc ComLisp} in den Maschinencode TC des Transputers }}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/1.1}, Year = {1995}, Month = jun, } @TechReport{Hoffmann95b, Author = {Hoffmann, Ulrich}, Title = {{Die \"Ubersetzerimplementierungssprache {\sc ComLisp}}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/1.2}, Year = {1995}, Month = jun, } @TechReport{Hoffmann95c, Author = {Hoffmann, Ulrich}, Title = {{Die \"Ubersetzerzwischensprache Cop}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/1.3}, Year = {1995}, Month = jun, } @TechReport{Hoffmann95d, Author = {Hoffmann, Ulrich}, Title = {{Die \"Ubersetzerzwischensprache {\sc intermediateC}}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/1.4}, Year = {1995}, Month = jun, } @TechReport{Hoffmann95e, Author = {Hoffmann, Ulrich}, Title = {{Die Assemblersprache {\sc TASM} des Transputers}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/1.5}, Year = {1995}, Month = jun, } @TechReport{Hoffmann96a, Author = {Hoffmann, Ulrich}, Title = {{Die \"Ubersetzung von {\sc intermediateC} in den Assemblercode {\sc Tasm} des Transputers}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/1.6}, Year = {1996}, Month = jun, } @TechReport{Hoffmann96b, Author = {Hoffmann, Ulrich}, Title = {{Die \"Ubersetzung von {\sc ComLisp} in die Compiler--Zwischensprache Cop}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/1.8}, Year = {1996}, Month = jun, } @TechReport{Hoffmann96c, Author = {Hoffmann, Ulrich}, Title = {{Die \"Ubersetzung von Cop nach {\sc intermediateC}}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/1.9}, Year = {1996}, Month = jun, } @Inproceedings{Hoffmann96d, Author = {Hoffmann, Ulrich}, Title = {{\"Uber die korrekte Implementierung von Compilern}}, BookTitle = HONNEF, Address = {Bad Honnef}, pages = {94--105}, Year = 1996, note = {Also available as Technical Report Verifix/CAU/3.1} } @TechReport{Hoffmann96f, Author = {Hoffmann, Ulrich}, Title = {{Das \"Ubersetzerprogramm von {\sc ComLisp} nach Cop}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/1.10}, Year = {1996}, Month = jun } @TechReport{Hoffmann96g, Author = {Hoffmann, Ulrich}, Title = {{Das \"Ubersetzerprogramm von Cop nach {\sc intermediateC}}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/1.11}, Year = {1996}, Month = jun } @TechReport{Hoffmann96h, Author = {Hoffmann, Ulrich}, Title = {{Korrekte Programmkonstruktion in {\sc ComLisp}}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/1.12}, Year = {1996}, Month = jun } @TechReport{Hoffmann96i, Author = {Hoffmann, Ulrich}, Title = {{Das \"Ubersetzerprogramm von {\sc intermediateC} nach {\sc Tasm}}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/1.13}, Year = {1996}, Month = jun } @TechReport{Hoffmann96j, Author = {Hoffmann, Ulrich}, Title = {{Das \"Ubersetzerprogramm von {\sc Tasm} nach {\sc TC}}}, Institution = {CAU Kiel}, Type = {Technical Report}, Number = {Verifix/CAU/1.6}, Year = {1996}, Month = jun } @InCollection{Hoffmann97, author = "Ulrich Hoffmann", booktitle = "Arbeitstagung Programmiersprachen", editor = "Herbert Kuchen", publisher = {Westf\"alische Wilhelms-Universit\"at M\"unster}, title = {{Korrekte Implementierung von \"Uber\-set\-zungs\-spezi\-fi\-ka\-tio\-nen in hoher Programmiersprache}}, year = 1997, series = {Arbeitsbericht des Institutes f\"ur Wirtschaftsinformatik}, volume = 58, pages = "13--20", scope = "trans", } @Inproceedings{Hoffmann97b, Author = {U.\ Hoffmann}, Title = {{Correct Implementation of Compiler Programs}}, BookTitle = {Workshop on Programming Languages and Fundamentals of Programming, Avendorf September 1997}, editor = {Rudolf Berghammer and Friedemann Simon}, series = {Technical Report 9717}, year = 1997, publisher = CAUIFIUPM, address = {Kiel}, month = nov, pages = {127--138}, } @InProceedings{Hoffmann98, Author = {Hoffmann, Ulrich}, Title = {{Towards a Trusted Tool-Chain for Software Development}}, Year = {1998}, Address = {Malente (Germany)}, Booktitle = {Proceedings ATOOLS'98 Workshop on ``Tool Support for System Specification, Development, and Verification''}, Editor = {Rudolf Berghammer and Yassine Lakhneche}, Series = {Advances in Computing Science}, Publisher = SPRINGER, Note = {Submitted for Publication} } @PhDThesis{Hoffmann98b, Author = {Hoffmann, Ulrich}, Title = {{Compiler Implementation Verification through Rigorous Syntactical Code Inspection}}, School = {Technische Fakult\"at der Christian-Albrechts-Universit\"at zu Kiel}, Address = {{K}iel}, Year = 1998 } @TechReport{Hoffmann/Pfeifer96, Author = {Ulrich Hoffmann and Holger Pfeifer}, Title = {{Formalisierung der \"Ubersetzung von C$^{\mbox{\rm int}}$ nach {\sc TASS} und ihr mechanischer Korrektheitsbeweis}}, Institution = {CAU Kiel, Universit\"at Ulm}, Type = {Technical Report}, Number = {Verifix/CAU-Ulm/1.1}, Year = {1996}, Note = {In Vorbereitung} } @Manual{Inmos88, Title = {Transputer instruction set: {A} compiler writer's guide}, Publisher = {Prentice Hall}, Organization = {Inmos Limited}, Year = 1988 } @Book{Jensen/Wirth75, Author = {K. Jensen and N. Wirth}, Title = {{PASCAL} {U}ser {M}anual and {R}eport}, Publisher = {Springer Verlag}, Year = 1975 } @Book{Jones90, Author = {{C.B.} Jones}, Title = {{Systematic Software Development Using VDM, 2nd ed.}}, Publisher = {Prentice Hall}, Address = {New York, London}, Year = {1990} } @Inproceedings{Jones/Schmidt80, Author = {Jones, {N. D.} and Schmidt, {D. A.}}, Title = {Compiler generation from denotational semantics}, Series = LNCS, Volume = {94}, BookTitle = {Workshop on Semantics Directed Compiler Generation}, Year = {1980} } @TechReport{Joyce89, Author = {J.J. Joyce}, Address = {New Museums Site, Pembroke Street, Cambridge, CB2 3QG, England}, Institution = {University of Cambridge}, Month = mar, Number = {167}, Title = {A verified compiler for a Verified Microprocessor}, Year = {1989} } @Inproceedings{Joyce90, Author = {Joyce, {Jeffrey J.}}, Title = {Totally {V}erified {S}ystems: {L}inking {V}erified {S}oftware to {V}erified {H}ardware}, Editor = {Leeser, M. and Brown, G.}, Series = LNCS, Volume = {408}, BookTitle = {Hardware Specification, Verification and Synthesis: Mathematical Aspects}, Year = {1990} } @Inproceedings{Kamin88, Author = {Kamin, S.}, Title = {{I}nheritance in {S}malltalk--80: {A} {D}enotational {A}pproach}, BookTitle = POPL, Pages = {80--87}, Organization = {ACM}, Year = 1988 } @TechReport{Karger92, Author = {{Burghard v.} Karger}, Title = {{D}istinguishing {D}ivergence from {C}haos in {CSP}}, Type = {ProCoS Report}, Institution = {Universit\"at Kiel}, Year = {1992} } @TechReport{Karger93, Author = {{Burghard v.} Karger}, Title = {{A}lgebraic {C}ompiler {V}erification}, Type = {Internal Report}, Institution = {Oxford University Computing Laboratory}, Month = oct, Year = {1993} } @Article{Kastens80, Author = {U. Kastens}, Title = {Ordered Attribute Grammars}, Journal = {Acta Informatica}, Volume = {13}, Number = {3}, Year = {1980}, Pages = {229--256} } @TechReport{Kaufmann/Moore94, Author = {M. Kaufmann and {J S.} Moore}, Title = {{Design Goals of ACL2}}, Institution = {Computational Logic, Inc.}, Type = {Technical Report}, Number = {101}, Month = aug, Year = 1994 } @Book{Keene89, Author = {Keene, {S.E.}}, Title = {Object {O}riented {P}rogramming in {Common Lisp}}, Publisher = AW, Address = {Reading, MA}, Year = 1989 } @Book{Kernighan/Ritchie78, Author = {Kernighan, {B.W.} and Ritchie, {D.M.}}, Title = {{T}he {C} {P}rogramming {L}anguage}, Publisher = {Prentice-Hall}, Address = {Englewoods Cliff, NY}, Year = 1978 } @Book{Kernighan/Ritchie83, Author = {Kernighan, {B.W.} and Ritchie, {D.M.}}, Title = {{P}rogrammieren in {C}}, Publisher = {Hanser Verlag}, Address = {M\"unchen, Wien}, Year = {1983} } @Book{Kersten95, author = {H. Kersten}, title = {{S}icherheit in der {I}nformationstechnik, 2. {A}ufl.}, publisher = {Oldenbourg}, year = {1995}, address = {M\"unchen, Wien} } @Inproceedings{Knemeyer/Schulenburg93, Author = {Knemeyer, U. and {Graf von der Schulenburg}, {J.-M.}}, Editor = {Puppe, F. and G\"unter, A.}, Title = {``{E}xpertensysteme'' - {W}elche {F}aktoren f\"ordern und hemmen die {I}mplementation und {D}iffusion der {T}echnologie in der {V}ersicherungswirtschaft.}, BookTitle = {Expertensysteme '93}, Publisher = {Informatik aktuell, Springer-Verlag}, Address = {Berlin, Heidelberg, New York}, Year = 1993 } @Inproceedings{Knoop+92, Author = {Knoop, J. and R\"uthing, O. and Steffen, B.}, Address = {San Francisco, CA}, BookTitle = {Proc.~} # PLDI #{'92}, Pages = {224 - 234}, Series = SIGPLANNOT, Volume = {{\em 27},7}, Title = {Lazy code motion}, Month = jun, Year = {1992} } @unpublished{Knoop+93a, Author = {Knoop, J. and R\"uthing, O. and Steffen, B.}, Note = {To appear in ~} # TOPLAS #{. Available as MIP-Bericht 9310, Fakult\"at f\"ur Mathematik und Informatik, Universit\"at Passau, 35 pages}, Title = {Optimal Code Motion: {T}heory and Practice}, Year = {1993} } @Article{Knoop+93b, Author = {Knoop, J. and R\"uthing, O. and Steffen, B.}, Journal = JPLDI, Title = {Lazy Strength Reduction}, Year = {1993}, Volume = {1}, Number = {1}, Pages = {71-91}, Publisher = {Chapman \& Hall}, Address = {London, UK}, } @Inproceedings{Knoop+94, Author = {Knoop, J. and R\"uthing, O. and Steffen, B.}, Title = {Partial Dead Code Elimination}, BookTitle = {Proc.~} # PLDI #{'94}, Address = {Orlando, FL}, Month = jun, Year = {1994}, Note = {To appear} } @Inproceedings{Knoop/Steffen92a, Author = {Knoop, J. and Steffen, B.}, Address = {Paderborn, Germany}, BookTitle = {Proc. 4$^{th}$~} # CC, Pages = {125 - 140}, Publisher = SPRINGER, Series = LNCS # {~ 641}, Title = {The Interprocedural Coincidence Theorem}, Year = {1992} } @Inproceedings{Knoop/Steffen92b, Author = {Knoop, J. and Steffen, B.}, Address = {Paderborn, Germany}, BookTitle = {Addenda to Proc. 4$^{th}$~} # CC, Pages = {36 - 39}, Publisher = {Published as Tech. Rep. No. 103, Department of Computer Science, University of Paderborn}, Title = {Optimal interprocedural partial redundancy elimination. {E}xtended abstract}, Year = {1992} } @Inproceedings{Knoop/Steffen92c, Author = {Knoop, J. and Steffen, B.}, Address = {Schlo{\ss} Dagstuhl, Germany}, BookTitle = {Software Construction---Foundation and Application}, Editor = {Langmaack, H. and Neuhold, E. and Paul, M.}, Organization = {Internationales Begegnungs- und Forschungszentrum f\"ur Informatik}, Series = {Dagstuhl-Seminar-Report 29}, Title = {Optimal Interprocedural Data Flow Analysis}, Year = {1992} } @PhDThesis{Knoop93, Author = {Knoop, J.}, Title = {Optimal Interprocedural Program Optimization: {A} new framework and its application}, School = CAUIfIuPM, Year = {1993}, Note = {To appear as monograph in the series {\em Lecture Notes in Computer Science}, Springer-Verlag, Heidelberg, Germany, 1994.} } @unpublished{Knoop94, Author = {Knoop, J.}, Title = {Higher Order Data Flow Analysis}, Note = {Submitted to the {\em IFIP Working Conference on ``Programming Concepts, Methods and Calculi (PROCOMET'94)''}}, Month = jun, Year = {1994}, Address = {San Miniato, Italy} } @MastersThesis{Knutzen91, Author = {Knutzen, Heinz}, Title = {{C}odegenerierung und {L}aufzeitsystem {e}ines {C}ompilers {v}on {Common Lisp} {n}ach {C}}, School = CAUIfIuPM, Address = {{K}iel}, Year = 1991 } @Book{Kock92, Author = {G. Kock}, Title = {Spezifikation und Verifikation von Optimierungsalgorithmen}, Note = {Dissertation an der Universit\"at Karlsruhe}, Publisher = {Oldenburg Verlag}, Year = {1992} } @Inproceedings{Landwehr+82, Author = {Rudolf Landwehr and H.-St. Jansohn and Gerhard Goos}, Title = {Experience with an Automatic Code Generator Generator}, Year = {1982}, Volume = {17:6}, BookTitle = {Compiler Construction Conference}, Pages = {56 -- 66} } @Inproceedings{Lange+96, Author = {Lange, H. and M\"oller, R. and Neumann, B.}, Title = {{Avoiding Combinatorial Explosion in Automatic Test Generation: Reasoning about Measurements is the Key}}, Year = {1996}, Address = {Dresden}, BookTitle = {Proceedings of KI'96 Conference on Artificial Intelligence}, Publisher = {Springer Verlag} } @TechReport{Langmaack89, Author = {Langmaack, H.}, Title = {{\"U}ber {v}ollst\"andig {o}perationell {a}d\"aquate {d}enotationelle {S}emantik {f}unktionaler {P}rogrammiersprachen}, Institution = CAUIfIuPM, Type = {Institutsbericht}, Number = {Nr. 8901}, Address = {Kiel}, Year = 1989 } @Article{Langmaack96a, Author = {Langmaack, H.}, Title = {{The ProCoS Approach to Correct Systems}}, Journal = {Real Time Systems}, Volume = {13}, Pages = {253-275}, Publisher = {Kluwer Academic Publishers}, Year = 1997 } @TechReport{Langmaack96b, Author = {Langmaack, H.}, Title = {{Softwareengineering zur Zertifizierung von Systemen: Spe\-zi\-fi\-ka\-tions-, Imple\-men\-tie\-rungs-, \"Ubersetzerkorrektheit}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/4.1}, Year = {1996}, Month = aug, Note = {Erscheint in Informationstechnik und Technische Informatik it-ti, Oldenbourg Verlag} } @Article{Langmaack97c, Author = {Langmaack, H.}, Title = {{Contribution to Goodenough's and Gerhart's Theory of Software Testing and Verification: Relation between Strong Compiler Test and Compiler Implementation Verification}}, Journal = {Foundations of Computer Science: Potential-Theory-Cognition. LNCS}, Editor = {C. Freksa and M. Jantzen and R. Valk}, Publisher = {Springer Verlag}, Volume = {1337}, Pages = {321-335}, Address = {Berlin, Heidelberg, New York}, Year = 1997 } @Article{Langmaack97a, Author = {Langmaack, Hans}, Title = {{Softwareengineering zur Zertifizierung von Systemen: Spezifikations-, Implementierungs-, \"Ubersetzerkorrektheit}}, Journal = {Informationstechnik und Technische Informatik it-ti}, Pages = {41-47}, Number = 3, Volume = 97, Publisher = {Oldenbourg Verlag}, Year = 1997, } @Article{Langmaack97b, Author = {Langmaack, Hans}, Title = {{Theoretische Informatik ist Grundlage f\"ur das sichere Beherrschen realistischer Software und Systeme}}, Editor = {K. Brunnstein and H. Oberquelle}, Journal = {25 Jahre Informatik an der Universit\"at Hamburg. Informatik: Stand, Trends, Visionen}, HowPublished = {Bericht SBI-HH-B-195/95, Universit\"at Hamburg}, Pages = {47-62}, Year = 1997, } @Misc{Langmaack/Goerigk95, Author = {Hans Langmaack and Wolfgang Goerigk}, Title = {{Technik verifizierter \"U}bersetzerimplementierung ({{\em {VerComp}\/}})}, Year = {1995}, Address = {Kiel}, Howpublished = {DFG-Projektantrag. Kiel} } @Book{Lee89, Author = {P. Lee}, Title = {Realistic Compiler Generation}, Publisher = {MIT Press}, Year = {1989} } @Book{Lippe/Simon90, Author = {Lippe, W. and Simon, F.}, Title = {{A}pplikative {P}rogrammierung}, Publisher = {Lehrbuch, Springer-Verlag}, Address = {Berlin}, Year = {In Vorbereitung} } @Inproceedings{Littlewood/Strigini95, Author = {B. Littlewood and L. Strigini}, Title = {{V}alidation of {U}ltra-{H}igh {D}ependability for {S}oftware-based {S}ystems}, BookTitle = {Proc. Predictably Dependable Computing Systems, Esprit Basic Research Series}, Editor = {B. Randell and {J.-C.} Laprie and H. Kopetz and B. Littlewood}, Publisher = SPRINGER, Pages = {473--494}, Year = 1995 } @Book{Loeckx/Sieber87, Key = {Loeckx \& Sieber}, Author = {Jacques Loeckx and Kurt Sieber}, Title = {{The Foundations of Program Verification (Second edition)}}, Publisher = {John Wiley and Sons}, Year = {1987}, Address = {New York, N.Y.}, Annote = {121 references.}, } @manual{Luo/Pollack92, Author = {Z. Luo and R. Pollack}, Month = may, Organization = {University of Edinburgh}, Title = {{LEGO} Proof Development System: User's Manual}, Year = {1992} } @TechReport{Luo90, Author = {Z. Luo}, Institution = {University of Edinburgh}, Month = jul, Number = {CST-65-90}, Title = {An {E}xtended {C}alculus of {C}onstructions}, Year = {1990} } @Article{Luo91a, Author = {Z. Luo}, Journal = {Information and Computation}, Pages = {107--137}, Title = {A {H}igher-{O}rder {C}alculus and {T}heory {A}bstraction}, Volume = {90}, Year = {1991} } @Inproceedings{Luo91b, Author = {Z. Luo}, BookTitle = {TAPSOFT'91}, Editor = {S. Abramsky and T.S.E. Maibaum}, Pages = {143--168}, Publisher = SPRINGER, Title = {Program Specification and Data Refinement in Type Theory}, Year = {1991} } @Article{Marriott93, Author = {K. Marriott}, Title = {Frameworks for abstract interpretation}, Journal = {Acta Informatica}, Volume = {30}, Pages = {103--129}, Year = {1993} } @Inproceedings{McCarthy/Painter67, Author = {McCarthy, J. and Painter, {J.A.}}, Title = {Correctness of a Compiler for Arithmetical Expressions}, Editor = {J.T. Schwartz}, BookTitle = {Proceedings of a Symposium in Applied Mathematics, 19, Mathematical Aspects of Computer Science}, Organization = {American Mathematical Society}, Year = {1967} } @Inproceedings{McCarthy60, Author = {McCarthy, J.}, Title = {{R}ecursive {F}unctions of {S}ymbolic {E}xpressions and their {C}omputation by {M}achine, {P}art {I}}, BookTitle = {Communications of the ACM}, Series = {Vol. 3}, Number = {4}, Year = 1960 } @Book{McCarthy62, Author = {McCarthy, J. and Abrahams, {P.W.} and Edwards, {D.J.} and Hart, {T.P.} and Levin, {M.I.}}, Title = {LISP 1.5 {P}rogrammer's {M}anual}, Publisher = {The MIT Press}, Address = {Cambridge, MA}, Year = 1962 } @PhDThesis{Meijer92, Author = {E. Meijer}, Title = {Calculating Compilers}, School = {University of Nijmwegen}, Year = {1992} } @Book{Mertens+93, Author = {Mertens, P. and Barowski,V. and Geis, W.}, Title = {{B}etriebliche {E}xpertensystem-{A}nwendungen}, Publisher = {2. Auflage, Springer-Verlag}, Address = {Berlin, Heidelberg, New York}, Year = 1990 } @MastersThesis{Michelsen98, Author = {Michelsen, Dagobert}, Title = {{Korrektheit der Daten- und Operationsverfeinerung f\"ur eine applikative Sprache mit automatischer Speicherbereinigung}}, School = CAUIfIuPM, Address = {{K}iel}, Year = 1998 } @Book{Milner+90, Author = {Robin Milner and Mads Tofte and Robert Harper}, Title = {{T}he {D}efinition of {S}tandard {ML}}, Publisher = {MIT Press}, Year = {1990} } @MastersThesis{Mohnberg90, Author = {Mohnberg, A.}, Title = {{G}arbage {C}ollection {f}\"ur {COLIBRI}, {A}nforderungen, {K}onzepte {u}nd {I}mplementierung}, School = CAUIfIuPM, Address = {{K}iel}, Year = 1990 } @InProceedings{Moore/Kaufmann96, Author = {{J S.} Moore and M. Kaufmann}, Title = {{ACL2}: {A}n Industrial Strength Version of {Nqthm}}, Booktitle = {Proceedings of COMPASS '96}, Year = 1996, Month = jun } @TechReport{Moore88, Author = {{J S.} Moore}, Address = {Austin, Texas}, Institution = {Comp. Logic Inc}, Number = {22}, Title = {Piton: A Verified Assembly Level Language}, Year = {1988} } @Article{Moore89, Author = {{J S.} Moore}, Title = {A mechanically verified language implementation}, Journal = {Journal of Automated Reasoning}, Year = {1989}, Volume = {5}, Number = {4}, } @TechReport{Moore92, Author = {{J S.} Moore}, Address = {Austin, Texas}, Institution = {Lecture Res. Prog. Pres., Comp. Logic Inc.}, Title = {{T}he {A}cl2-{P}roject}, Year = {1992} } @Book{Moore96, Author = {J S. Moore}, Title = {Piton, A Mechanically Verified Assembly-Level Language}, Publisher = {Kluwer Academic Publishers}, Year = 1996 } @Inproceedings{Morris74, Author = {{F. L.} Morris}, Title = {Advice on structuring compilers and proving them correct}, BookTitle = {1st Proceedings of Principles of Programming Languages}, Pages = {144--152}, Year = {1974} } @TechReport{Mosses79, Author = {P. D. Mosses}, Title = {SIS - semantics implementation system, reference manual and user guide}, Number = {Departmental Report DAIMI MD-30}, Institution = {Computer Science Department, Aarhus University}, Year = {1979} } @Inproceedings{Mosses82, Author = {P. D. Mosses}, Title = {Abstract semantic algebras}, BookTitle = {Formal description of programming concepts II}, Organization = {IFIP IC-2 Working Conference}, Editor = {D. Bj\o rner}, Publisher = {North Holland}, Pages = {63--88}, Year = {1982} } @Book{Mosses92, Author = {P. D. Mosses}, Title = {Action Semantics}, Publisher = {Cambridge University Press}, Year = {1992} } @MastersThesis{Mueller-Olm90, author = {Markus M\"uller-Olm}, title = {{Korrektheit einer \"Ubersetzung der Sprache rekursiver Funktionsdefinitionen erster Ordnung in eine einfache imperative Sprache}}, school = {CAU Kiel}, year = 1990 } @InCollection{Mueller-Olm93, Author = {Markus M\"uller-Olm}, Title = {{P}roven {C}orrect {C}ompiling {S}pecification {SubLisp} to {PL}}, BookTitle = {{P}rovably {C}orrect {S}ystems}, Publisher = {ProCos I Partners}, Year = 1993, Chapter = 30, Editor = {Dines Bj\o rner and Hans Langmaack and C.~A.~R.~Hoare}, Pages = {405--451} } @TechReport{Mueller-Olm95, Author = {Markus M\"uller-Olm}, Title = {{A}n {E}xercise in {C}ompiler {V}erification}, Type = {Internal Report}, Institution = {CS Department, University of Kiel}, Year = 1995 } @Book{Mueller-Olm96, Author = {Markus M\"uller-Olm}, Title = {{Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction}}, Publisher = Springer, Series = LNCS, Volume = {1283}, Year = {1997}, Address = {Berlin, Heidelberg, New York} } @TechReport{Mueller-Olm96b, Author = {Markus M\"uller-Olm}, Title = {{Three Views on Preservation of Partial Correctness}}, Type = {Technical Report}, Institution = {CAU Kiel}, Number = {Verifix/CAU/5.1}, Year = {1996}, Month = oct, } @Book{Nagl90, Author = {M. Nagl}, Title = {{Softwaretechnik: Methodisches Programmieren im Gro\ss en}}, Publisher = {Springer-Verlag}, Address = {Berlin, Heidelberg}, Year = {1990} } @Book{Nagl91, Author = {M. Nagl}, Title = {{ADA, Eine Einf\"uhrung in die Programmiersprache der Softwaretechnik}}, Publisher = {Vieweg-Verlag}, Year = 1991, Edition = {3.\ verb.\ } } @InProceedings{Necula97, title = "Proof-Carrying Code", author = "George C. Necula", pages = "106--119", booktitle = "Conference Record of {POPL}~'97: The 24th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages", month = "15--17 " # jan, year = "1997", address = "Paris, France", references = "\cite{JACM::BoyerY1996} \cite{JACM::HarperHP1993} \cite{APAL::MillerNPS1991} \cite{LICS::Pfenning1989}", } @InProceedings{Necula/Lee98, title = "The Design and Implementation of a Certifying Compiler", author = "George C. Necula and Peter Lee", booktitle = "Proceedings of the {ACM} {SIGPLAN}'98 Conference on Programming Language Design and Implementation ({PLDI})", address = "Montreal, Canada", month = "17--19~" # jun, year = "1998", pages = "333--344", references = "\cite{JACM::HarperHP1993} \cite{JAR::Moore1989} \cite{POPL::Morris1973} \cite{POPL::MorrisettWC1998} \cite{POPL::Necula1997} \cite{TOPLAS::NelsonO1979} \cite{JACM::Shostak1981} \cite{PLDI::TarditiMCSHL1996} \cite{JAR::Young1989}", } @Article{Nelson/Oppen80, Author = {G. Nelson and D. Oppen}, Journal = {JACM}, Number = {2}, Pages = {356-364}, Title = {Fast decision procedures based on congruence closure}, Volume = {27}, Year = {1980} } @Article{Nielson82, Author = {Nielson, {F. A.}}, Title = {A denotational framework for data flow analysis}, Journal = {Acta Informatica}, Volume = {18}, Pages = {265--287}, Year = {1982} } @manual{Nuprl93, Author = {The Nuprl Group}, Edition = {4.1}, Month = mar, Note = {(Draft)}, Organization = {Cornell University}, Title = {The {Nuprl} Proof Development System}, Year = {1993} } @Book{ODonnell85, Author = {{M.J.} {O'D}onnell}, Title = {Equational Logic as a Programming Language}, Publisher = {MIT Press}, Year = {1985} } @TechReport{Oliva/Wand92, Author = {{Dino P.} Oliva and Mitchell Wand}, Title = {{A} {V}erified {C}ompiler for {P}ure {PreScheme}}, Institution = {Northeastern University College of Computer Science}, Type = {Technical Report}, Number = {NU-CCS-92-5}, Address = {Northeastern University}, Month = feb, Year = 1992 } @Article{Oppacher/Suen88, Author = {F. Oppacher and E. Suen}, Journal = {Journal of Automated Reasoning}, Volume = {4}, Pages = {69-100}, Title = {{HARP}: A Tableau-Based Theorem Prover}, Year = {1988} } @Inproceedings{Owre+92, Author = {S. Owre and {J. M.} Rushby and N. Shankar}, BookTitle = {Proceedings 11th International Conference on Automated Deduction CADE}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Artificial Intelligence}, Volume = {607}, Month = oct, Pages = {748-752}, Title = {{PVS}: {A} {P}rototype {V}erification {S}ystem}, Address = {Saratoga, NY}, Editor = {Deepak Kapur}, Year = {1992} } @Inproceedings{Owre+93, Author = {S. Owre and J. Rushby and N. Shankar and {F.W. von} Henke}, BookTitle = {Proceedings FME'93: Industrial-Strength Formal Methods}, Key = {Owre 93}, Month = apr, Pages = {482--500}, Publisher = {Springer-Verlag LNCS 670}, Title = {Formal verification of fault-tolerant architectures: some lessons learned}, Year = {1993} } @Inproceedings{Palsberg92, Author = {J. Palsberg}, Title = {An automatically generated and provably correct compiler for a subset of ADA}, BookTitle = {IEEE International Conference on Computer Languages}, Year = {1992} } @InProceedings{Parnas94, Author = {Parnas, {David Lorge}}, title = {{I}nspection of {S}afety {C}ritical {S}oftware {U}sing {P}rogram-{F}unction {T}ables}, Editor = {Duncan, K. and Krueger, K.}, Booktitle = {Proceedings of the 13th World Computer Congress 1994, Volume 3}, Year = {1994}, Publisher = {Elsevier Science B.V. (North-Holland)} } @Book{Partsch90, Author = {H. Partsch}, Publisher = SPRINGER, Series = {Texts and Monographs in Computer Science}, Title = {Specification and Transformation of Programs}, Year = {1990} } @PHDTHESIS{Paulson81, Author = {L. Paulson}, Title = {A compiler generator for semantic grammars}, School = {Stanford University}, Year = {1981} } @Inproceedings{Persch+83, Author = {Guido Persch and H.-S. Jansohn and W. Kirchg\"assner and Rudolf Landwehr and Manfred Dausmann and Sophia Drossopoulou and Gerhard Goos}, Title = {Ada Compiler Karlsruhe Overview}, Year = {1983}, BookTitle = {Ada-Europe / Adatex Joint Conference on Ada}, Publisher = {Commission of the European Communities}, Pages = {2/1 -- 4}, Address = {Br\"ussel} } @PhDThesis{Pettersson95, Author = {Pettersson, M.}, Title = {{Compiling Natural Semantics}}, School = {Link{\o}ping University}, Address = {Link{\o}ping, Sweden}, Year = 1995 } @TechReport{Pfeifer94, Author = {H. Pfeifer}, Institution = {Universit{\"a}t Ulm}, Number = {94--02}, Title = {Reflexion von {\sc QED} in {\sc QED}}, Type = {Korso Study Note}, Year = {1994} } @TechReport{Pfeifer96a, Author = {Pfeifer, Holger}, Title = {{Supporting Refinement Calculus Proofs in PVS}}, Institution = {Universit\"at Ulm}, Type = {Technical Report}, Number = {Verifix/Ulm/3.1}, Year = {1996}, Month = apr } @TechReport{Pfeifer+96, Author = {Pfeifer, Holger and Dold, Axel and {von Henke}, {F.W.} and Rue{\ss}, Harald}, Title = {{Mechanized Semantics of Simple Imperative Programming Constructs}}, Institution = {Universit\"at Ulm}, Type = {Ulmer Informatik-Berichte}, Number = {96-11}, Year = {1996}, Month = dec } @TechReport{Pfeifer+96a, Author = {Pfeifer, Holger and Dold, Axel and {von Henke}, {F.W.} and Rue{\ss}, Harald}, Title = {{Mechanized Semantics of Simple Imperative Programming Constructs}}, Institution = {Universit\"at Ulm}, Type = {Technical Report}, Number = {Verifix/Ulm/15.1}, Year = {1996}, Month = aug } @Misc{Pofahl95, Author = {E. Pofahl}, Title = {{Methods Used for Inspecting Safety Relevant Software}}, Howpublished = {{In W. J. Cullyer, W. A. Halang, B.J. Kr\"amer (eds.): High Integrity Programmable Electronic Systems, Dagstuhl-Sem.-Rep. 107, p 13}}, Year = {1995} } @InCollection{Polak81, Author = {W. Polak}, Editor = {G. Goos, J. Hartmanis}, Number = {124}, Publisher = SPRINGER, Series = {LNCS}, Title = {Compiler Specification and Verification}, BookTitle = {Lecture Notes in Computer Science}, Year = {1981} } @Article{Pym/Wallen90a, Author = {David Pym and Lincoln Wallen}, Journal = {10th CADE}, Pages = {236-250}, Title = {Investigations into proof-search in a system of first-order dependent function types}, Volume = {LNCS 449}, Year = {1990} } @Book{Randell+95, Title = {Proceedings of Predictably Dependable Computing Systems PDCS'95}, Author = {B. Randell and {J.-C.} Laprie and H. Kopetz and B. Littlewood (Eds.)}, Publisher = {Esprit Basic Research Series, Springer-Verlag}, Year = 1995 } @Inproceedings{Reddy88, Author = {Reddy, {U.S.}}, Title = {Objects as {C}losures: {A}bstract {S}emantics of {O}bject {O}riented {L}anguages}, BookTitle = {Proceedings of the 1988 ACM Conference on LISP and Functional Programming}, Pages = {289--297}, Year = 1988 } @Misc{Robinson96, author = {A. Robinson}, title = {Formal and Informal Proof}, howpublished = {{Vortrag im Kolloquium des DFG-Schwerpunktprogramms ``Deduktion'', Dagstuhl}}, year = {1996}, month = jan } @MastersThesis{Ruehle98, Author = {R{\"u}hle, J\"urgen}, Title = {{Verifikation der Codegenerierung im Verifix-Projekt: Pr\"adikattransformer und Erhaltung partieller Korrektheit}}, School = CAUIfIuPM, Address = {{K}iel}, Year = 1998 } @TechReport{Rubinfeld90, Author = {R. Rubinfeld}, Title = {A Mathematical Theory of Self-Checking, Self-Testing and Self-Correcting Programs}, Institution = {International Computer Science Institute}, Number = {TR--90--054}, Year = {1990} } @TechReport{Ruess93, Author = {H. Rue{\ss}}, Institution = {Universit{\"a}t Ulm}, Number = {93--01}, Title = {Report on the {S}pecification {L}anguage {\sc QED}}, Type = {Korso Working Paper}, Year = {1993} } @TechReport{Rushby+91, Author = {John Rushby and {Friedrich von Henke} and Sam Owre}, Address = {Menlo Park, CA}, Institution = {Computer Science Laboratory, SRI International}, Month = feb, Number = {SRI--CSL--91--2}, Title = {An Introduction to Formal Specification and Verification Using {{\sc Ehdm}}}, Year = {1991} } @Article{Rushby/vHenke93, Key = {Rushby 93}, Author = {J. M. Rushby and {F.W. von} Henke}, Title = {Formal verification of algorithms for critical systems}, Journal = {IEEE Trans. on Software Engineering}, Year = {1993}, Volume = {19}, Number = {1}, Month = jan, Pages = {13--23} } @Unpublished{Rushby94, Author = {J. Rushby}, Month = jan, Note = {Incomplete Draft}, Title = {Proof Movie II: A Proof with PVS}, Year = {1994} } @TechReport{Sampaio91, Author = {Augusto Sampaio}, Title = {A Comparative Study of Theorem Provers: Proving Correctness of Compiling Specifications}, Institution = {Oxford University Computing Laboratory, Programming Research Group}, Year = {1991}, Key = {PRG-TN-20-90} } @PhDThesis{Sampaio93, Author = {Augusto Sampaio}, Title = {An Algebraic Approach to Compiler Design}, School = {Oxford University Computing Laboratory}, Year = {1993}, Month = oct, Note = {Technical Monograph PRG--110, Oxford University Computing Laboratory}, Address = {Programming Research Group} } @Article{Schmidt85, Author = {D. A. Schmidt}, Title = {Detecting global variables in denotational specifications}, Journal = {ACM Transactions on Programming Languages and Systems}, Volume = {7}, Number = {2}, Pages = {299--310}, Year = {1985} } @Article{Schmidt88, Author = {D. A. Schmidt}, Title = {Detecting stack-based environments in denotational definitions}, Journal = {Science of Computer Programming}, Volume = {11}, Pages = {107--131}, Year = {1988} } @TechReport{Schroeer88, Author = {{F. W.} Schr\"oer}, Title = {Districts: A Foundation for the Suppression of Partial Redundancies}, Institution = {GMD-Berichte}, Number = {304}, Year = {1988} } @Article{Schroeer88b, Author = {{F. W.} Schr\"oer}, Title = {Das GMD Modula-2 Entwicklungssystem}, Journal = {GMD-Spiegel}, Volume = {1}, Year = {1988} } @PhDThesis{Schuerr91, Author = {Sch\"urr, Andreas}, Title = {Operationales Spezifizieren mit programmierten Graphersetzungssystemen}, SCHOOL = {{Universit\"at Aachen, Deutscher Universit\"ats-Verlag}}, Year = {1991} } @Inproceedings{Schwarz+88, Author = {Schwarz, B. and Kirchg\"assner, W. and Landwehr, R.}, Title = {An Optimizer for Ada - Design, Experiences and Results}, Booktitle = {Proceedings of the ACM SIGPLAN '89 Conference on Programming Language Design and Implementation}, Year = 1989, Month = jun } @TechReport{Schwier93a, Author = {D. Schwier}, Institution = {Universit{\"a}t Ulm}, Number = {93--04}, Title = {Semantik von {\sc QED}}, Type = {Korso Working Paper}, Year = {1993} } @TechReport{Schwier93b, Author = {D. Schwier}, Institution = {Universit{\"a}t Ulm}, Number = {93--05}, Title = {Formale {P}rogrammentwicklung in {\sc QED}}, Type = {Korso Study Note}, Year = {1993} } @Inproceedings{Shankar91, Author = {N. Shankar}, BookTitle = {CADE-11}, Publisher = {Springer LNCS 607}, Title = {Proof Search in the Intuitionistic Sequent Calculus}, Year = {1991} } @Article{Shostak79a, Author = {Robert E. Shostak}, Journal = {JACM}, Month = apr, Number = {2}, Pages = {361-360}, Title = {A Practical Decision Procedure for Arithmetic with Function Symbols}, Volume = {26}, Year = {1979}, Category = {DecisionProcedures} } @TechReport{Simpson90, Author = {T. Simpson}, Address = {Department of Computer Science, University of Calgary, 2500 University Drive N.W., Calgary, Alberta, Canada, T2N 1N4}, Institution = {Department of Computer Science, University of Calgary,}, Month = oct, Number = {90/410/34}, Title = {Correctness of a Compiler Specification for the SECD Machine}, Type = {Research Report}, Year = {1990} } @Book{Sites92, Author = {Richard L. Sites}, Title = {{Alpha} {A}rchitecture {R}eference {M}anual}, Publisher = {Digital Equipment Corporation}, Year = 1992 } @TechReport{Smith82, Author = {Smith, {B.C.}}, Title = {{R}eflection and {S}emantics in a {P}rocedural {L}anguage}, Institution = {Massachusetts Institute of Technology}, Type = {{T}echnischer {B}ericht}, Number = {MIT-LCS-TR-272}, Address = {Cambridge, MA}, Year = 1982 } @Inproceedings{Smith84, Author = {Smith, {B.C.}}, Title = {{R}eflection and {S}emantics in {L}isp}, BookTitle = {Proceedings of the 11th ACM Symposium on Principles of Programming Languages POPL'84}, Pages = {23-35}, Year = 1984 } @TechReport{Smith87, Author = {D.R. Smith}, Address = {Palo Alto, CA}, Institution = {Kestrel Institute}, Number = {KES.U.87.12}, Title = {Structure and Desing of Global Search Algorithms}, Year = {1987} } @Book{Steele84, Author = {Steele, {G.L.}}, Title = {{Common Lisp}: {T}he {L}anguage}, Publisher = {Digital Press}, Address = {Bedford, MA}, Year = 1984 } @Book{Steele90, Author = {Steele, {G.L.}}, Title = {{Common Lisp}: {T}he {L}anguage. Second Edition}, Publisher = {Digital Press}, Address = {Bedford, MA}, Year = 1990 } @Inproceedings{Steffen+89, Author = {Steffen, B. and Knoop, J. and R\"uthing, O.}, Title = {{T}he {V}alue {F}low {G}raph: {A} {P}rogram {R}epresentation {f}or {O}ptimal {P}rogram {T}ransformations}, BookTitle = {\mbox{$3^{rd}$} ESOP}, Publisher = {LNCS 432}, Pages = {389--405}, Address = {Copenhagen, Denmark}, Note = {--\ Extended version available as: Bericht Nr. 9004, Institut f\"ur Informatik und Praktische Mathematik, Christian-Albrechts-Universit\"at Kiel, Germany, 1990}, Year = 1990 } @Inproceedings{Steffen+90, Author = {Steffen, B. and Knoop, J. and R\"uthing, O.}, Address = {Copenhagen, Denmark}, BookTitle = {Proc. 3$^{rd}$~} # ESOP, Pages = {389 - 405}, Publisher = SPRINGER, Series = LNCS # {~ 432}, Title = {The Value Flow Graph: {A} Program Representation for Optimal Program Transformations}, Year = {1990} } @Inproceedings{Steffen+91, Author = {Steffen, B. and Knoop, J. and R\"uthing, O.}, Address = {Brighton, UK}, BookTitle = {Proc. 4$^{th}$~} # TAPSOFT, Pages = {394 - 415}, Publisher = SPRINGER, Series = LNCS # {~494}, Title = {Efficient Code Motion and an Adaption to Strength Reduction}, Year = {1991} } @Inproceedings{Steffen/Knoop89, Author = {Steffen, B. and Knoop, J.}, Address = {Por\c{a}bka-Kozubnik, Poland}, BookTitle = {Proc. 14$^{th}$ MFCS}, Pages = {481-491}, Publisher = SPRINGER, Series = LNCS # {379}, Title = {Finite Constants: {C}haracterizations of a New Decidable Set of Constants}, Year = {1989} } @Article{Steffen/Knoop91, Author = {Steffen, B. and Knoop, J.}, Journal = tcs, Note = {Extended version of \cite{Steffen/Knoop89}}, Number = {2}, Pages = {481-491}, Publisher = SPRINGER, Title = {Finite Constants: {C}haracterizations of a New Decidable Set of Constants}, Volume = {80}, Year = {1991} } @Inproceedings{Steffen87a, Author = {Steffen, B.}, Title = {{O}ptimal {R}un {T}ime {O}ptimization. {P}roved {b}y {a} {N}ew {L}ook {a}t {A}bstract {I}nterpretations}, BookTitle = {\mbox{$2^{nd}$} TAPSOFT}, Publisher = {LNCS 249}, Pages = {52--68}, Address = {Pisa, Italy}, Year = 1987 } @PhDThesis{Steffen87b, Author = {Steffen, B.}, Title = {{A}bstrakte {I}nterpretationen {b}eim {O}ptimieren {v}on {P}rogrammlaufzeiten. {E}in {O}ptimalit\"atskonzept {u}nd {s}eine {A}nwendung}, School = {Bericht Nr. 8713, Institut f\"ur Informatik und Praktische Mathematik der Christian-Albrechts-Universit\"at}, Address = {Kiel}, Year = 1987 } @Inproceedings{Steffen89, Author = {Steffen, B.}, Title = {{O}ptimal {D}ata {F}low {A}nalysis {v}ia {O}bservational {E}quivalence}, BookTitle = {\mbox{$14^{th}$} MFCS}, Publisher = {LNCS 397}, Pages = {492--502}, Address = {Por\c{a}bka-Kozubnik, Poland}, Year = 1989 } @Book{Stoy77, Author = {Stoy, {J.E.}}, Title = {{D}enotational {S}emantics: {T}he {S}cott--{S}trachey {A}pproach to {P}rogramming {L}anguage {T}heory}, Publisher = {MIT Press}, Address = {Cambridge, MA., London}, Year = 1977 } @TechReport{Symbolics85, Author = {{Symbolics Inc.}}, Title = {Reference guide to {Symbolics} {LISP}}, Institution = {Symbolics Inc.}, Address = {Cambridge, MA}, Year = 1985 } @TechReport{Symbolics86, Author = {{Symbolics Inc.}}, Title = {Symbolics {Common Lisp}: {L}anguage {C}oncepts}, Institution = {Symbolics Inc.}, Address = {Cambridge, MA}, Year = 1986 } @TechReport{Taiichi/Masami86, Author = {Taiichi, Y. and Masami, H.}, Title = {{K}yoto {C}ommon {L}isp {R}eport}, Institution = {Research Institute for Mathematical Science}, Address = {Kyoto University}, Year = 1986 } @TechReport{Tarditi+90, Author = {Tarditi, D. and Acharya, A. and Lee, P.}, Title = {{N}o {A}ssembly required: {C}ompiling {S}tandard {ML} to {C}.}, Institution = {School of Computer Science, CMU}, Year = {1990}, Number = {CMU-CS-90-187}, Month = dec } @Article{Thatcher+81, Author = {Thatcher, J. W. and Wagner, E. G. and Wright, J.B.}, Title = {More on Advice on Structuring Compilers and Proving them Correct}, Journal = {Theoretical Computer Science}, Volume = {15}, Year = {1981}, Pages = {223--249} } @Article{Thompson84, Author = {Ken Thompson}, Title = {{Reflections on Trusting Trust}}, Journal = {Communications of the ACM}, Volume = {27}, Number = {8}, Year = {1984}, Pages = {761--763}, Note = {Also in ACM Turing Award Lectures: The First Twenty Years 1965-1985, ACM Press, 1987, and in Computers Under Attack: Intruders, Worms, and Viruses Copyright, ACM Press 1990} } @Book{Uhl86, Author = {J. Uhl}, Title = {Spezifikation von Programmiersprachen und \"Ubersetzern}, Series = {GMD-Berichte}, Volume = {161}, Publisher = {Oldenburg-Verlag}, Year = {1986} } @Inproceedings{Vollmer/Hoffart92, Author = {J. Vollmer and R. Hoffart}, Title = {Modula-P, a Language For Parallel Programming; Definition and Implementation on a Transputer Network}, BookTitle = {IEEE International Conference on Computer Languages}, Year = {1992} } @book{Waite/Goos84, Author = {William M. Waite and Gerhard Goos}, Title = {{C}ompiler {C}onstruction}, Year = {1984}, Publisher = {Springer Verlag} } @Inproceedings{Wallace95, Author = {C. Wallace}, Title = {{T}he {S}emantics of the {C++}--{P}rogramming {L}anguage}, Editor = {E. B\"orger}, BookTitle = {Specification and Validation Methods}, Publisher = {Oxford University Press}, Year = {1995}, } @Book{Wallen90, Author = {{Lincoln A.} Wallen}, Publisher = {MIT Press}, Title = {Automated proof search in non-classical logics}, Year = {1990} } @Inproceedings{Wand/Friedman86, Author = {Wand, M. and Friedman, {D.P.}}, Title = {{T}he {M}ystery of the {T}ower {R}evealed: {A} {N}on-{R}eflective {D}escription of the {R}eflective {T}ower}, BookTitle = {Proceedings of the 1986 ACM-Conference on Lisp and Functional Programming}, Pages = {298-307}, Address = {Cambridge, MA}, Year = 1986 } @Article{Wand84, Author = {Wand, M.}, Title = {A semantic prototyping system}, Journal = {SIGPLAN Notices}, Note = {SIGPLAN 84 Symp. On Compiler Construction}, Volume = {19}, Number = {6}, Pages = {213--221}, Month = jun, Year = {1984} } @Inproceedings{Wand87, Author = {Wand, M.}, Title = {Complete {T}ype {I}nference for {S}imple {O}bjects}, BookTitle = {Proceedings of the {IEEE} Symposium on Logic in Computer Science}, Pages = {37--44}, Address = {Ithaca, N.Y.}, Year = 1985 } @Article{Wasserman/Blum97, Author = "Hal Wasserman and Manuel Blum", Title = "Software reliability via run-time result-checking", Journal = "Journal of the ACM", Volume = "44", Number = "6", Pages = "826--849", Month = nov, Year = "1997", Coden = "JACOAH", ISSN = "0004-5411", Bibdate = "Fri Feb 13 15:58:32 MST 1998", Acknowledgement = ack-nhfb, } @Article{Weber-Wulff93, Author = {Weber-Wulff, Deborah}, Journal = {Formal Aspects of Computing}, Number = {2}, Pages = {121--151}, Title = {Proof Movie -- a proof with the Boyer-Moore prover}, Volume = {5}, Year = {1993} } @Book{Weber91, Author = {M. Weber}, Title = {A Meta Calculus for Formal System Development}, Series = {GMD--Berichte}, Publisher = {Oldenbourg-Verlag}, Volume = {195}, Year = {1991} } @Inproceedings{Weule93, Author = {Weule, H.}, Editor = {Puppe, F. and G\"unter, A.}, Title = {{E}xpertensysteme im industriellen {E}insatz}, BookTitle = {Expertensysteme '93}, Publisher = {Informatik aktuell, Springer-Verlag}, Address = {Berlin, Heidelberg, New York}, Year = 1993 } @TechReport{Wolf99a, Author = {Andreas Wolf}, Institution = {CAU Kiel}, Month = feb, Number = {Verifix/CAU/6.1}, Title = {{An Exercise in Compiler Verification Revisited -- Preserving Partial Correctness }}, Type = {Technical Report}, Year = {1999} } @TechReport{Wolf99b, Author = {Andreas Wolf}, Institution = {CAU Kiel}, Month = feb, Number = {Verifix/CAU/6.2}, Title = {{The Adequacy of a Loop's Definition}}, Type = {Technical Report}, Year = {1999} } @Inproceedings{Woodcock/Morgan90, Author = {Woodcock, {J.C.P.} and Morgan, Carroll}, Editor = {D. Bj\o rner and {C.A.R.} Hoare and H. Langmaack}, Title = {{R}efinement of {S}tate {B}ased {C}oncurrent {S}ystems}, BookTitle = {Proc. of the 3. International Symposium of VDM Europe VDM'90}, Series = LNCS, Number = 428, Publisher = SPRINGER, Address = {Kiel}, Year = {1990} } @InProceedings{Yellin95, author = "Frank Yellin", title = "Low Level Security in Java", keywords = "java, safe language, security, byte code verifier", url = "http://www.w3.org/pub/Conferences/WWW4/Papers/197/40.html", booktitle = "Fourth International Conference on the World-Wide Web", address = "MIT, Boston", year = "1995", month = dec, } @TechReport{Young88, Author = {W.D. Young}, Address = {Austin, Texas}, Institution = {Comp. Logic. Inc.}, Number = {33}, Title = {A Verified Code Generator for a Subset of Gypsy}, Year = {1988} } @Book{Zimmermann90, Author = {W. Zimmermann}, Title = {Automatische Komplexit{\"a}tsanalyse funktionaler Programme}, Series = {Informatik-Fachberichte}, Volume = {261}, Publisher = SPRINGER, Year = {1990} } @Unpublished{Zimmermann/Gaul96, Author = {W. Zimmermann and T. Gaul}, Title = {{On the Construction of Correct Compiler Back-Ends: An ASM Approach}}, Note = {{A}ccepted at {J}ournal of {U}niversal {C}omputer {S}cience}, Year = 1996 } @Misc{ZSI89, Author = {{ZSI-Zentralstelle f\"ur Sicherheit in der In\-for\-ma\-tions\-technik}}, Title = {{IT-Sicherheitskriterien}}, Howpublished = {Bundesanzeiger Verlagsgesellschaft, K\"oln}, Year = {1989} } @Misc{ZSI90, Author = {{ZSI-Zentralstelle f\"ur Sicherheit in der In\-for\-ma\-tions\-technik}}, Title = {{IT-Evaluationshandbuch}}, Howpublished = {{Bundesanzeiger Verlagsgesellschaft, K\"oln}}, Year = {1990} } @Inproceedings{diPrimio+85, Author = {diPrimio, F. and Bungers, D. and Christaller, Th.}, Title = {{BABYLON} als {W}erkzeug zum {A}ufbau von {E}xpertensystemen}, BookTitle = {Informatik--Fachberichte Nr. 112 ``Wissensbasierte Systeme''}, Editor = {Brauer, W. and Radig, B.}, Publisher = SPRINGER, Pages = {234--245}, Address = {Berlin}, Year = 1985 } @Inproceedings{vHenke+94, Author = {{F.W. von} Henke and A. Dold and M. Grosse and H. Rue{\ss} and D. Schwier and M. Strecker}, BookTitle = {Arbeitsberichte des {\sc Korso}-Projekts}, Note = {Erscheint im Laufe des Jahres}, Publisher = {Springer LNCS}, Title = {Construction and {D}eduction {M}ethods for the {F}ormal {D}evelopment of {S}oftware}, Year = {1994} } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Verifix -- Karlsruhe -- Berichte %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @TechReport{Verifix95:ISinformell, author = {A. Dold and T. Gaul and W. Goerigk and G. Goos and A. Heberle and F. von Henke and U. Hoffmann and H. Langmaack and H. Pfeifer and H. Ruess and W. Zimmermann}, title = "{D}efinition of the {L}anguage {IS}", institution = "University of Karlsruhe/Kiel/Ulm", type = {Verifix Working Paper}, number = "[Verifix/UKA/1]", Year = 1995, } @TechReport{Verifix95:SemIS, author = {A. Heberle and M. M\"uller and W. Zimmermann}, title = "An {E}volving {A}lgebra {S}pecification of the {O}perational {S}emantics of {IS}", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/2]", Year = 1995, } @TechReport{Verifix96:MIS1, author = {T.S. Gaul and A. Heberle and W. Zimmermann}, title = "An {E}volving {A}lgebra {S}pecification of the {O}perational {S}emantics of {MIS}", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/3]", Year = 1995, } @TechReport{Verifix95:Alpha, author = {T.S. Gaul and W. Zimmermann}, title = "An {E}volving {A}lgebra for the {A}lpha {P}rocessor {F}amily", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/4]", Year = 1995, } @TechReport{Verifix96:MIS1toAlphaSimple, author = {T.S. Gaul}, title = "Code generation for the {DEC}-{A}lpha {P}rocessor {F}amily", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/5]", Year = 1996, } @TechReport{Verifix96:MIStoAlpha, author = {T.S. Gaul}, title = "{S}pecification and {V}erification of code generation rules for MIS to DEC-Alpha compilation", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/6]", Year = 1996, } @TechReport{Verifix96:SemAnalyse0, author = {A. Heberle and W. Zimmermann and G. Goos}, title = "{S}pecification and {V}erification of {C}ompiler {F}rontend {T}asks: {S}emantic {A}nalysis", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/7]", Year = 1996, } @TechReport{Verifix96:IS0toMIS, author = {A. Heberle and W. Zimmermann}, title = "{S}pezifikation der {\"U}bersetzung von {$IS_0$} nach {$MIS$}", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/8]", Year = 1996, } @TechReport{Verifix96:IS0toMISproofDA, author = {A. Heberle and W. Zimmermann}, title = "{S}pezifikation und {V}erifikation der {D}atenabbildung von $\mbox{\it IS}_0$ nach $\mbox{\it MIS}$", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/9]", Year = 1996, } @Techreport{ZDG:96, author = {W. Zimmermann and A. Dold and T. Gaul}, title = "{On the Construction of Correct Compiler Back--Ends}", institution = "University of Karlsruhe, University of Ulm", type = {Verifix Working Paper}, number = "[Verifix/UKA/10]", Year = 1996, } @TechReport{Verifix96:Bench, author = {T.S. Gaul}, title = "Bechmarking code-generation for IS to DEC-Alpha", institution = "University of Karlsruhe", type = {Verifix Working Paper}, number = "[Verifix/UKA/11]", Year = 1996, } %----------------------------------------------------------------------