| 2026 | CAV | Modular Reasoning About Object Relations. | Micha Greutmann, Marco Eilers, Peter Mller |
| 2026 | SP | The Secrets Must Not Flow: Scaling Security Verification to Large Codebases. | Linard Arquint, Samarth Kishor, Jason R. Koenig, Joey Dodds, Daniel Kroening, Peter Mller |
| 2026 | TACAS | SMTScope: Automated and Efficient Analysis of SMT Traces. | Jons Fiala, Peter Mller |
| 2025 | CAV | Fifteen Years of Viper. | Marco Eilers, Malte Schwerhoff, Alexander J. Summers, Peter Mller |
| 2025 | CAV | Accelerating Automated Program Verifiers by Automatic Proof Localization. | Kiran Gopinathan, Dionysios Spiliopoulos, Vikram Goyal, Peter Mller, Markus Pschel, Ilya Sergey |
| 2025 | CCS | Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router. | Joo C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David A. Basin, Peter Mller, Adrian Perrig |
| 2024 | CAV | Verification Algorithms for Automated Separation Logic Verifiers. | Marco Eilers, Malte Schwerhoff, Peter Mller |
| 2024 | CCS | Verifiable Security Policies for Distributed Systems. | Felix A. Wolf, Peter Mller |
| 2024 | ICLR | GraphChef: Decision-Tree Recipes to Explain Graph Neural Networks. | Peter Mller, Lukas Faber, Karolis Martinkus, Roger Wattenhofer |
| 2023 | CCS | A Generic Methodology for the Modular Verification of Security Protocol Implementations. | Linard Arquint, Malte Schwerhoff, Vaibhav Mehta, Peter Mller |
| 2023 | SP | Sound Verification of Security Protocols: From Design to Interoperable Implementations. | Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David A. Basin, Peter Mller |
| 2022 | CAV | Sound Automation of Magic Wands. | Thibault Dardinier, Gaurav Parthasarathy, No Weeks, Peter Mller, Alexander J. Summers |
| 2021 | CAV | Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. | Marco Eilers, Severin Meier, Peter Mller |
| 2021 | CAV | Formally Validating a Practical Verification Condition Generator. | Gaurav Parthasarathy, Peter Mller, Alexander J. Summers |
| 2021 | CAV | Gobra: Modular Specification and Verification of Go Programs. | Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, Joo Carlos Pereira, Peter Mller |
| 2021 | FM | Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers. | Alexandra Bugariu, Arshavir Ter-Gabrielyan, Peter Mller |
| 2021 | FM | Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA. | Felix A. Wolf, Malte Schwerhoff, Peter Mller |
| 2020 | ICSE | Automatically testing string solvers. | Alexandra Bugariu, Peter Mller |
| 2019 | TACAS | The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. | Nils Becker, Peter Mller, Alexander J. Summers |
| 2018 | CAV | Permission Inference for Array Programs. | Jrme Dohrau, Alexander J. Summers, Caterina Urban, Severin Mnger, Peter Mller |
| 2018 | CAV | Nagini: A Static Verifier for Python. | Marco Eilers, Peter Mller |
| 2018 | CAV | MaxSMT-Based Type Inference for Python 3. | Mostafa Hassan, Caterina Urban, Marco Eilers, Peter Mller |
| 2018 | ESOP | Modular Product Programs. | Marco Eilers, Peter Mller, Samuel Hitz |
| 2018 | ESOP | An Abstract Interpretation Framework for Input Data Usage. | Caterina Urban, Peter Mller |
| 2018 | ICINCO | Root Cause Analysis of Deep Drawing Processes with Superimposed Low-Frequency Vibrations on Servo-Screw Presses - A Practical Research on Predictability in Simulation. | Andr Sewohl, Sebastian Kriechenbauer, Peter Mller, Holger Schlegel, Dirk Landgrebe |
| 2018 | PLDI | Static serializability analysis for causal consistency. | Lucas Brutschy, Dimitar Dimitrov, Peter Mller, Martin T. Vechev |
| 2018 | SAS | Abstract Interpretation of CTL Properties. | Caterina Urban, Samuel Ueltschi, Peter Mller |
| 2018 | TACAS | Automating Deductive Verification for Weak-Memory Programs. | Alexander J. Summers, Peter Mller |
| 2017 | FASE | Precise Version Control of Trees with Line-Based Version Control Systems. | Dimitar Asenov, Balz Guenat, Peter Mller, Martin Otth |
| 2017 | ICSE | A general framework for dynamic stub injection. | Maria Christakis, Patrick Emmisberger, Patrice Godefroid, Peter Mller |
| 2017 | POPL | Serializability for eventual consistency: criterion, analysis, and applications. | Lucas Brutschy, Dimitar Dimitrov, Peter Mller, Martin T. Vechev |
| 2016 | CAV | Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. | Peter Mller, Malte Schwerhoff, Alexander J. Summers |
| 2016 | CHI | The Effect of Richer Visualizations on Code Comprehension. | Dimitar Asenov, Otmar Hilliges, Peter Mller |
| 2016 | ESOP | Actor Services - Modular Verification of Message Passing Programs. | Alexander J. Summers, Peter Mller |
| 2016 | ICSE | Guiding dynamic symbolic execution toward unverified program executions. | Maria Christakis, Peter Mller, Valentin Wstholz |
| 2016 | PSB | A Bayesian Nonparametric Model for Reconstructing Tumor Subclones Based on Mutation Pairs. | Subhajit Sengupta, Tianjian Zhou, Peter Mller, Yuan Ji |
| 2016 | TACAS | Integrated Environment for Diagnosing Verification Errors. | Maria Christakis, K. Rustan M. Leino, Peter Mller, Valentin Wstholz |
| 2016 | TACAS | Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets). | Cdric Favre, Hagen Vlzer, Peter Mller |
| 2016 | VMCAI | Viper: A Verification Infrastructure for Permission-Based Reasoning. | Peter Mller, Malte Schwerhoff, Alexander J. Summers |
| 2015 | ECOOP | Modular Verification of Finite Blocking in Non-terminating Programs. | Pontus Bostrm, Peter Mller |
| 2015 | POPL | Building automatic program verifiers. | Peter Mller |
| 2015 | PSB | BayClone: Bayesian Nonparametric Inference of Tumor Subclones Using NGS Data. | Subhajit Sengupta, Jing Wang, Juhee Lee, Peter Mller, Kamalakar Gulukota, Arunava Banerjee, Yuan Ji |
| 2015 | VMCAI | An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer. | Maria Christakis, Peter Mller, Valentin Wstholz |
| 2015 | VMCAI | Automatic Inference of Heap Properties Exploiting Value Domains. | Pietro Ferrara, Peter Mller, Milos Novcek |
| 2014 | ECOOP | Constraint Semantics for Abstract Read Permissions. | John Tang Boyland, Peter Mller, Malte Schwerhoff, Alexander J. Summers |
| 2014 | OOPSLA | Static analysis for independent app developers. | Lucas Brutschy, Pietro Ferrara, Peter Mller |
| 2014 | OOPSLA | TouchGuru: Integrating Static Analysis with a Mobile Development Environment. | Lucas Brutschy, Pietro Ferrara, Peter Mller |
| 2014 | RV | Dynamic Test Generation with Static Fields and Initializers. | Maria Christakis, Patrick Emmisberger, Peter Mller |
| 2014 | SEFM | Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations. | Maria Christakis, Peter Mller, Valentin Wstholz |
| 2013 | ECOOP | Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions. | Stefan Heule, Ioannis T. Kassios, Peter Mller, Alexander J. Summers |
| 2013 | VMCAI | Abstract Read Permissions: Fractional Permissions without the Fractions. | Stefan Heule, K. Rustan M. Leino, Peter Mller, Alexander J. Summers |
| 2012 | FM | Collaborative Verification and Testing with Explicit Assumptions. | Maria Christakis, Peter Mller, Valentin Wstholz |
| 2012 | VMCAI | Automatic Inference of Access Permissions. | Pietro Ferrara, Peter Mller |
| 2011 | ECOOP | Tunable Static Inference for Generic Universe Types. | Werner Dietl, Michael D. Ernst, Peter Mller |
| 2011 | ECOOP | Fractional permissions without the fractions. | Stefan Heule, K. Rustan M. Leino, Peter Mller, Alexander J. Summers |
| 2011 | FM | The 1st Verified Software Competition: Experience Report. | Vladimir Klebanov, Peter Mller, Natarajan Shankar, Gary T. Leavens, Valentin Wstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Wei |
| 2011 | FM | Using Debuggers to Understand Failed Verification Attempts. | Peter Mller, Joseph N. Ruskiewicz |
| 2011 | OOPSLA | Freedom before commitment: a lightweight type system for object initialisation. | Alexander J. Summers, Peter Mller |
| 2010 | ESOP | Deadlock-Free Channels and Locks. | K. Rustan M. Leino, Peter Mller, Jan Smans |
| 2010 | FASE | Proving Consistency and Completeness of Model Classes Using Theory Interpretation. | dm Darvas, Peter Mller |
| 2010 | FASE | Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups. | Hermann Lehner, Peter Mller |
| 2010 | GI | Informationsmanagement in der Milchviehhaltung - am Beispiel der Milchviehherde "Frankenforst" der Universitt Bonn. | Wolfgang Bscher, Ute Mller, Peter Mller, Eckhard Stamer |
| 2009 | ESOP | A Basis for Verifying Multi-threaded Programs. | K. Rustan M. Leino, Peter Mller |
| 2008 | ECOOP | A Unified Framework for Verification Techniques for Object Invariants. | Sophia Drossopoulou, Adrian Francalanza, Peter Mller, Alexander J. Summers |
| 2008 | ESOP | Verification of Equivalent-Results Methods. | K. Rustan M. Leino, Peter Mller |
| 2008 | FM | Checking Well-Formedness of Pure-Method Specifications. | Arsenii Rudich, dm Darvas, Peter Mller |
| 2007 | ECOOP | Generic Universe Types. | Werner Dietl, Sophia Drossopoulou, Peter Mller |
| 2007 | ICSE | Information Hiding and Visibility in Interface Specifications. | Gary T. Leavens, Peter Mller |
| 2007 | OOPSLA | Ownership transfer in universe types. | Peter Mller, Arsenii Rudich |
| 2007 | PDPTA | An Input Queueing Implementation for Low-Latency Speculative Optical Switches. | Raj Krishnamurthy, Peter Mller |
| 2007 | SEFM | Sound reasoning about unchecked exceptions. | Bart Jacobs, Peter Mller, Frank Piessens |
| 2006 | ESOP | A Verification Methodology for Model Fields. | K. Rustan M. Leino, Peter Mller |
| 2006 | EuroPLop | A Pattern Language for Overlay Networks in Peer-to-Peer Systems. | Dominik Grolimund, Peter Mller |
| 2006 | FM | Changing Programs Correctly: Refactoring with Specifications. | Fabian Bannwart, Peter Mller |
| 2005 | FM | Modular Verification of Static Class Invariants. | K. Rustan M. Leino, Peter Mller |
| 2005 | HOTI | Control Path Implementation for a Low-Latency Optical HPC Switch. | Cyriel Minkenberg, Franois Abel, Peter Mller, Raj Krishnamurthy, Mitchell Gusat, B. Roe Hemenway |
| 2004 | ECOOP | Object Invariants in Dynamic Contexts. | K. Rustan M. Leino, Peter Mller |
| 2000 | RECOMB | A combinatorial approach to protein docking with flexible side-chains. | Ernst Althaus, Oliver Kohlbacher, Hans-Peter Lenhof, Peter Mller |
| 1999 | ESOP | A Programming Logic for Sequential Java. | Arnd Poetzsch-Heffter, Peter Mller |
| 1997 | AISTATS | Markov chain Monte Carlo methods for decision analysis. | Concha Bielza, Peter Mller, David Ros Insua |
| 1997 | GI | Formal Specification Techniques for Object-Oriented Programs. | Peter Mller, Arnd Poetzsch-Heffter |
| 1987 | SIGIR | Probabilistic Search Term Weighting-Some Negative Results. | Norbert Fuhr, Peter Mller |