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
Publications
2020 |
Journal Articles and Book Chapters |
S. Graf, S. P. Jones, R. G. Scott: Lower Your Guards: A Compositional Pattern-Match Coverage Checker. ICFP 2020 |
Ph.D. theses |
J. v. Raumer: Higher Inductive Types, Inductive Families, and Inductive-Inductive Types. Ph.D. thesis |
M. Hecker: Timing Sensitive Dependency Analysis and its Application to Software Security. Ph.D. thesis |
Conference Papers |
A. Kaposi, J. v. Raumer: A Syntax for Mutual Inductive Families. |
S. Ullrich, L. d. Moura: Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. IJCAR 2020 |
N. Kraus, J. v. Raumer: Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type
Theory. |
F. D. Loch, M. Johns, M. Hecker, M. Mohr, G. Snelting: Hybrid Taint Analysis for Java EE. SAC 2020 |
S. Rheindt, A. Fried, O. Lenke, L. Nolte, T. Twardzik, T. Wild, A. Herkersdorf: X-CEL: A Method to Estimate Near-Memory Acceleration Potential in Tile-based MPSoCs. ARCS 2020 |
2018 |
Journal Articles and Book Chapters |
S. Bischof, J. Breitner, D. Lohner, G. Snelting: Illi Isabellistes Se Custodes Egregios Praestabant. |
S. Bischof, J. Breitner, J. Graf, M. Hecker, M. Mohr, G. Snelting: Low-Deterministic Security For Low-Nondeterministic Programs. JCS |
Ph.D. theses |
A. Zwinkau: Resource-aware Programming in a High-level Language -- Improved performance with manageable effort on clustered MPSoCs. Ph.D. thesis |
M. Mohr: Aspects of Code Generation and Data Transfer Techniques for Modern Parallel Architectures. Ph.D. thesis |
Conference Papers |
T. Hamann, M. Herda, H. Mantel, M. Mohr, D. Schneider, M. Tasch: A Uniform Information-Flow Security Benchmark Suite For Source Code and Bytecode. |
S. Buchwald, A. Fried, S. Hack: Synthesizing an Instruction Selection Rule Library from Semantic Specifications. CGO '18 |
B. Beckert, S. Bischof, M. Herda, M. Kirsten, M. K. Büning: Using Theorem Provers to Increase the Precision of Dependence Analysis
for Information Flow Control. ICFEM 2018 |
2017 |
Journal Articles and Book Chapters |
J. Breitner, M. Hecker, G. Snelting: Der Grader Praktomat. Automatisierte Bewertung in der Programmierausbildung |
M. Wagner, D. Lohner: Minimal Static Single Assignment Form. AFP 2017 |
G. Ebner, S. Ullrich, J. Roesch, J. Avigad, L. d. Moura: A Metaprogramming Framework for Formal Verification. PACMPL ICFP 2017 |
Conference Papers |
B. Beckert, S. Bischof, M. Herda, M. Kirsten, M. K. Büning: Combining Graph-Based and Deduction-Based Information-Flow Analysis. HOTSPOT 2017 |
F. v. Doorn, J. v. Raumer, U. Buchholtz: Homotopy Type Theory in Lean. |
M. Mohr, C. Tradowsky: Pegasus: Efficient Data Transfers for PGAS Languages on Non-Cache-Coherent Many-Cores. DATE 2017 |
S. Greiner, M. Mohr, B. Beckert: Modular Verification of Information Flow Security in Component-Based Systems. SEFM 2017 |
Other Publications |
M. E. Kramer, M. Hecker, S. Greiner, K. Bao, K. Yurchenko: Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems. |
2016 |
Journal Articles and Book Chapters |
S. Wildermann, M. Bader, L. Bauer, M. Damschen, D. Gabriel, M. Gerndt, M. Glaß, J. Henkel, J. Paul, A. Pöppl, S. Roloff, T. Schwarzer, G. Snelting, W. S. a: Invasive Computing for Timing-Predictable Stream Processing on MPSOCS. it 2016 |
S. Ullrich, D. Lohner: Verified Construction of Static Single Assignment Form. AFP 2016 |
J. Breitner, D. Lohner: The meta theory of the Incredible Proof Machine. AFP 2016 |
J. Breitner, R. Eisenberg, S. P. Jones, S. Weirich: Safe zero-cost coercions for Haskell. |
Ph.D. theses |
J. Breitner: Lazy Evaluation: From natural semantics to a machine-checked compiler transformation. Ph.D. thesis |
J. Graf: Information Flow Control with System Dependence Graphs -- Improving Modularity, Scalability and Precision for Object Oriented Languages. Ph.D. thesis |
Conference Papers |
J. v. Raumer: Formalizing Double Groupoids and Cross Modules in the Lean Theorem
Prover. |
J. Breitner, J. Graf, M. Hecker, M. Mohr, G. Snelting: On Improvements Of Low-Deterministic Security. POST 16 |
J. Graf, M. Hecker, M. Mohr, G. Snelting: Sicherheitsanalyse mit JOANA. Sicherheit 2016 |
J. Graf, M. Hecker, M. Mohr, G. Snelting: Tool Demonstration: JOANA. POST 16 |
S. Buchwald, D. Lohner, S. Ullrich: Verified Construction of Static Single Assignment Form. CC 2016 |
J. Breitner: Visual theorem proving with the Incredible Proof Machine. ITP 2016 |
A. Zwinkau: An X10 Memory Model. X10 2016 |
2015 |
Journal Articles and Book Chapters |
D. Giffhorn, G. Snelting: A new algorithm for low-deterministic security. IJIS |
G. Snelting: Understanding Probabilistic Software Leaks. SCP 2015 |
J. Breitner: The Safety of Call Arity. AFP 2015 |
Conference Papers |
J. Breitner: Call Arity. TFP 2014 |
M. Mohr, S. Buchwald, A. Zwinkau, C. Erhardt, B. Oechslein, J. Schedel, D. Lohmann: Cutting Out the Middleman: OS-Level Support for X10 Activities. X10 2015 |
J. Breitner: Formally Proving a Compiler Transformation Safe. Haskell'15 |
M. Mohr, J. Graf, M. Hecker: JoDroid: Adding Android Support to a Static Information Flow Control Tool. |
S. Buchwald, M. Mohr, A. Zwinkau: Malleable Invasive Applications. ATPS 2015 |
S. Buchwald: Optgen: A Generator for Local Optimizations. CC 2015 |
S. Buchwald, M. Mohr, I. Rutter: Optimal Shuffle Code with Permutation Instructions. WADS 2015 |
E. Lovat, A. Fromm, M. Mohr, A. Pretschner: SHRIFT System-Wide HybRid Information Flow Tracking. IFIPSec 2015 |
L. M. d. Moura, S. Kong, J. Avigad, F. v. Doorn, J. v. Raumer: The Lean Theorem Prover (System Description). |
M. Witterauf, A. Tanase, J. Teich, V. Lari, A. Zwinkau, G. Snelting: Adaptive fault tolerance through invasive computing. |
R. Küsters, T. Truderung, B. Beckert, D. Bruns, M. Kirsten, M. Mohr: A Hybrid Approach for Proving Noninterference of Java Programs. CSF 2015 |
J. Graf, M. Hecker, M. Mohr, G. Snelting: Checking Applications using Security APIs with JOANA. ASA 2015 |
Other Publications |
J. Breitner, C. Podszun: Stiftzauber -- Eigene Bücher und Spiele für den Tiptoi vertonen. c't 08/15 |
S. Buchwald, M. Mohr, I. Rutter: Optimal Shuffle Code with Permutation Instructions. arXiv.org |
G. Snelting: Rezension zu "M. Zollner: Physik der Elektrogitarre". Spektrum der Wissenschaft |
J. Breitner, C. Podszun: Punktgenau -- Multimedia-Spielzeug Tiptoi selbst programmieren. Make: 06/15 |
2014 |
Journal Articles and Book Chapters |
E. Jakumeit, S. Buchwald, D. Wagelaar, L. Dan, Á. Hegedüs, M. Herrmannsdörfer, T. Horn, E. Kalnina, C. Krause, K. Lano, M. Lepper, A. Rensink, L. Rose, S. Wätzol: A survey and comparison of transformation tools based on the transformation tool contest. SCP 2014 |
A. Lochbihler: Making the Java Memory Model Safe. TOPLAS 2014 |
S. Stork, K. Naden, J. Sunshine, M. Mohr, A. Fonseca, P. Marques, J. Aldrich: AEminium: A Permission Based Concurrent-by-Default Programming Language Approach. TOPLAS 2014 |
G. Snelting, D. Giffhorn, J. Graf, C. Hammer, M. Hecker, M. Mohr, D. Wasserrab: Checking Probabilistic Noninterference Using JOANA. IT 2014 |
Conference Papers |
J. Heisswolf, A. Zaib, A. Zwinkau, S. Kobbe, A. Weichslgartner, J. Teich, J. Henkel, G. Snelting, A. Herkersdorf, J. Becker: CAP: Communication Aware Programming. DAC 2014 |
R. Küsters, E. Scapin, T. Truderung, J. Graf: Extending and Applying a Framework for the Cryptographic Verification of Java Programs. POST 14 |
J. Breitner, R. Eisenberg, S. P. Jones, S. Weirich: Safe Zero-cost Coercions for Haskell. ICFP 2014 |
Other Publications |
R. Küsters, E. Scapin, T. Truderung, J. Graf: (accompanying technical report) Extending and Applying a Framework for the Cryptographic Verification of Java Programs.. Other Publications |
M. Braun, S. Buchwald, M. Mohr, A. Zwinkau: Dynamic X10: Resource-Aware Programming for Higher Efficiency. |
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 |
A. Lochbihler: Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler. LNI - Ausgezeichnete Informatikdissertationen 2012 |
M. Mohr, A. Grudnitsky, T. Modschiedler, L. Bauer, S. Hack, J. Henkel: Hardware Acceleration for Programs in SSA Form. CASES 2013 |
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 |
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 |
A. Zwinkau, S. Buchwald, G. Snelting: InvadeX10 Documentation v0.5. |
J. Graf, M. Hecker, M. Mohr, B. Nordhoff: Lock-sensitive Interference Analysis for Java: Combining Program Dependence Graphs with Dynamic Pushdown Networks. ID 2013 |
R. Küsters, T. Truderung, B. Beckert, D. Bruns, J. Graf, C. Scheben: A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java Programs. GRSRD 2013 |
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. |
A. Zwinkau: Resource Awareness for Efficiency in High-Level Programming Languages. |
J. Graf, M. Hecker, M. Mohr: Using JOANA for Information Flow Control in Java Programs - A Practical Guide. |
R. Küsters, T. Truderung, J. Graf: (accompanying technical report) A Framework for the Cryptographic Verification of Java-like Programs. |
D. Giffhorn, G. Snelting: Probabilistic Noninterference Based on Program Dependence Graphs. |
A. Lochbihler: The Java Memory Model is Type Safe. |
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. |
A. Lochbihler: A Unified, Machine-Checked Formalisation of Java and the Java Memory Model. |
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. |
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. |
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. TR 1999 |
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. TR 1998 |
C. Lindig: Analysis of Software Variants. PURE 1998 |
H. Müller, T. Reps, G. Snelting: Program Comprehension and Software Reengineering. |
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. TR 1997 |
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. CSR 1995 |
F. Grosch: No Type Stamps and No Structure Stamps - A Referentially-Transparent
Higher-Order Module Language. CSR 1995 |
P. Funk, A. Lewien, G. Snelting: Algorithms for Concept Lattice Decomposition and their Applications. CSR 1995 |