Peter Müller

ORCID

Publication Activity (10 Years)

Years Active: 1997-2024
Publications (10 Years): 80

Top Venues

CoRR

Proc. ACM Program. Lang.

CAV (1)

CAV (2)

Publications

João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David A. Basin, Peter Müller, Adrian Perrig
Protocols to Code: Formal Verification of a Next-Generation Internet Router. CoRR (2024)
Marco Eilers, Malte Schwerhoff, Peter Müller
Verification Algorithms for Automated Separation Logic Verifiers. CAV (1) (2024)
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version). CoRR (2024)
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Federico Poli, Xavier Denis, Peter Müller, Alexander J. Summers
Reasoning about Interior Mutability in Rust using Library-Defined Capabilities. CoRR (2024)
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
Formal Foundations for Translational Separation Logic Verifiers (extended version). CoRR (2024)
Marco Eilers, Malte Schwerhoff, Peter Müller
Verification Algorithms for Automated Separation Logic Verifiers. CoRR (2024)
Thibault Dardinier, Peter Müller
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Aurel Bílý, João C. Pereira, Jan Schär, Peter Müller
Refinement Proofs in Rust Using Ghost Locks. CoRR (2023)
Jonás Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey
Leveraging Rust Types for Program Synthesis. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Thibault Dardinier, Peter Müller
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). CoRR (2023)
Marco Eilers, Thibault Dardinier, Peter Müller
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, Anna Becchi
Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281). Dagstuhl Reports 13 (7) (2023)
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
Verification-Preserving Inlining in Automatic Separation Logic Verifiers. Proc. ACM Program. Lang. 7 (OOPSLA1) (2023)
Linard Arquint, Malte Schwerhoff, Vaibhav Mehta, Peter Müller
A Generic Methodology for the Modular Verification of Security Protocol Implementations. CCS (2023)
Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David A. Basin, Peter Müller
Sound Verification of Security Protocols: From Design to Interoperable Implementations. SP (2023)
Alexandra Bugariu, Arshavir Ter-Gabrielyan, Peter Müller
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (Extended Version). Formal Aspects Comput. 35 (2) (2023)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers
Sound Automation of Magic Wands. CAV (2) (2022)
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version). CoRR (2022)
Thibault Dardinier, Peter Müller, Alexander J. Summers
Fractional resources in unbounded separation logic. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Felix A. Wolf, Malte Schwerhoff, Peter Müller
Concise outlines for a complex logic: a proof outline checker for TaDA. Formal Methods Syst. Des. 61 (1) (2022)
Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers
The Prusti Project: Formal Verification for Rust. NFM (2022)
Marco Eilers, Thibault Dardinier, Peter Müller
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. CoRR (2022)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Alexander J. Summers, Peter Müller
Sound Automation of Magic Wands (extended version). CoRR (2022)
Linard Arquint, Malte Schwerhoff, Vaibhav Mehta, Peter Müller
A Generic Methodology for the Modular Verification of Security Protocol Implementations. CoRR (2022)
Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David A. Basin, Peter Müller
Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version). CoRR (2022)
Aurel Bílý, Jonas Hansen, Peter Müller, Alexander J. Summers
Compositional Reasoning for Side-effectful Iterators and Iterator Adapters. CoRR (2022)
Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, Alexander J. Summers
Rich specifications for Ethereum smart contract verification. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Felix A. Wolf, Malte Schwerhoff, Peter Müller
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA. FM (2021)
Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, Peter Müller
Gobra: Modular Specification and Verification of Go Programs (extended version). CoRR (2021)
Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, Alexander J. Summers
Modular specification and verification of closures in Rust. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, Alexander J. Summers
Modular Verification of Collaborating Smart Contracts. CoRR (2021)
Claire Dross, Carlo A. Furia, Marieke Huisman, Rosemary Monahan, Peter Müller
VerifyThis 2019: a program verification competition. Int. J. Softw. Tools Technol. Transf. 23 (6) (2021)
Marco Eilers, Severin Meier, Peter Müller
Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. CAV (1) (2021)
Gaurav Parthasarathy, Peter Müller, Alexander J. Summers
Formally Validating a Practical Verification Condition Generator. CAV (2) (2021)
Peter Müller
Introduction to the Special Section on ESOP 2020. ACM Trans. Program. Lang. Syst. 43 (4) (2021)
Alexandra Bugariu, Arshavir Ter-Gabrielyan, Peter Müller
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers. CoRR (2021)
Aurel Bílý, Christoph Matheja, Peter Müller
Flexible Refinement Proofs in Separation Logic. CoRR (2021)
Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, Peter Müller
Gobra: Modular Specification and Verification of Go Programs. CAV (1) (2021)
Alexandra Bugariu, Arshavir Ter-Gabrielyan, Peter Müller
Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers. FM (2021)
Gaurav Parthasarathy, Peter Müller, Alexander J. Summers
Formally Validating a Practical Verification Condition Generator (extended version). CoRR (2021)
Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, David A. Basin
Igloo: soundly linking compositional refinement and separation logic for distributed system verification. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Claire Dross, Carlo A. Furia, Marieke Huisman, Rosemary Monahan, Peter Müller
VerifyThis 2019: A Program Verification Competition (Extended Report). CoRR (2020)
Marco Eilers, Peter Müller, Samuel Hitz
Modular Product Programs. ACM Trans. Program. Lang. Syst. 42 (1) (2020)
Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers
How do programmers use unsafe rust? Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Felix A. Wolf, Malte Schwerhoff, Peter Müller
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper). CoRR (2020)
Alexander J. Summers, Peter Müller
Automating deductive verification for weak-memory programs (extended version). Int. J. Softw. Tools Technol. Transf. 22 (6) (2020)
Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, David A. Basin
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification. CoRR (2020)
Alexandra Bugariu, Peter Müller
Automatically testing string solvers. ICSE (2020)
Vytautas Astrauskas, Peter Müller, Federico Poli, Alexander J. Summers
Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Arshavir Ter-Gabrielyan, Alexander J. Summers, Peter Müller
Modular verification of heap reachability properties in separation logic. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Arshavir Ter-Gabrielyan, Alexander J. Summers, Peter Müller
Modular Verification of Heap Reachability Properties in Separation Logic. CoRR (2019)
Nils Becker, Peter Müller, Alexander J. Summers
The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. TACAS (1) (2019)
Marco Eilers, Peter Müller, Samuel Hitz
Modular Product Programs. ESOP (2018)
Lucas Brutschy, Dimitar K. Dimitrov, Peter Müller, Martin T. Vechev
Static serializability analysis for causal consistency. PLDI (2018)
Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller
Permission Inference for Array Programs. CoRR (2018)
Caterina Urban, Peter Müller
An Abstract Interpretation Framework for Input Data Usage. ESOP (2018)
Caterina Urban, Samuel Ueltschi, Peter Müller
Abstract Interpretation of CTL Properties. SAS (2018)
Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller
Permission Inference for Array Programs. CAV (2) (2018)
Alexander J. Summers, Peter Müller
Automating Deductive Verification for Weak-Memory Programs. TACAS (1) (2018)
Peter Müller
The Binomial Heap Verification Challenge in Viper. Principled Software Development (2018)
Alexandra Bugariu, Valentin Wüstholz, Maria Christakis, Peter Müller
Automatically testing implementations of numerical abstract domains. ASE (2018)
Florentin Guth, Valentin Wüstholz, Maria Christakis, Peter Müller
Specification Mining for Smart Contracts with Automatic Abstraction Tuning. CoRR (2018)
Marco Eilers, Peter Müller
Nagini: A Static Verifier for Python. CAV (1) (2018)
Mostafa Hassan, Caterina Urban, Marco Eilers, Peter Müller
MaxSMT-Based Type Inference for Python 3. CAV (2) (2018)
Lucas Brutschy, Dimitar K. Dimitrov, Peter Müller, Martin T. Vechev
Serializability for eventual consistency: criterion, analysis, and applications. POPL (2017)
Alexander J. Summers, Peter Müller
Automating Deductive Verification for Weak-Memory Programs. CoRR (2017)
Dimitar Asenov, Balz Guenat, Peter Müller, Martin Otth
Precise Version Control of Trees with Line-Based Version Control Systems. FASE (2017)
Maria Christakis, Patrick Emmisberger, Patrice Godefroid, Peter Müller
A general framework for dynamic stub injection. ICSE (2017)
Peter Müller, Malte Schwerhoff, Alexander J. Summers
Viper: A Verification Infrastructure for Permission-Based Reasoning. VMCAI (2016)
Cédric Favre, Hagen Völzer, Peter Müller
Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets). TACAS (2016)
Peter Müller, Malte Schwerhoff, Alexander J. Summers
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution. CoRR (2016)
Dimitar Asenov, Peter Müller, Lukas Vogel
The IDE as a scriptable information system. ASE (2016)
Dimitar Asenov, Peter Müller, Lukas Vogel
The IDE as a Scriptable Information System (extended version). CoRR (2016)
Maria Christakis, K. Rustan M. Leino, Peter Müller, Valentin Wüstholz
Integrated Environment for Diagnosing Verification Errors. TACAS (2016)
Dimitar Asenov, Otmar Hilliges, Peter Müller
The Effect of Richer Visualizations on Code Comprehension. CHI (2016)
Alexander J. Summers, Peter Müller
Actor Services - Modular Verification of Message Passing Programs. ESOP (2016)
Julian Dolby, Orna Grumberg, Peter Müller, Omer Tripp
Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201). Dagstuhl Reports 6 (5) (2016)
Peter Müller, Malte Schwerhoff, Alexander J. Summers
Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. CAV (1) (2016)
Maria Christakis, Peter Müller, Valentin Wüstholz
Guiding dynamic symbolic execution toward unverified program executions. ICSE (2016)
Maria Christakis, Peter Müller, Valentin Wüstholz
An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer. VMCAI (2015)
Peter Müller
Building automatic program verifiers. PLMW@POPL (2015)
Pietro Ferrara, Peter Müller, Milos Novácek
Automatic Inference of Heap Properties Exploiting Value Domains. VMCAI (2015)
Pontus Boström, Peter Müller
Modular Verification of Finite Blocking in Non-terminating Programs. ECOOP (2015)
Lucas Brutschy, Pietro Ferrara, Peter Müller
TouchGuru: Integrating Static Analysis with a Mobile Development Environment. MobileDeLi (2014)
Dimitar Asenov, Peter Müller
Envision: A fast and flexible visual code editor with fluid interactions (Overview). VL/HCC (2014)
Maria Christakis, Peter Müller, Valentin Wüstholz
Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations. SEFM (2014)
Lucas Brutschy, Pietro Ferrara, Peter Müller
Static analysis for independent app developers. OOPSLA (2014)
Maria Christakis, Patrick Emmisberger, Peter Müller
Dynamic Test Generation with Static Fields and Initializers. RV (2014)
John Tang Boyland, Peter Müller, Malte Schwerhoff, Alexander J. Summers
Constraint Semantics for Abstract Read Permissions. FTfJP@ECOOP (2014)
Stefan Heule, Ioannis T. Kassios, Peter Müller, Alexander J. Summers
Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions. ECOOP (2013)
Dimitar Asenov, Peter Müller
Customizing the visualization and interaction for embedded domain-specific languages in a structured editor. VL/HCC (2013)
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
Abstract Read Permissions: Fractional Permissions without the Fractions. VMCAI (2013)
Pietro Ferrara, Peter Müller
Automatic Inference of Access Permissions. VMCAI (2012)
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson
Behavioral interface specification languages. ACM Comput. Surv. 44 (3) (2012)
Maria Christakis, Peter Müller, Valentin Wüstholz
Collaborative Verification and Testing with Explicit Assumptions. FM (2012)
Ioannis T. Kassios, Peter Müller, Malte Schwerhoff
Comparing Verification Condition Generation with Symbolic Execution: An Experience Report. VSTTE (2012)
Alexander J. Summers, Peter Müller
Freedom before commitment: a lightweight type system for object initialisation. OOPSLA (2011)
Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, Herman Venter
Specification and verification: the Spec# experience. Commun. ACM 54 (6) (2011)
Werner Dietl, Sophia Drossopoulou, Peter Müller
Separating ownership topology and encapsulation with generic universe types. ACM Trans. Program. Lang. Syst. 33 (6) (2011)

Peter Müller.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Peter Müller