Formal Specification Techniques for Object-Oriented Programs. - Peter Müller 001; Arnd Poetzsch-Heffter (GI Jahrestagung, 1997)

Kapselung und Methodenbindung: Javas Designprobleme und ihre Korrektur. - Peter Müller 001; Arnd Poetzsch-Heffter (Java-Informations-Tage, 1998)

Logical foundations for typed object-oriented languages. - Arnd Poetzsch-Heffter; Peter Müller 001 (PROCOMET, 1998)

Formal Techniques for Java Programs. - Bart Jacobs 001; Gary T. Leavens; Peter Müller 001; Arnd Poetzsch-Heffter (ECOOP Workshops, 1999)

Alias Control Is Crucial for Modular Verification of Object-Oriented Programs. - Peter Müller 001; Arnd Poetzsch-Heffter (ECOOP Workshops, 1999)

A Programming Logic for Sequential Java. - Arnd Poetzsch-Heffter; Peter Müller 001 (ESOP, 1999)

Making Executable Interface Specifications More Expressive. - Peter Müller 001; Jörg Meyer 004; Arnd Poetzsch-Heffter (Java-Informations-Tage, 1999)

Formal Techniques for Java Programs. - Sophia Drossopoulou; Susan Eisenbach; Bart Jacobs 001; Gary T. Leavens; Peter Müller 001; Arnd Poetzsch-Heffter (ECOOP Workshops, 2000)

Modular Specification and Verification of Object-Oriented Programs - Peter Müller 001 (Springer, 2002)

Formal Techniques for Java-Like Programs. - Susan Eisenbach; Gary T. Leavens; Peter Müller 001; Arnd Poetzsch-Heffter; Erik Poll (ECOOP Workshops, 2003)

Modular specification of frame properties in JML. - Peter Müller 001; Arnd Poetzsch-Heffter; Gary T. Leavens (Concurr. Comput. Pract. Exp., 2003)

A Type System for Checking Applet Isolation in Java Card. - Werner Dietl; Peter Müller 001; Arnd Poetzsch-Heffter (CASSIS, 2004)

Object Invariants in Dynamic Contexts. - K. Rustan M. Leino; Peter Müller 001 (ECOOP, 2004)

Formal Techniques for Java-Like Programs (FTfJP). - Alessandro Coglio; Marieke Huisman; Joseph Kiniry; Peter Müller 001; Erik Poll (ECOOP Workshops, 2004)

Modular Verification of Static Class Invariants. - K. Rustan M. Leino; Peter Müller 001 (FM, 2005)

Reasoning about Object Structures Using Ownership. - Peter Müller 001 (VSTTE, 2005)

A Program Logic for Bytecode. - Fabian Bannwart; Peter Müller 001 (Bytecode@ETAPS, 2005)

Universes: Lightweight Ownership for JML. - Werner Dietl; Peter Müller 001 (J. Object Technol., 2005)

A Verification Methodology for Model Fields. - K. Rustan M. Leino; Peter Müller 001 (ESOP, 2006)

A Pattern Language for Overlay Networks in Peer-to-Peer Systems. - Dominik Grolimund; Peter Müller 001 (EuroPLoP, 2006)

Changing Programs Correctly: Refactoring with Specifications. - Fabian Bannwart; Peter Müller 001 (FM, 2006)

MOBIUS: Mobility, Ubiquity, Security. - Gilles Barthe; Lennart Beringer; Pierre Crégut; Benjamin Grégoire; Martin Hofmann 001; Peter Müller 001; Erik Poll; Germán Puebla; Ian Stark; Eric Vétillard (TGC, 2006)

Reasoning About Method Calls in Interface Specifications. - Ádám Darvas; Peter Müller 001 (J. Object Technol., 2006)

Modular invariants for layered object structures. - Peter Müller 001; Arnd Poetzsch-Heffter; Gary T. Leavens (Sci. Comput. Program., 2006)

