Lesegruppe


Dr. Sabine Glesner, Jan Olaf Blech und Lars Gesellensetter


Termine:

jeweils Dienstags, 10:00 im AVG 2. OG Raum 211 (Küche)

Diese Veranstaltung soll ein Forum darstellen, um aktuelle Forschungsfragen zu diskutieren. Behandelt werden u.a. Themen aus Compileroptimierung und -verifikation sowie Software Engineering (insbesondere Komponentensysteme). Jedes Treffen findet unter einem Themenschwerpunkt statt, zu dem auch Literatur bekanntgegeben wird.
Die Lesegruppe ist weniger als geschlossene Veranstaltung anzusehen, sondern als eine Menge einzelner Termine mit verschiedenen Inhalten. Wer also Lust hat, bei einem Kaffee in netter Runde aktuelle Themen aus Compileroptimierung und -verifikation zu diskutieren, ist herzlichst eingeladen. Angeregte Diskussionen können auch im Anschluß in der Mensa weitergeführt werden (wo wir für Nachzügler auch gegen 12 Uhr anzutreffen sind).
Übrigens freuen wir uns auch über Themenvorschläge - wenn ihr also einen interessanten Artikel findet, den ihr gerne näher diskutieren oder vorstellen möchtet, sagt Bescheid!


Termin Thema Literatur
08.02.2005 Semantik von Statecharts
Hierarchische Automaten
  • David Harel, "On visual formalisms", Commun.ACM, 1988.
  • Pnueli Shalev, "What is in a Step: On the Semantics of Statescharts", Lecture Notes In Computer Science; Vol. 526, 1991.
  • Gerald Luettgen, Michael von der Beeck, and Rance Cleaveland, "A Compositional Approach tp Statechart Semantics", Foundations of Software Engineering, 2000.
  • Giorgio Busatto, "An Abstract Model of Hierarchical Graphs and Hierarchical Graph Transformations", Dissertation, 2002.
15.02.2005 Model Checking
Petri-Netze
  • Edmund M. Clarke Jr., Orna Grumberg, and Doron A. Peled, "Model Checking", MIT Press, 1999.
22.02.2005 SSA-Repräsentation
  • Fred C. Chow, Sun Chan, Shin-Ming Liu, Raymond Lo, and Mark Streich, "Effective Representation of Aliases and Indirect Memory Operations in SSA Form", Springer Verlag, 1996.
  • Glen E. Weaver, Kathryn S. McKinley, Charles C. Weems, "Score: A Compiler Representation For Heterogeneous Systems", Heterogeneous Computing Workshop, 1996.
  • Kathryn S. McKinley, Sharad Singhai, Glen E. Weaver, and Charles C. Weems, "Compiler Architectures for Heterogeneous Systems", Languages and Compilers for Parallel Computing, 1995.
01.03.2005 Software aus Komponenten
FOCUS
  • Dirk Heuzeroth, "Aspektorientierte Konfiguration und Adaption von Komponenteninteraktionen", Dissertation an der Universität Karlsruhe, 2004.
  • Manfred Broy, Frank Dederich, Claus Dendorfer, Max Fuchs, Thomas Gritzner, and Rainer Weber, "The Design of Distributed Systems - An Introduction to FOCUS", Technical Report TUM, 1992.
  • Komponenten - alles was man wissen muß (courtesy of JOB 03/05)
08.03.2005 – 05.04.2005 fällt aus
12.04.2005 Verifikation von Programmtransformationen
  • B. Goldberg, L. Zuck, and C. Barrett, "Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers", COCV, 2004.
  • Y. Hu, C. Barrett, B. Goldberg, and A. Pnueli, "Validating More Loop Optimizations", COCV, 2005.
  • K.C. Shashidhar, M. Bruynooghe, F. Catthoor, and G. Janssens, "Verification of Source Code Transformations by Program Equivalence Checking", CC, 2005.
  • J. Condit and G. C. Necula, "Data Slicing: Separating the Heap into Independent Regions", CC, 2005.
19.04.2005 Profitabilität von Programmtransformationen; Templates vs. Objektorientierung
  • M. Zhao, B.R. Childers and M. L. Soffa, "A Model-based Framework: An Approach for Profit-driven Optimization", MICRO, 2005. download
  • A. Stepanov, "An Interview with A. Stepanov", stlport, 2001.link
