Peter Müller

Orcid: 0000-0001-7001-2566

Affiliations:
  • ETH Zürich, Department of Computer Science, Switzerland
  • Microsoft Research, Redmond, USA
  • University of Hagen, Germany


According to our database1, Peter Müller authored at least 154 papers between 1997 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language.
Proc. ACM Program. Lang., 2024

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties.
Proc. ACM Program. Lang., 2024

Hypra: A Deductive Program Verifier for Hyper Hoare Logic.
Proc. ACM Program. Lang., 2024

Formal Foundations for Translational Separation Logic Verifiers (extended version).
CoRR, 2024

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities.
CoRR, 2024

Protocols to Code: Formal Verification of a Next-Generation Internet Router.
CoRR, 2024

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version).
CoRR, 2024

Verifiable Security Policies for Distributed Systems.
Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 2024

Verification Algorithms for Automated Separation Logic Verifiers.
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (Extended Version).
Formal Aspects Comput., June, 2023

Verification-Preserving Inlining in Automatic Separation Logic Verifiers.
Proc. ACM Program. Lang., April, 2023

Leveraging Rust Types for Program Synthesis.
Proc. ACM Program. Lang., 2023

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity.
Proc. ACM Program. Lang., 2023

Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281).
Dagstuhl Reports, 2023

Refinement Proofs in Rust Using Ghost Locks.
CoRR, 2023

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version).
CoRR, 2023

Sound Verification of Security Protocols: From Design to Interoperable Implementations.
Proceedings of the 44th IEEE Symposium on Security and Privacy, 2023

A Generic Methodology for the Modular Verification of Security Protocol Implementations.
Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

2022
Concise outlines for a complex logic: a proof outline checker for TaDA.
Formal Methods Syst. Des., August, 2022

Sound Verification of Security Protocols: From Design to Interoperable Implementations.
Dataset, August, 2022

Sound Verification of Security Protocols: From Design to Interoperable Implementations.
Dataset, August, 2022

The Complete Guide to SCION - From Design Principles to Formal Verification
Information Security and Cryptography, Springer, ISBN: 978-3-031-05288-0, 2022

Fractional resources in unbounded separation logic.
Proc. ACM Program. Lang., 2022

Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version).
CoRR, 2022

Compositional Reasoning for Side-effectful Iterators and Iterator Adapters.
CoRR, 2022

Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version).
CoRR, 2022

Sound Automation of Magic Wands (extended version).
CoRR, 2022

The Prusti Project: Formal Verification for Rust.
Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

Sound Automation of Magic Wands.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2021
Introduction to the Special Section on ESOP 2020.
ACM Trans. Program. Lang. Syst., 2021

VerifyThis 2019: a program verification competition.
Int. J. Softw. Tools Technol. Transf., 2021

Modular specification and verification of closures in Rust.
Proc. ACM Program. Lang., 2021

Rich specifications for Ethereum smart contract verification.
Proc. ACM Program. Lang., 2021

Flexible Refinement Proofs in Separation Logic.
CoRR, 2021

Formally Validating a Practical Verification Condition Generator (extended version).
CoRR, 2021

Gobra: Modular Specification and Verification of Go Programs (extended version).
CoRR, 2021

Modular Verification of Collaborating Smart Contracts.
CoRR, 2021

Identifying Overly Restrictive Matching Patterns in SMT-Based Program Verifiers.
Proceedings of the Formal Methods - 24th International Symposium, 2021

Gobra: Modular Specification and Verification of Go Programs.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Formally Validating a Practical Verification Condition Generator.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

The First Fifteen Years of the Verified Software Project.
Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

2020
Modular Product Programs.
ACM Trans. Program. Lang. Syst., 2020

Automating deductive verification for weak-memory programs (extended version).
Int. J. Softw. Tools Technol. Transf., 2020

How do programmers use unsafe rust?
Proc. ACM Program. Lang., 2020

Igloo: soundly linking compositional refinement and separation logic for distributed system verification.
Proc. ACM Program. Lang., 2020

Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper).
CoRR, 2020

VerifyThis 2019: A Program Verification Competition (Extended Report).
CoRR, 2020

Automatically testing string solvers.
Proceedings of the ICSE '20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June, 2020

2019
Modular verification of heap reachability properties in separation logic.
Proc. ACM Program. Lang., 2019

Leveraging rust types for modular specification and verification.
Proc. ACM Program. Lang., 2019

The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

2018
Specification Mining for Smart Contracts with Automatic Abstraction Tuning.
CoRR, 2018

Automating Deductive Verification for Weak-Memory Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Abstract Interpretation of CTL Properties.
Proceedings of the Static Analysis - 25th International Symposium, 2018

Static serializability analysis for causal consistency.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Automatically testing implementations of numerical abstract domains.
Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