07091 Executive Summary - Mobility, Ubiquity and Security. - Gilles Barthe; Heiko Mantel; Peter Müller 001; Andrew C. Myers; Andrei Sabelfeld (Mobility, Ubiquity and Security, 2007)

07091 Abstracts Collection - Mobility, Ubiquity and Security. - Gilles Barthe; Heiko Mantel; Peter Müller 001; Andrew C. Myers; Andrei Sabelfeld (Mobility, Ubiquity and Security, 2007)

Generic Universe Types. - Werner Dietl; Sophia Drossopoulou; Peter Müller 001 (ECOOP, 2007)

Universe Types for Topology and Encapsulation. - Dave Cunningham; Werner Dietl; Sophia Drossopoulou; Adrian Francalanza; Peter Müller 001; Alexander J. Summers (FMCO, 2007)

Information Hiding and Visibility in Interface Specifications. - Gary T. Leavens; Peter Müller 001 (ICSE, 2007)

Ownership transfer in universe types. - Peter Müller 001; Arsenii Rudich (OOPSLA, 2007)

Sound reasoning about unchecked exceptions. - Bart Jacobs 002; Peter Müller 001; Frank Piessens (SEFM, 2007)

Proof-transforming compilation of programs with abrupt termination. - Peter Müller 001; Martin Nordio (SAVCBS, 2007)

Formal Translation of Bytecode into BoogiePL. - Hermann Lehner; Peter Müller 001 (Bytecode@ETAPS, 2007)

Specification and verification challenges for sequential object-oriented programs. - Gary T. Leavens; K. Rustan M. Leino; Peter Müller 001 (Formal Aspects Comput., 2007)

A Unified Framework for Verification Techniques for Object Invariants. - Sophia Drossopoulou; Adrian Francalanza; Peter Müller 001; Alexander J. Summers (Types, Logics and Semantics for State, 2008)

Formal Techniques for Java-Like Programs. - Elvira Albert; Anindya Banerjee 001; Sophia Drossopoulou; Marieke Huisman; Atsushi Igarashi; Gary T. Leavens; Peter Müller 001; Tobias Wrigstad (ECOOP Workshops, 2008)

Aliasing, Confinement, and Ownership in Object-Oriented Programming. - Dave Clarke 001; Sophia Drossopoulou; Peter Müller 001; James Noble 001; Tobias Wrigstad (ECOOP Workshops, 2008)

Verification of Equivalent-Results Methods. - K. Rustan M. Leino; Peter Müller 001 (ESOP, 2008)

Checking Well-Formedness of Pure-Method Specifications. - Arsenii Rudich; Ádám Darvas; Peter Müller 001 (FM, 2008)

Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs. - K. Rustan M. Leino; Peter Müller 001 (LASER Summer School, 2008)

Proof-Transforming Compilation of Eiffel Programs. - Martin Nordio; Peter Müller 001; Bertrand Meyer 001 (TOOLS (46), 2008)

Flexible Immutability with Frozen Objects. - K. Rustan M. Leino; Peter Müller 001; Angela Wallenburg (VSTTE, 2008)

Faithful mapping of model classes to mathematical structures. - Ádám Darvas; Peter Müller 001 (IET Softw., 2008)

A Modular Verification Methodology for C# Delegates. - Peter Müller 001; Joseph N. Ruskiewicz (Rigorous Methods for Software Construction and Analysis, 2009)

A Basis for Verifying Multi-threaded Programs. - K. Rustan M. Leino; Peter Müller 001 (ESOP, 2009)

Verification of Concurrent Programs with Chalice. - K. Rustan M. Leino; Peter Müller 001; Jan Smans (FOSAD, 2009)

A Sound and Complete Program Logic for Eiffel. - Martin Nordio; Cristiano Calcagno; Peter Müller 001; Bertrand Meyer 001 (TOOLS (47), 2009)

Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods. - Alexander J. Summers; Sophia Drossopoulou; Peter Müller 001 (J. Object Technol., 2009)

