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.
| Conference Papers |
|
A. Fried, M. Stemmer-Grabow, J. Wachter: Register Allocation for Compressed ISAs in LLVM. CC '23 |
|
S. Ullrich, L. d. Moura: 'do' Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl). ICFP 2022 |
|
L. d. Moura, S. Ullrich: The Lean 4 Theorem Prover and Programming Language. CADE 28 |
|
J. Bechberger, A. Weigl: Upper Bound Computation of Information Leakages for Unbounded Recursion. |
|
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 |
|
S. Rheindt, A. Fried, O. Lenke, L. Nolte, T. Wild, A. Herkersdorf: NEMESYS: Near-Memory Graph Copy Enhanced System-Software. MEMSYS 2019 |
|
N. Kraus, J. v. Raumer: Path Spaces of Higher Inductive Types in Homotopy Type Theory. |
|
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 |
|
S. Greiner, M. Mohr, B. Beckert: Modular Verification of Information Flow Security in Component-Based Systems. SEFM 2017 |
|
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 |
|
A. Zwinkau: An X10 Memory Model. X10 2016 |
|
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 |
|
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 |
|
M. Witterauf, A. Tanase, J. Teich, V. Lari, A. Zwinkau, G. Snelting: Adaptive fault tolerance through invasive computing. |
|
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). |
|
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 |
|
J. Graf, M. Hecker, M. Mohr: Using JOANA for Information Flow Control in Java Programs - A Practical Guide. ATPS 2013 |
|
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 |
|
R. Küsters, T. Truderung, J. Graf: A Framework for the Cryptographic Verification of Java-like Programs. CSF 2012 |
|
A. Lochbihler: Java and the Java Memory Model -- a Unified, Machine-Checked Formalisation. ESOP 2012 |
|
A. Zwinkau, V. Pankratius: AutoTunium: An Evolutionary Tuner for General-Purpose Multicore Applications. ICPADS 2012 |
|
F. Hannig, S. Roloff, G. Snelting, J. Teich, A. Zwinkau: Resource-aware programming and simulation of MPSoC architectures through extension of X10. SCOPES 2011 |
|
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 |
|
S. Buchwald, A. Zwinkau: Instruction Selection by Graph Transformation. CASES '10 |
|
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 |
|
P. Lammich, A. Lochbihler: The Isabelle Collections Framework. ITP 2010 |
|
B. Katz, M. Krug, A. Lochbihler, I. Rutter, G. Snelting, D. Wagner: Gateway Decompositions for Constrained Reachability Problems. SEA 2010 |
|
M. Braun, C. Mallon, S. Hack: Preference-Guided Register Assignment. CC 2010 |
|
A. Lochbihler: Verifying a Compiler for Java Threads. ESOP 2010 |
|
C. Hammer: Experiences with PDG-based IFC. ESSoS'10 |
|
D. Wasserrab, D. Lohner: Proving Information Flow Noninterference by Reusing a Machine-Checked
Correctness Proof for Slicing. VERIFY 2010 |
|
D. Giffhorn: Chopping Concurrent Programs. SCAM 2009 |
|
A. Lochbihler: Formalising FinFuns - Generating Code for Functions as Data from
Isabelle/HOL. TPHOLs 2009 |
|
D. Wasserrab, D. Lohner, G. Snelting: On PDG-Based Noninterference and its Modular Proof. PLAS 2009 |
|
M. Braun, S. Hack: Register Spilling and Live-Range Splitting for SSA-Form Programs. CC 2009 |
|
D. Giffhorn, C. Hammer: Precise Analysis of Java Programs using JOANA (Tool Demonstration). SCAM 2008 |
|
D. Wasserrab, A. Lochbihler: Formalizing a Framework for Dynamic Slicing of Program Dependence
Graphs in Isabelle/HOL. TPHOLS 2008 |
|
C. Hammer, R. Schaade, G. Snelting: Static Path Conditions for Java. PLAS 2008 |
|
C. Hammer, J. Dolby, M. Vaziri, F. Tip: Dynamic Detection of Atomic-Set-Serializability Violations. ICSE 2008 |
|
A. Lochbihler: Type Safe Nondeterminism - A Formal Semantics of Java Threads. FOOL 2008 |
|
D. Giffhorn, C. Hammer: An Evaluation of Slicing Algorithms for Concurrent Programs. SCAM 2007 |
|
A. Lochbihler, G. Snelting: On Temporal Path Conditions in Dependence Graphs. SCAM 2007 |
|
D. Wasserrab, T. Nipkow, G. Snelting, F. Tip: C++ ist typsicher? Garantiert!. SE 2007 |
|
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 |
|
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, U. Eibauer, S. Schöffmann: Aspect Mining for Aspect Refactoring: An Experience Report. TEAM 2006 |
|
C. Hammer, J. Krinke, G. Snelting: Information Flow Control for Java Based on Path Conditions in Dependence
Graphs. ISSSE 2006 |
|
C. Hammer, M. Grimme, J. Krinke: Dynamic Path Conditions in Dependence Graphs. PEPM 2006 |
|
M. Störzer, F. Forster, R. Sterr: Detecting Precedence-Related Advice Interference. ASE 2006 |
|
G. Snelting: Quantifier Elimination and Information Flow Control for Software
Security. A3L 2005 |
|
M. Störzer, S. Hanenberg: A Classification of Pointcut Language Constructs. SPLAT 2005 |
|
M. Störzer, J. Graf: Using Pointcut Delta Analysis to Support Evolution of Aspect-Oriented
Software. ICSM 2005 |
|
M. Streckenbach, G. Snelting: Refactoring Class Hierarchies with KABA. OOPSLA 2004 |
|
C. Constantinides, T. Skotiniotis, M. Störzer: AOP Considered Harmful. EIWAS 2004 |
|
M. Störzer, C. Koppen: PCDiff: Attacking the Fragile Pointcut Problem, Abstract. EIWAS 2004 |
|
C. Hammer, G. Snelting: An Improved Slicer for Java. PASTE 2004 |
|
S. Breu, J. Krinke: Aspect Mining Using Event Traces. ASE 2004 |
|
J. Krinke: Barrier Slicing and Chopping. SCAM 2003 |
|
J. Krinke: Context-Sensitive Slicing of Concurrent Programs. FSE 2003 |
|
M. Störzer, J. Krinke, S. Breu: Trace Analysis for Aspect Application. AAOS 2003 |
|
S. Breu, J. Krinke: Aspect Mining Using Dynamic Analysis. WSR 2003 |
|
M. Störzer: Analysis of AspectJ Programs. GIAOSD 2003 |
|
M. Störzer, J. Krinke: Interference Analysis for AspectJ. FOAL 2003 |
|
A. D. Lucia, M. Harman, R. Hierons, J. Krinke: Unions of Slices are not Slices. CSMR 2003 |
|
G. Snelting: Concept Lattices in Software Analysis. ICFCA 2003 |
|
J. Krinke: Evaluating Context-Sensitive Slicing and Chopping. ICSM 2002 |
|
G. Snelting, F. Tip: Semantics-Based Composition of Class Hierarchies. ECOOP 2002 |
|
T. Robschink, G. Snelting: Efficient Path Conditions in Dependence Graphs. ICSE 2002 |
|
J. Krinke: Identifying Similar Code with Program Dependence Graphs. WCRE 2001 |
|
J. Krinke: Identifizierung von ähnlichem Code mit Programmabhängigkeitsgraphen. WSR 2001 |
|
H. Cleve, A. Zeller: Finding Failure Causes through Automated Testing. AADEBUG 2000 |
|
R. Hildebrandt, A. Zeller: Simplifying Failure-Inducing Input. ISSTA 2000 |
|
A. Zeller: Making Students Read and Review Code. ITiCSE 2000 |
|
A. Zeller: Datenstrukturen visualisieren und animieren mit DDD. SV 2000 |
|
G. Snelting: Software Reengineering Based on Concept Lattices. CSMR 2000 |
|
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 |
|
T. Robschink, J. Krinke: Heuristische Graphzerlegung für redundanzarme Pfadbedingungen in
ValSoft. GWGI 1999 |
|
C. Lindig, G. Snelting: Formale Begriffsanalyse im Software Engineering. TR 1999 |
|
J. Krinke, T. Robschink: Kombination von Slicing und Constraint-Solving für Software-Reengineering. WSR 1999 |
|
G. Snelting, F. Tip: Reengineering Class Hierarchies Using Concept Analysis. FSE 1998 |
|
A. Zeller: Versioning System Models through Description Logic. SCM 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 |
|
J. Krinke, G. Snelting, T. Robschink: Software-Sicherheitsprüfung mit VALSOFT. ST 1998 |
|
B. Fischer: Specification-Based Browsing of Software Component Libraries. ASE 1998 |
|
J. Schumann, B. Fischer: NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical. ASE 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 |
|
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 |
|
G. Snelting: Combining Slicing and Constraint Solving for Validation of Measurement
Software. SAS 1996 |
|
A. Zeller: Software Configuration with Feature Logic. WRKP 1996 |
|
A. Zeller: Smooth operations with square operators - The version set model in
ICE. SCM 1996 |
|
A. Zeller: A Unified Version Model for Configuration Management. FSE 1995 |
|
C. Lindig: Komponentensuche mit Begriffen. ST 1995 |
|
A. Zeller, G. Snelting: Handling Version Sets through Feature Logic. ESEC 1995 |
|
C. Lindig: Concept-Based Component Retrieval. IJCAI 1995 |
|
B. Fischer, M. Kievernagel, G. Snelting: Deduction-Based Software Component Retrieval. IJCAI 1995 |
|
B. Fischer, M. Kievernagel, W. Struckmann: High-Precision Retrieval for High-Quality Software. SQC 1995 |
|
F. Grosch: Eine typisierte, rein funktionale Modulsprache für das Programmieren-im-Großen. WGI 1995 |
|
B. Fischer, M. Kievernagel, W. Struckmann: VCR: A VDM-based software component retrieval tool. ISCE 1995 |
|
M. Krone, G. Snelting: On the Inference of Configuration Structures from Source Code. ICSE 1994 |
|
C. Lindig: STYLE - A Practical Type Checker for Scheme. SAGEGP 1994 |
|
G. Snelting, A. Zeller: Inferenzbasierte Werkzeuge in NORA. ST 1993 |
|
B. Fischer: Resolution for Feature Logics. WGI 1993 |
|
F. Grosch, G. Snelting: Polymorphic Components for Monomorphic Languages. IWSR-2 1993 |
|
G. Snelting, F. Grosch, U. Schroeder: Inference-Based Support for Programming in the Large. ESEC 1991 |
|
T. Nipkow, G. Snelting: Type Classes and Overloading Resolution via Order-Sorted Unification. FPCA 1991 |
|
W. Henhapl, S. Kaes, G. Snelting: Utilizing fifth generation technology in software development tools. ESSDE 1991 |