An Abstract Interpretation Framework for Input Data Usage.
Proceedings of the Programming Languages and Systems, 2018

MaxSMT-Based Type Inference for Python 3.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Nagini: A Static Verifier for Python.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Permission Inference for Array Programs.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

The Binomial Heap Verification Challenge in Viper.
Proceedings of the Principled Software Development, 2018

2017
Viper: A Verification Infrastructure for Permission-Based Reasoning.
Proceedings of the Dependable Software Systems Engineering, 2017

Serializability for eventual consistency: criterion, analysis, and applications.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

A general framework for dynamic stub injection.
Proceedings of the 39th International Conference on Software Engineering, 2017

Precise Version Control of Trees with Line-Based Version Control Systems.
Proceedings of the Fundamental Approaches to Software Engineering, 2017

2016
Synergies among Testing, Verification, and Repair for Concurrent Programs (Dagstuhl Seminar 16201).
Dagstuhl Reports, 2016

The IDE as a Scriptable Information System (extended version).
CoRR, 2016

Viper: A Verification Infrastructure for Permission-Based Reasoning.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Diagnostic Information for Control-Flow Analysis of Workflow Graphs (a.k.a. Free-Choice Workflow Nets).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Integrated Environment for Diagnosing Verification Errors.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

The IDE as a scriptable information system.
Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

Guiding dynamic symbolic execution toward unverified program executions.
Proceedings of the 38th International Conference on Software Engineering, 2016

Actor Services - Modular Verification of Message Passing Programs.
Proceedings of the Programming Languages and Systems, 2016

The Effect of Richer Visualizations on Code Comprehension.
Proceedings of the 2016 CHI Conference on Human Factors in Computing Systems, 2016

Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015
Automatic Inference of Heap Properties Exploiting Value Domains.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

Building automatic program verifiers.
Proceedings of the Programming Languages Mentoring Workshop, 2015

Modular Verification of Finite Blocking in Non-terminating Programs.
Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014
Envision: A fast and flexible visual code editor with fluid interactions (Overview).
Proceedings of the IEEE Symposium on Visual Languages and Human-Centric Computing, 2014

Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations.
Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Dynamic Test Generation with Static Fields and Initializers.
Proceedings of the Runtime Verification - 5th International Conference, 2014

TouchGuru: Integrating Static Analysis with a Mobile Development Environment.
Proceedings of the 2nd International Workshop on Mobile Development Lifecycle, 2014

Static analysis for independent app developers.
Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, 2014

Constraint Semantics for Abstract Read Permissions.
Proceedings of 16th Workshop on Formal Techniques for Java-like Programs, 2014

2013
Object Ownership in Program Verification.
Proceedings of the Aliasing in Object-Oriented Programming. Types, 2013

Abstract Read Permissions: Fractional Permissions without the Fractions.
Proceedings of the Verification, 2013

Customizing the visualization and interaction for embedded domain-specific languages in a structured editor.
Proceedings of the 2013 IEEE Symposium on Visual Languages and Human Centric Computing, 2013

Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions.
Proceedings of the ECOOP 2013 - Object-Oriented Programming, 2013

2012
Behavioral interface specification languages.
ACM Comput. Surv., 2012

Comparing Verification Condition Generation with Symbolic Execution: An Experience Report.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Automatic Inference of Access Permissions.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Collaborative Verification and Testing with Explicit Assumptions.
Proceedings of the FM 2012: Formal Methods, 2012

2011
Formal Methods-Based Tools for Race, Deadlock, and Other Errors.
Proceedings of the Encyclopedia of Parallel Computing, 2011

Separating ownership topology and encapsulation with generic universe types.
ACM Trans. Program. Lang. Syst., 2011

Specification and verification: the Spec# experience.
Commun. ACM, 2011

Freedom before commitment: a lightweight type system for object initialisation.
Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2011

Using Debuggers to Understand Failed Verification Attempts.
Proceedings of the FM 2011: Formal Methods, 2011


Fractional permissions without the fractions.
Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs, 2011

Tunable Static Inference for Generic Universe Types.
Proceedings of the ECOOP 2011 - Object-Oriented Programming, 2011

2010
Reasoning about Function Objects.
Proceedings of the Objects, Models, Components, Patterns, 48th International Conference, 2010

Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups.
Proceedings of the Fundamental Approaches to Software Engineering, 2010

Proving Consistency and Completeness of Model Classes Using Theory Interpretation.
Proceedings of the Fundamental Approaches to Software Engineering, 2010

Deadlock-Free Channels and Locks.
Proceedings of the Programming Languages and Systems, 2010

2009
Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods.
J. Object Technol., 2009

A Sound and Complete Program Logic for Eiffel.
Proceedings of the Objects, Components, Models and Patterns, 47th International Conference, 2009

Verification of Concurrent Programs with Chalice.
Proceedings of the Foundations of Security Analysis and Design V, 2009