Deadlock-Free Channels and Locks. - K. Rustan M. Leino; Peter Müller 001; Jan Smans (ESOP, 2010)

Proving Consistency and Completeness of Model Classes Using Theory Interpretation. - Ádám Darvas; Peter Müller 001 (FASE, 2010)

Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups. - Hermann Lehner; Peter Müller 001 (FASE, 2010)

Reasoning about Function Objects. - Martin Nordio; Cristiano Calcagno; Bertrand Meyer 001; Peter Müller 001; Julian Tschannen (TOOLS (48), 2010)

Tunable Static Inference for Generic Universe Types. - Werner Dietl; Michael D. Ernst; Peter Müller 001 (ECOOP, 2011)

Fractional permissions without the fractions. - Stefan Heule; K. Rustan M. Leino; Peter Müller 001; Alexander J. Summers (FTfJP@ECOOP, 2011)

The 1st Verified Software Competition: Experience Report. - Vladimir Klebanov; Peter Müller 001; Natarajan Shankar; Gary T. Leavens; Valentin Wüstholz; Eyad Alkassar; Rob Arthan; Derek Bronish; Rod Chapman; Ernie Cohen; Mark A. Hillebrand; Bart Jacobs 002; et al. (FM, 2011)

Using Debuggers to Understand Failed Verification Attempts. - Peter Müller 001; Joseph N. Ruskiewicz (FM, 2011)

Freedom before commitment: a lightweight type system for object initialisation. - Alexander J. Summers; Peter Müller 001 (OOPSLA, 2011)

Specification and verification: the Spec# experience. - Mike Barnett 001; Manuel Fähndrich; K. Rustan M. Leino; Peter Müller 001; Wolfram Schulte; Herman Venter (Commun. ACM, 2011)

Separating ownership topology and encapsulation with generic universe types. - Werner Dietl; Sophia Drossopoulou; Peter Müller 001 (ACM Trans. Program. Lang. Syst., 2011)

Formal Methods-Based Tools for Race, Deadlock, and Other Errors. - Peter Müller 001 (Encyclopedia of Parallel Computing, 2011)

Collaborative Verification and Testing with Explicit Assumptions. - Maria Christakis; Peter Müller 001; Valentin Wüstholz (FM, 2012)

Automatic Inference of Access Permissions. - Pietro Ferrara 001; Peter Müller 001 (VMCAI, 2012)

Comparing Verification Condition Generation with Symbolic Execution: An Experience Report. - Ioannis T. Kassios; Peter Müller 001; Malte Schwerhoff (VSTTE, 2012)

Behavioral interface specification languages. - John Hatcliff; Gary T. Leavens; K. Rustan M. Leino; Peter Müller 001; Matthew J. Parkinson (ACM Comput. Surv., 2012)

Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions. - Stefan Heule; Ioannis T. Kassios; Peter Müller 001; Alexander J. Summers (ECOOP, 2013)

Customizing the visualization and interaction for embedded domain-specific languages in a structured editor. - Dimitar Asenov; Peter Müller 001 (VL/HCC, 2013)

Abstract Read Permissions: Fractional Permissions without the Fractions. - Stefan Heule; K. Rustan M. Leino; Peter Müller 001; Alexander J. Summers (VMCAI, 2013)

Object Ownership in Program Verification. - Werner Dietl; Peter Müller 001 (Aliasing in Object-Oriented Programming, 2013)

Constraint Semantics for Abstract Read Permissions. - John Tang Boyland; Peter Müller 001; Malte Schwerhoff; Alexander J. Summers (FTfJP@ECOOP, 2014)

Static analysis for independent app developers. - Lucas Brutschy; Pietro Ferrara 001; Peter Müller 001 (OOPSLA, 2014)

