Disclaimer: This site contains postscript and pdf files of articles that may be covered by copyright. You may browse the articles for your personal use (in the same spirit as you may read a journal or a proceeding article in a public library). Retrieving, copying, redistributing these files may violate the copyright protection law.
KIT-Bibliothek
Recent Papers
| 2013 |
| Journal Articles and Book Chapters |
|
D. Giffhorn, G. Snelting: A New Algorithm for Low-Deterministic Security. |
|
A. Lochbihler: Making the Java Memory Model Safe. |
| Conference Papers |
|
A. Lochbihler: Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler. |
|
H. Bungartz, C. Riesinger, M. Schreiber, G. Snelting, A. Zwinkau: Invasive Computing in HPC with X10. |
|
A. Lochbihler: Light-weight containers for Isabelle: efficient, extensible, nestable. ITP 2013 |
Publications
| 2013 |
| Journal Articles and Book Chapters |
|
J. Breitner: The Correctness of Launchbury's Natural Semantics for Lazy Evaluation. AFP 2013 |
|
A. Lochbihler: Light-weight Containers. AFP 2013 |
| Conference Papers |
|
M. Braun, S. Buchwald, S. Hack, R. Leißa, C. Mallon, A. Zwinkau: Simple and Efficient Construction of Static Single Assignment Form. CC 2013 |
|
J. Graf, M. Hecker, M. Mohr: Using JOANA for Information Flow Control in Java Programs - A Practical Guide. ATPS 2013 |
| Other Publications |
|
J. Graf, M. Hecker, M. Mohr, B. Nordhoff: Lock-sensitive Interference Analysis for Java: Combining Program Dependence Graphs with Dynamic Pushdown Networks. Other Publications |
|
J. Breitner, B. Huffman, N. Mitchell, C. Sternagel: Certified HLints with Isabelle/HOLCF-Prelude. Other Publications |
| 2012 |
| Journal Articles and Book Chapters |
|
L. Rose, M. Herrmannsdoerfer, S. Mazanek, P. V. Gorp, S. Buchwald, T. Horn, E. Kalnina, A. Koch, K. Lano, B. Schätz, M. Wimmer: Graph and model transformation tools for model migration. |
| Ph.D. theses |
|
D. Giffhorn: Slicing of Concurrent Programs and its Application to Information Flow Control. Ph.D. thesis |
|
A. Lochbihler: A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler. Ph.D. thesis |
| Conference Papers |
|
A. Zwinkau, V. Pankratius: AutoTunium: An Evolutionary Tuner for General-Purpose Multicore Applications. ICPADS 2012 |
|
A. Lochbihler: Java and the Java Memory Model -- a Unified, Machine-Checked Formalisation. ESOP 2012 |
|
R. Küsters, T. Truderung, J. Graf: A Framework for the Cryptographic Verification of Java-like Programs. CSF 2012 |
| Other Publications |
|
M. Braun, S. Buchwald, M. Mohr, A. Zwinkau: An X10 Compiler for Invasive Architectures. Technical Report |
|
A. Zwinkau: Resource Awareness for Efficiency in High-Level Programming Languages. Technical Report |
|
J. Graf, M. Hecker, M. Mohr: Using JOANA for Information Flow Control in Java Programs - A Practical Guide. Technical Report |
|
R. Küsters, T. Truderung, J. Graf: A Framework for the Cryptographic Verification of Java-like Programs. Technical Report |
|
D. Giffhorn, G. Snelting: Probabilistic Noninterference Based on Program Dependence Graphs. Technical Report |
|
A. Lochbihler: The Java Memory Model is Type Safe. Technical Report |
| 2011 |
| Journal Articles and Book Chapters |
|
D. Giffhorn: Advanced chopping of sequential and concurrent programs. SQJ |
|
J. Teich, J. Henkel, A. Herkersdorf, D. Schmitt-Landsiedel, W. Schröder-Preikschat, G. Snelting: Invasive Computing: An Overview. |
|
B. Beckert, D. Hofheinz, J. Müller-Quade, A. Pretschner, G. Snelting: Software Security in Virtualized Infrastructures - The Smart
Meter Example. |
| Conference Papers |
|
A. Lochbihler, L. Bulwahn: Animating the Formalised Semantics of a Java-like Language. ITP 2011 |
|
S. Buchwald, A. Zwinkau, T. Bersch: SSA-Based Register Allocation with PBQP. CC '11 |
|
F. Hannig, S. Roloff, G. Snelting, J. Teich, A. Zwinkau: Resource-aware programming and simulation of MPSoC architectures through extension of X10. SCOPES 2011 |
| Other Publications |
|
M. Braun, S. Buchwald, A. Zwinkau: Firm---A Graph-Based Intermediate Representation. Technical Report |
|
A. Lochbihler: A Unified, Machine-Checked Formalisation of Java and the Java Memory Model. Technical Report |
| 2010 |
| Journal Articles and Book Chapters |
|
A. Lochbihler: Coinductive. AFP 2010 |
|
D. Wasserrab, G. Klein, T. Nipkow, L. Paulson: Information Flow Noninterference via Slicing. AFP 2010 |
|
E. Jakumeit, S. Buchwald, M. Kroll: GrGen.NET. |
| Ph.D. theses |
|
D. Wasserrab: From Formal Semantics to Verified Slicing - A Modular Framework with
Applications in Language Based Security. Ph.D. thesis |
| Conference Papers |
|
D. Wasserrab, D. Lohner: Proving Information Flow Noninterference by Reusing a Machine-Checked
Correctness Proof for Slicing. VERIFY 2010 |
|
C. Hammer: Experiences with PDG-based IFC. ESSoS'10 |
|
M. Braun, C. Mallon, S. Hack: Preference-Guided Register Assignment. CC 2010 |
|
A. Lochbihler: Verifying a Compiler for Java Threads. ESOP 2010 |
|
B. Katz, M. Krug, A. Lochbihler, I. Rutter, G. Snelting, D. Wagner: Gateway Decompositions for Constrained Reachability Problems. SEA 2010 |
|
P. Lammich, A. Lochbihler: The Isabelle Collections Framework. ITP 2010 |
|
M. Taghdiri, G. Snelting, C. Sinz: Information Flow Analysis via Path Condition Refinement. FAST 2010 |
|
J. Graf: Speeding up context-, object- and field-sensitive SDG generation. SCAM 2010 |
|
S. Buchwald, A. Zwinkau: Instruction Selection by Graph Transformation. CASES '10 |
| Other Publications |
|
B. Beckert, D. Hofheinz, J. Müller-Quade, A. Pretschner, G. Snelting: Software Security in Virtualized Infrastructures -- The Smart Meter
Example. Technical Report |
| 2008 |
| Journal Articles and Book Chapters |
|
G. Snelting, D. Wasserrab: A Correctness Proof for the Volpano/Smith Security Typing System. AFP 2008 |
|
D. Wasserrab: Towards Certified Slicing. AFP 2008 |
|
G. Snelting: Wissenschaftspolitische Herausforderungen für die Informatik. IS 2008 |
| Conference Papers |
|
A. Lochbihler: Type Safe Nondeterminism - A Formal Semantics of Java Threads. FOOL 2008 |
|
C. Hammer, J. Dolby, M. Vaziri, F. Tip: Dynamic Detection of Atomic-Set-Serializability Violations. ICSE 2008 |
|
C. Hammer, R. Schaade, G. Snelting: Static Path Conditions for Java. PLAS 2008 |
|
D. Wasserrab, A. Lochbihler: Formalizing a Framework for Dynamic Slicing of Program Dependence
Graphs in Isabelle/HOL. TPHOLS 2008 |
|
D. Giffhorn, C. Hammer: Precise Analysis of Java Programs using JOANA (Tool Demonstration). SCAM 2008 |
| Other Publications |
|
C. Hammer, G. Snelting: Flow-Sensitive, Context-Sensitive, and Object-sensitive Information
Flow Control Based on Program Dependence Graphs. Technical Report |
| 2006 |
| Journal Articles and Book Chapters |
|
D. Wasserrab: CoreC++. AFP 2006 |
|
G. Snelting, T. Robschink, J. Krinke: Efficient Path Conditions in Dependence Graphs for Software Safety
Analysis. TOSEM 2006 |
| Conference Papers |
|
M. Störzer, F. Forster, R. Sterr: Detecting Precedence-Related Advice Interference. ASE 2006 |
|
C. Hammer, M. Grimme, J. Krinke: Dynamic Path Conditions in Dependence Graphs. PEPM 2006 |
|
C. Hammer, J. Krinke, G. Snelting: Information Flow Control for Java Based on Path Conditions in Dependence
Graphs. ISSSE 2006 |
|
M. Störzer, U. Eibauer, S. Schöffmann: Aspect Mining for Aspect Refactoring: An Experience Report. TEAM 2006 |
|
D. Wasserrab, T. Nipkow, G. Snelting, F. Tip: An Operational Semantics and Type Safety Proof for Multiple Inheritance
in C++. OOPSLA 2006 |
|
M. Störzer, B. Ryder, X. Ren, F. Tip: Finding Failure Inducing Changes in Java Programs using Change Classification. FSE 2006 |
|
C. Hammer, J. Krinke, F. Nodes: Intransitive Noninterference in Dependence Graphs. ISoLA 2006 |
| 1999 |
| Journal Articles and Book Chapters |
|
J. Krinke, T. Robschink, G. Snelting: Software-Sicherheitsprüfung mit VALSOFT. IFE 1999 |
|
A. Zeller: Funktionell und verständlich programmieren - so lernen es die Passauer. STT 1999 |
| Ph.D. theses |
|
C. Lindig: Algorithmen zur Begriffsanalyse und ihre Anwendung bei Softwarebibliotheken. Ph.D. thesis |
| Conference Papers |
|
J. Krinke, T. Robschink: Kombination von Slicing und Constraint-Solving für Software-Reengineering. WSR 1999 |
|
C. Lindig, G. Snelting: Formale Begriffsanalyse im Software Engineering. TR 1999 |
|
T. Robschink, J. Krinke: Heuristische Graphzerlegung für redundanzarme Pfadbedingungen in
ValSoft. GWGI 1999 |
|
K. Frühauf, A. Zeller: Software Configuration Management - State of the Art, State of the
Practice. SCM 1999 |
|
M. Streckenbach, G. Snelting: Understanding Class Hierarchies with KABA. WOOR 1999 |
|
A. Zeller: Yesterday, my program worked. Today, it does not. Why?. ESEC/FSE 1999 |
| Other Publications |
|
G. Snelting: Software Technology Group: 1998 Department Report. Technical Report |
| 1998 |
| Journal Articles and Book Chapters |
|
B. Fischer, J. Schumann, G. Snelting, W. Bibel, P. H. Schmitt: Deduction-Based Software Component Retrieval. AD(III) 1998 |
|
G. Snelting: Paul Feyerabend und die Softwaretechnologie. IS 1998 |
|
G. Snelting: Paul Feyerabend and software technology. STTT 1998 |
|
J. Krinke, G. Snelting: Validation of Measurement Software as an Application of Slicing and
Constraint Solving. IST 1998 |
| Conference Papers |
|
J. Krinke, G. Snelting, T. Robschink: Software-Sicherheitsprüfung mit VALSOFT. ST 1998 |
|
B. Fischer: Specification-Based Browsing of Software Component Libraries. ASE 1998 |
|
G. Snelting: Concept Analysis - A New Framework for Program Understanding. PASTE 1998 |
|
A. Rossberg: Functional Programming-in-the-Large Using M. WFLP 1998 |
|
J. Krinke: Static Slicing of Threaded Programs. PASTE 1998 |
|
A. Zeller: Versioning System Models through Description Logic. SCM 1998 |
|
G. Snelting, F. Tip: Reengineering Class Hierarchies Using Concept Analysis. FSE 1998 |
| Other Publications |
|
C. Lindig: Analyse von Softwarevarianten. Technical Report |
|
C. Lindig: Analysis of Software Variants. Other Publications |
|
H. Müller, T. Reps, G. Snelting: Program Comprehension and Software Reengineering. Technical Report |
| 1997 |
| Journal Articles and Book Chapters |
|
G. Snelting: Paul Feyerabend und die Softwaretechnologie. ST 1997 |
|
A. Zeller, G. Snelting: Unified Versioning Through Feature Logic. TOSEM 1997 |
| Ph.D. theses |
|
A. Zeller: Configuration Management with Version Sets - A Unified Software Versioning
Model and its Applications. Ph.D. thesis |
| Conference Papers |
|
C. Lindig, G. Snelting: Assessing Modular Structure of Legacy Code Based on Mathematical
Concept Analysis. ICSE 1997 |
|
F. Grosch, J. Schumann: M - eine typisierte, funktionale Sprache für das Programmieren-im-Großen. IS 1997 |
|
B. Fischer, G. Snelting: Reuse by Contract. FCBS 1997 |
|
B. Fischer, J. Schumann: NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical. WATPSE 1997 |
|
B. Fischer, J. Schumann: SETHEO Goes Software Engineering: Application of ATP to Software
Reuse. CADE 1997 |
|
J. Schumann, B. Fischer: NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical. ASE 1997 |
| Other Publications |
|
G. Snelting, U. Grottker, M. Goldapp: VALSOFT Abschlussbericht. Other Publications |
| 1995 |
| Conference Papers |
|
B. Fischer, M. Kievernagel, W. Struckmann: VCR: A VDM-based software component retrieval tool. ISCE 1995 |
|
F. Grosch: Eine typisierte, rein funktionale Modulsprache für das Programmieren-im-Großen. WGI 1995 |
|
B. Fischer, M. Kievernagel, W. Struckmann: High-Precision Retrieval for High-Quality Software. SQC 1995 |
|
C. Lindig: Concept-Based Component Retrieval. IJCAI 1995 |
|
B. Fischer, M. Kievernagel, G. Snelting: Deduction-Based Software Component Retrieval. IJCAI 1995 |
|
A. Zeller, G. Snelting: Handling Version Sets through Feature Logic. ESEC 1995 |
|
A. Zeller: A Unified Version Model for Configuration Management. FSE 1995 |
|
C. Lindig: Komponentensuche mit Begriffen. ST 1995 |
| Other Publications |
|
G. Snelting: Reengineering of Configurations Based on Mathematical Concept Analysis. Technical Report |
|
F. Grosch: No Type Stamps and No Structure Stamps - A Referentially-Transparent
Higher-Order Module Language. Technical Report |
|
P. Funk, A. Lewien, G. Snelting: Algorithms for Concept Lattice Decomposition and their Applications. Technical Report |