A Basis for Verifying Multi-threaded Programs.
Proceedings of the Programming Languages and Systems, 2009

A Modular Verification Methodology for C# Delegates.
Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009

2008
Faithful mapping of model classes to mathematical structures.
IET Softw., 2008

Flexible Immutability with Frozen Objects.
Proceedings of the Verified Software: Theories, 2008

Proof-Transforming Compilation of Eiffel Programs.
Proceedings of the Objects, Components, Models and Patterns, 46th International Conference, 2008

Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs.
Proceedings of the Advanced Lectures on Software Engineering, 2008

Checking Well-Formedness of Pure-Method Specifications.
Proceedings of the FM 2008: Formal Methods, 2008

Verification of Equivalent-Results Methods.
Proceedings of the Programming Languages and Systems, 2008

Aliasing, Confinement, and Ownership in Object-Oriented Programming.
Proceedings of the Object-Oriented Technology. ECOOP 2008 Workshop Reader, 2008

Formal Techniques for Java-Like Programs.
Proceedings of the Object-Oriented Technology. ECOOP 2008 Workshop Reader, 2008

A Unified Framework for Verification Techniques for Object Invariants.
Proceedings of the Types, Logics and Semantics for State, 03.02. - 08.02.2008, 2008

2007
Specification and verification challenges for sequential object-oriented programs.
Formal Aspects Comput., 2007

Formal Translation of Bytecode into BoogiePL.
Proceedings of the Second Workshop on Bytecode Semantics, 2007

Proof-transforming compilation of programs with abrupt termination.
Proceedings of the 2007 Conference Specification and Verification of Component-Based Systems, 2007

Sound reasoning about unchecked exceptions.
Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

Ownership transfer in universe types.
Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

Information Hiding and Visibility in Interface Specifications.
Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

Universe Types for Topology and Encapsulation.
Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

Generic Universe Types.
Proceedings of the ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30, 2007

07091 Abstracts Collection - Mobility, Ubiquity and Security.
Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

07091 Executive Summary - Mobility, Ubiquity and Security.
Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

2006
Modular invariants for layered object structures.
Sci. Comput. Program., 2006

Reasoning About Method Calls in Interface Specifications.
J. Object Technol., 2006

MOBIUS: Mobility, Ubiquity, Security.
Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

Changing Programs Correctly: Refactoring with Specifications.
Proceedings of the FM 2006: Formal Methods, 2006

A Pattern Language for Overlay Networks in Peer-to-Peer Systems.
Proceedings of the EuroPLoP' 2006, 2006

A Verification Methodology for Model Fields.
Proceedings of the Programming Languages and Systems, 2006

2005
Universes: Lightweight Ownership for JML.
J. Object Technol., 2005

A Program Logic for Bytecode.
Proceedings of the First Workshop on Bytecode Semantics, 2005

Reasoning about Object Structures Using Ownership.
Proceedings of the Verified Software: Theories, 2005

Modular Verification of Static Class Invariants.
Proceedings of the FM 2005: Formal Methods, 2005

2004
Formal Techniques for Java-Like Programs (FTfJP).
Proceedings of the Object-Oriented Technology: ECOOP 2004 Workshop Reader, 2004

Object Invariants in Dynamic Contexts.
Proceedings of the ECOOP 2004, 2004

A Type System for Checking Applet Isolation in Java Card.
Proceedings of the Construction and Analysis of Safe, 2004

2003
Modular specification of frame properties in JML.
Concurr. Comput. Pract. Exp., 2003

Formal Techniques for Java-Like Programs.
Proceedings of the Object-Oriented Technology: ECOOP 2003 Workshop Reader, 2003

2002
Modular Specification and Verification of Object-Oriented Programs
Lecture Notes in Computer Science 2262, Springer, ISBN: 3-540-43167-5, 2002

2000
Formal Techniques for Java Programs.
Proceedings of the Object-Oriented Technology, 2000

1999
Making Executable Interface Specifications More Expressive.
Proceedings of the JIT '99, 1999

A Programming Logic for Sequential Java.
Proceedings of the Programming Languages and Systems, 1999

Alias Control Is Crucial for Modular Verification of Object-Oriented Programs.
Proceedings of the Object-Oriented Technology, ECOOP'99 Workshop Reader, 1999

Formal Techniques for Java Programs.
Proceedings of the Object-Oriented Technology, ECOOP'99 Workshop Reader, 1999

1998
Logical foundations for typed object-oriented languages.
Proceedings of the Programming Concepts and Methods, 1998

Kapselung und Methodenbindung: Javas Designprobleme und ihre Korrektur.
Proceedings of the JIT '98, 1998

1997
Formal Specification Techniques for Object-Oriented Programs.
Proceedings of the Informatik '97, 1997


  Loading...