TouchGuru: Integrating Static Analysis with a Mobile Development Environment. - Lucas Brutschy; Pietro Ferrara 001; Peter Müller 001 (MobileDeLi, 2014)

Dynamic Test Generation with Static Fields and Initializers. - Maria Christakis; Patrick Emmisberger; Peter Müller 001 (RV, 2014)

Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations. - Maria Christakis; Peter Müller 001; Valentin Wüstholz (SEFM, 2014)

Envision: A fast and flexible visual code editor with fluid interactions (Overview). - Dimitar Asenov; Peter Müller 001 (VL/HCC, 2014)

Modular Verification of Finite Blocking in Non-terminating Programs. - Pontus Boström; Peter Müller 001 (ECOOP, 2015)

Building automatic program verifiers. - Peter Müller 001 (PLMW@POPL, 2015)

An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer. - Maria Christakis; Peter Müller 001; Valentin Wüstholz (VMCAI, 2015)

Automatic Inference of Heap Properties Exploiting Value Domains. - Pietro Ferrara 001; Peter Müller 001; Milos Novácek (VMCAI, 2015)

Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. - Peter Müller 001; Malte Schwerhoff; Alexander J. Summers (CAV (1), 2016)

The Effect of Richer Visualizations on Code Comprehension. - Dimitar Asenov; Otmar Hilliges; Peter Müller 001 (CHI, 2016)

Actor Services - Modular Verification of Message Passing Programs. - Alexander J. Summers; Peter Müller 001 (ESOP, 2016)

Guiding dynamic symbolic execution toward unverified program executions. - Maria Christakis; Peter Müller 001; Valentin Wüstholz (ICSE, 2016)

The IDE as a scriptable information system. - Dimitar Asenov; Peter Müller 001; Lukas Vogel 002 (ASE, 2016)

Integrated Environment for Diagnosing Verification Errors. - Maria Christakis; K. Rustan M. Leino; Peter Müller 001; Valentin Wüstholz (TACAS, 2016)

Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets). - Cédric Favre; Hagen Völzer; Peter Müller 001 (TACAS, 2016)

Viper: A Verification Infrastructure for Permission-Based Reasoning. - Peter Müller 001; Malte Schwerhoff; Alexander J. Summers (VMCAI, 2016)

The IDE as a Scriptable Information System (extended version). - Dimitar Asenov; Peter Müller 001; Lukas Vogel 002 (CoRR, 2016)

Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201). - Julian Dolby; Orna Grumberg; Peter Müller 001; Omer Tripp (Dagstuhl Reports, 2016)

Precise Version Control of Trees with Line-Based Version Control Systems. - Dimitar Asenov; Balz Guenat; Peter Müller 001; Martin Otth (FASE, 2017)

A general framework for dynamic stub injection. - Maria Christakis; Patrick Emmisberger; Patrice Godefroid; Peter Müller 001 (ICSE, 2017)

Serializability for eventual consistency: criterion, analysis, and applications. - Lucas Brutschy; Dimitar Dimitrov 004; Peter Müller 001; Martin T. Vechev (POPL, 2017)

Viper: A Verification Infrastructure for Permission-Based Reasoning. - Peter Müller 001; Malte Schwerhoff; Alexander J. Summers (Dependable Software Systems Engineering, 2017)

The Binomial Heap Verification Challenge in Viper. - Peter Müller 001 (Principled Software Development, 2018)

Permission Inference for Array Programs. - Jérôme Dohrau; Alexander J. Summers; Caterina Urban; Severin Münger; Peter Müller 001 (CAV (2), 2018)

Nagini: A Static Verifier for Python. - Marco Eilers; Peter Müller 001 (CAV (1), 2018)

MaxSMT-Based Type Inference for Python 3. - Mostafa Hassan; Caterina Urban; Marco Eilers; Peter Müller 001 (CAV (2), 2018)

An Abstract Interpretation Framework for Input Data Usage. - Caterina Urban; Peter Müller 001 (ESOP, 2018)