26.04.2005 Entscheidbarkeit von Typinferenzen;
Befehlsauswahl für Dual Instruction Set Processors;
evtl. Anwendbarkeit von Methoden aus BWL für Optimierungskriterien
  • S. Lee, J. Lee, C.Y. Park and S. L. Min, "A Flexible Tradeoff Between Code Size and WCET Using a Dual Instruction Set Processor", SCOPES, 2004.download
  • M. Odersky and P. Wadler, "Pizza into Java: Translating theory into practice", POPL, 1997. download
03.05.2005 Registerallokation;
Befehlsanordnung
  • J. Park and S.-M. Moon, "Optimistic register coalescing", TOPLAS, 2004.download
10.05.2005 Randomisierung in der Informatik
17.05.2005 fällt aus
24.05.2005 Game Theory (Model Checking)
  • W. Thomas, "Infinite games and verification", CAV'02,2002.download
  • R.Passerone, L. de Alfaro, T.A. Henzinger, A.L. Sangiovanni-Vincentelli, "Convertibility Verification and Converter Synthesis: Two Faces of the Same Coin. ICCAD'02,2002.download
31.05.2005 Probabilistisch verifizierbare Beweise
Wir freuen uns, zu diesem Termin Thilo Mie aus der Arbeitsgruppe von Prof. Calmet als Gast zu haben. Er wird uns von seinen aktuellen Arbeiten erzählen.
  • Thilo Mie: "Lokal überprüfbare Beweise und ihre Anwendungen". abstract
  • S. Arora, S. Safra, "Probabilistic Checking of Proofs: A New Characterization of NP", FOCS, 1992.download
07.06.2005 fällt aus
14.06.2005 Scheduling
  • S. Winkel, "Exploring the Performance Potential of Itanium Processors with ILP-based Scheduling", CGO, 2004.download
21.06.2005 Prozessalgebren
  • J. Parrow, "An Introduction to the pi-Calculus". Handbook of Process Algebra, ed. Bergstra, Ponse, Smolka, pages 479-543, Elsevier 2001. download
  • J.A. Bergstra, A. Ponse, S.A. Smolka (Editors), "Handbook of Process Algebra". Elsevier 2001.link
  • C. Röckl, "On the Mechanized Validation of Infinite-State and Parameterized Reactive and Mobile Systems". Ph.D. Thesis, Fakultät für Informatik, Technische Universität München, 2001. download
28.06.2005 Statecharts
Wir freuen uns, zu diesem Termin Steffen Helke aus der Arbeitsgruppe von Prof. Jähnichen (TU Berlin) als Gast zu haben. Er wird uns von seinen aktuellen Arbeiten erzählen.
  • Steffen Helke: "Maschinengestützte Analyse von Statechartsspezifikationen". abstract
05.07.2005 Speculation
  • J.Lin, T.Chen, W.-C. Hsu, R.D.-C. Ju, T.-F. Ngai, P.-C. Yew, S.Chan, "A Compiler Framework for Speculative Analysis and Optimizations", PLDI'03, 2003. download
  • V.-M. Panait, A. Sasturkar, W.-F. Wong, "Static Identification of Delinquent Loads", CGO'04, 2004. download
  • R.M. Rabbah, H. Sandanagobalane, M. Ekpanyapong, W.-F. Wong, "Compiler Orchestrated Prefetching via Speculation and Predication", ASPLOS'04, 2004. download
  • M. Mock, R. Villamarin, J. Baiocchi, "An Empirical Study of Data Speculation Use on the Intel Itanium 2 Processor", INTERACT'05, 2005. download
12.07.2005 Proof-Carrying Code aus Isabelle-Sicht
  • G.C.Necula, "Proof-Carrying Code". POPL97, 1997. download
  • M.Wildmoser, T.Nipkow, G.Klein, S.Nanz, "Prototyping Proof Carrying Code". Conf. on Theoretical Computer Science (TCS04), 2004. download
  • M.Wildmoser, T.Nipkow, "Asserting Bytecode Safety".ESOP05,2005. download
19.07.2005 Verifikation zustandsbasierter Systeme und ihrer Transformationen
  • Vortrag von Jan Olaf Blech und Andreas Humbert. abstract



Artikel:

  • M. E. Wolf and M. S. Lam, "A data locality optimizing algorithm", PLDI, 1991. download
  • J.O. Blech, S. Glesner, J. Leitner, and S. Mülling, "Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL", COCV, 2005. download


Weitere Artikel auf Anfrage, Mail an    lars (at] ipd [dot) info (dot] uni-karlsruhe [dot) de    (at/dot durch entsprechende Zeichen ersetzen).



last modified: 2005-Jul-14 15:15:28