Automatically testing implementations of numerical abstract domains. - Alexandra Bugariu; Valentin Wüstholz; Maria Christakis; Peter Müller 001 (ASE, 2018)

Static serializability analysis for causal consistency. - Lucas Brutschy; Dimitar Dimitrov 004; Peter Müller 001; Martin T. Vechev (PLDI, 2018)

Abstract Interpretation of CTL Properties. - Caterina Urban; Samuel Ueltschi; Peter Müller 001 (SAS, 2018)

Automating Deductive Verification for Weak-Memory Programs. - Alexander J. Summers; Peter Müller 001 (TACAS (1), 2018)

Specification Mining for Smart Contracts with Automatic Abstraction Tuning. - Florentin Guth; Valentin Wüstholz; Maria Christakis; Peter Müller 001 (CoRR, 2018)

The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. - Nils Becker; Peter Müller 001; Alexander J. Summers (TACAS (1), 2019)

Leveraging rust types for modular specification and verification. - Vytautas Astrauskas; Peter Müller 001; Federico Poli 001; Alexander J. Summers (Proc. ACM Program. Lang., 2019)

Modular verification of heap reachability properties in separation logic. - Arshavir Ter-Gabrielyan; Alexander J. Summers; Peter Müller 001 (Proc. ACM Program. Lang., 2019)

Automatically testing string solvers. - Alexandra Bugariu; Peter Müller 001 (ICSE, 2020)

VerifyThis 2019: A Program Verification Competition (Extended Report). - Claire Dross; Carlo A. Furia; Marieke Huisman; Rosemary Monahan; Peter Müller 001 (CoRR, 2020)

Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper). - Felix A. Wolf; Malte Schwerhoff; Peter Müller 001 (CoRR, 2020)

Igloo: soundly linking compositional refinement and separation logic for distributed system verification. - Christoph Sprenger 001; Tobias Klenze; Marco Eilers; Felix A. Wolf; Peter Müller 001; Martin Clochard; David A. Basin (Proc. ACM Program. Lang., 2020)

How do programmers use unsafe rust? - Vytautas Astrauskas; Christoph Matheja; Federico Poli 001; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2020)

Automating deductive verification for weak-memory programs (extended version). - Alexander J. Summers; Peter Müller 001 (Int. J. Softw. Tools Technol. Transf., 2020)

Modular Product Programs. - Marco Eilers; Peter Müller 001; Samuel Hitz (ACM Trans. Program. Lang. Syst., 2020)

The First Fifteen Years of the Verified Software Project. - Peter Müller 001; Natarajan Shankar (Theories of Programming, 2021)

Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. - Marco Eilers; Severin Meier; Peter Müller 001 (CAV (1), 2021)

Formally Validating a Practical Verification Condition Generator. - Gaurav Parthasarathy; Peter Müller 001; Alexander J. Summers (CAV (2), 2021)

Gobra: Modular Specification and Verification of Go Programs. - Felix A. Wolf; Linard Arquint; Martin Clochard; Wytse Oortwijn; João Carlos Pereira; Peter Müller 001 (CAV (1), 2021)

Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers. - Alexandra Bugariu; Arshavir Ter-Gabrielyan; Peter Müller 001 (FM, 2021)

Modular Verification of Collaborating Smart Contracts. - Christian Bräm; Marco Eilers; Peter Müller 001; Robin Sierra; Alexander J. Summers (CoRR, 2021)

Gobra: Modular Specification and Verification of Go Programs (extended version). - Felix A. Wolf; Linard Arquint; Martin Clochard; Wytse Oortwijn; João Carlos Pereira; Peter Müller 001 (CoRR, 2021)

Formally Validating a Practical Verification Condition Generator (extended version). - Gaurav Parthasarathy; Peter Müller 001; Alexander J. Summers (CoRR, 2021)

Flexible Refinement Proofs in Separation Logic. - Aurel Bílý; Christoph Matheja; Peter Müller 001 (CoRR, 2021)

Rich specifications for Ethereum smart contract verification. - Christian Bräm; Marco Eilers; Peter Müller 001; Robin Sierra; Alexander J. Summers (Proc. ACM Program. Lang., 2021)

Modular specification and verification of closures in Rust. - Fabian Wolff; Aurel Bílý; Christoph Matheja; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2021)

VerifyThis 2019: a program verification competition. - Claire Dross; Carlo A. Furia; Marieke Huisman; Rosemary Monahan; Peter Müller 001 (Int. J. Softw. Tools Technol. Transf., 2021)

Introduction to the Special Section on ESOP 2020. - Peter Müller 001 (ACM Trans. Program. Lang. Syst., 2021)

Sound Automation of Magic Wands. - Thibault Dardinier; Gaurav Parthasarathy; Noé Weeks; Peter Müller 001; Alexander J. Summers (CAV (2), 2022)

The Prusti Project: Formal Verification for Rust. - Vytautas Astrauskas; Aurel Bílý; Jonás Fiala; Zachary Grannan; Christoph Matheja; Peter Müller 001; Federico Poli 001; Alexander J. Summers (NFM, 2022)

Sound Automation of Magic Wands (extended version). - Thibault Dardinier; Gaurav Parthasarathy; Noé Weeks; Alexander J. Summers; Peter Müller 001 (CoRR, 2022)

Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version). - Thibault Dardinier; Gaurav Parthasarathy; Peter Müller 001 (CoRR, 2022)

Compositional Reasoning for Side-effectful Iterators and Iterator Adapters. - Aurel Bílý; Jonas Hansen; Peter Müller 001; Alexander J. Summers (CoRR, 2022)

Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version). - Linard Arquint; Felix A. Wolf; Joseph Lallemand; Ralf Sasse; Christoph Sprenger 001; Sven N. Wiesner; David A. Basin; Peter Müller 001 (CoRR, 2022)

Fractional resources in unbounded separation logic. - Thibault Dardinier; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2022)

The Complete Guide to SCION - From Design Principles to Formal Verification - Laurent Chuat; Markus Legner; David A. Basin; David Hausheer; Samuel Hitz; Peter Müller 001; Adrian Perrig (Springer, 2022)

Sound Verification of Security Protocols: From Design to Interoperable Implementations. - Linard Arquint; Felix A. Wolf; Joseph Lallemand; Ralf Sasse; Christoph Sprenger 001; Sven N. Wiesner; David A. Basin; Peter Müller 001 (Zenodo, 2022)

Sound Verification of Security Protocols: From Design to Interoperable Implementations. - Linard Arquint; Felix A. Wolf; Joseph Lallemand; Ralf Sasse; Christoph Sprenger 001; Sven N. Wiesner; David A. Basin; Peter Müller 001 (Zenodo, 2022)

Concise outlines for a complex logic: a proof outline checker for TaDA. - Felix A. Wolf; Malte Schwerhoff; Peter Müller 001 (Formal Methods Syst. Des., 2022)

A Generic Methodology for the Modular Verification of Security Protocol Implementations. - Linard Arquint; Malte Schwerhoff; Vaibhav Mehta; Peter Müller 001 (CCS, 2023)

Sound Verification of Security Protocols: From Design to Interoperable Implementations. - Linard Arquint; Felix A. Wolf; Joseph Lallemand; Ralf Sasse; Christoph Sprenger 001; Sven N. Wiesner; David A. Basin; Peter Müller 001 (SP, 2023)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). - Thibault Dardinier; Peter Müller 001 (CoRR, 2023)

Refinement Proofs in Rust Using Ghost Locks. - Aurel Bílý; João C. Pereira; Jan Schär; Peter Müller 001 (CoRR, 2023)

Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281). - Arie Gurfinkel; Isabella Mastroeni; Antoine Miné; Peter Müller 001; Anna Becchi (Dagstuhl Reports, 2023)

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. - Marco Eilers; Thibault Dardinier; Peter Müller 001 (Proc. ACM Program. Lang., 2023)

Leveraging Rust Types for Program Synthesis. - Jonás Fiala; Shachar Itzhaky; Peter Müller 001; Nadia Polikarpova; Ilya Sergey (Proc. ACM Program. Lang., 2023)

Verification-Preserving Inlining in Automatic Separation Logic Verifiers. - Thibault Dardinier; Gaurav Parthasarathy; Peter Müller 001 (Proc. ACM Program. Lang., 2023)

Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (Extended Version). - Alexandra Bugariu; Arshavir Ter-Gabrielyan; Peter Müller 001 (Formal Aspects Comput., 2023)

Verification Algorithms for Automated Separation Logic Verifiers. - Marco Eilers; Malte Schwerhoff; Peter Müller 001 (CAV (1), 2024)

Verifiable Security Policies for Distributed Systems. - Felix A. Wolf; Peter Müller 001 (CCS, 2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version). - Gaurav Parthasarathy; Thibault Dardinier; Benjamin Bonneau; Peter Müller 001; Alexander J. Summers (CoRR, 2024)

Protocols to Code: Formal Verification of a Next-Generation Internet Router. - João C. Pereira; Tobias Klenze; Sofia Giampietro; Markus Limbeck; Dionysios Spiliopoulos; Felix A. Wolf; Marco Eilers; Christoph Sprenger 001; David A. Basin; Peter Müller 001; Adrian Perrig (CoRR, 2024)

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities. - Federico Poli 001; Xavier Denis; Peter Müller 001; Alexander J. Summers (CoRR, 2024)

Formal Foundations for Translational Separation Logic Verifiers (extended version). - Thibault Dardinier; Michael Sammler; Gaurav Parthasarathy; Alexander J. Summers; Peter Müller 001 (CoRR, 2024)

Hypra: A Deductive Program Verifier for Hyper Hoare Logic. - Thibault Dardinier; Anqi Li; Peter Müller 001 (Proc. ACM Program. Lang., 2024)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. - Thibault Dardinier; Peter Müller 001 (Proc. ACM Program. Lang., 2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. - Gaurav Parthasarathy; Thibault Dardinier; Benjamin Bonneau; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2024)

Fifteen Years of Viper. - Marco Eilers; Malte Schwerhoff; Alexander J. Summers; Peter Müller 001 (CAV (1), 2025)

Accelerating Automated Program Verifiers by Automatic Proof Localization. - Kiran Gopinathan; Dionysios Spiliopoulos; Vikram Goyal; Peter Müller 001; Markus Püschel; Ilya Sergey (CAV (3), 2025)

On Formal Methods Thinking in Computer Science Education. - Brijesh Dongol; Catherine Dubois; Stefan Hallerstede; Eric C. R. Hehner; Carroll Morgan; Peter Müller 001; Leila Ribeiro 001; Alexandra Silva 001; Graeme Smith 001; Erik P. de Vink (Formal Aspects Comput., 2025)

Formal Foundations for Translational Separation Logic Verifiers. - Thibault Dardinier; Michael Sammler; Gaurav Parthasarathy; Alexander J. Summers; Peter Müller 001 (Proc. ACM Program. Lang., 2025)

Destabilizing Iris. - Simon Spies; Niklas Mück; Haoyi Zeng; Michael Sammler; Andrea Lattuada 001; Peter Müller 001; Derek Dreyer (Proc. ACM Program. Lang., 2025)

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees. - Zachary Grannan; Aurel Bílý; Jonás Fiala; Jasper Geer; Markus de Medeiros; Peter Müller 001; Alexander J. Summers (CoRR, 2025)

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version). - Linard Arquint; Samarth Kishor; Jason R. Koenig; Joey Dodds; Daniel Kroening; Peter Müller 001 (CoRR, 2025)