2025
Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, and Derek Dreyer: Destabilizing Iris
Programming Language Design and Implementation (PLDI), Proc. ACM Program. Lang., 2025.[PDF] [BIB]
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller: Formal Foundations for Translational Separation Logic Verifiers
Principles of Programming Languages (POPL), Proc. ACM Program. Lang., 2025.[PDF] [BIB] [Publisher]
2024
G. Parthasarathy: Formally Validating Translational Program Verifiers
Ph.D. Thesis, 2024.[PDF] [BIB]
Dongol, Brijesh, Dubois, Catherine, Hallerstede, Stefan, Hehner, Eric, Morgan, Carroll, Müller, Peter, Ribeiro, Leila, Silva, Alexandra, Smith, Graeme, and de Vink, Erik: On Formal Methods Thinking in Computer Science Education
Form. Asp. Comput., 2024.[PDF] [BIB] [Publisher]
F. A. Wolf: Automated Verification of Advanced Correctness and Security Properties
Ph.D. Thesis, 2024.[PDF] [BIB]
F. A. Wolf and P. Müller: Verifiable Security Policies for Distributed Systems
Computer and Communications Security (CCS), 2024.[PDF] [BIB] [Publisher]
T. Dardinier, A. Li, and P. Müller: Hypra: A Deductive Program Verifier for Hyper Hoare Logic
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2024.[PDF] [BIB] [Publisher]
F. Poli: Enabling Rich Lightweight Verification of Rust Software
Ph.D. Thesis, 2024.[PDF] [BIB]
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller: Formal Foundations for Translational Separation Logic Verifiers
Technical Report, 2024.[PDF] [BIB] [arXiv]
S. Rain, L. S. Brugger, A. Petkovic Komel, L. Kovács, and M. Rawson: Scaling CheckMate for Game-Theoretic Security
LPAR 2024: Proceedings of 25th Conference on Logic for Programming,
Artificial Intelligence and Reasoning, Port Louis, Mauritius, May
26-31, 2024, 2024.[PDF] [BIB] [Publisher]
V. Astrauskas: Leveraging Uniqueness for Modular Verification of Heap-Manipulating Programs
Ph.D. Thesis, 2024.[PDF] [BIB]
M. Eilers, M. Schwerhoff, and P. Müller: Verification Algorithms for Automated Separation Logic Verifiers
Computer Aided Verification (CAV), 2024.[PDF] [BIB] [Publisher]
Federico Poli, Xavier Denis, Peter Müller, and Alexander J. Summers: Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
Technical Report, 2024.[PDF] [BIB] [arXiv]
T. Dardinier and P. Müller: Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
Programming Language Design and Implementation (PLDI), Proc. ACM Program. Lang., 2024.[PDF] [BIB] [Publisher]
G. Parthasarathy, T. Dardinier, B. Bonneau, P. Müller, and A. J. Summers: Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
Programming Language Design and Implementation (PLDI), Proc. ACM Program. Lang., 2024.[PDF] [BIB] [Publisher] [Extended Version (arXiv)]
2023
A. Bílý, J. C. Pereira, J. Schär, and P. Müller: Refinement Proofs in Rust Using Ghost Locks
Technical Report, arXiv 2023.[PDF] [BIB] [arXiv]
A. Bílý, J. Hansen, P. Müller, and A. J. Summers: Compositional Reasoning about Advanced Iterator Patterns in Rust
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2023.[PDF] [BIB] [Publisher] [Talk]
L. S. Brugger, L. Kovács, A. Petković Komel, S. Rain, and M. Rawson: CheckMate: Automated Game-Theoretic Security Reasoning
Computer and Communications Security (CCS), 2023.[PDF] [BIB] [Publisher]
L. S. Brugger, L. Kovács, A. Petković Komel, S. Rain, and M. Rawson: CheckMate: Automated Game-Theoretic Security Reasoning (extended version)
Technical Report, EasyChair 2023.[PDF] [BIB] [EasyChair]
L. Arquint, M. Schwerhoff, V. Mehta, and P. Müller: A Generic Methodology for the Modular Verification of Security Protocol Implementations
Computer and Communications Security (CCS), 2023.[PDF] [BIB] [Publisher]
L. Arquint, M. Schwerhoff, V. Mehta, and P. Müller: A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)
Technical Report, arXiv 2023.[PDF] [BIB] [arXiv]
F. A. Wolf, M. Schwerhoff, and P. Müller: Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA
Formal Methods in System Design, 2023.[PDF] [BIB] [Publisher]
J. Fiala, S. Itzhaky, P. Müller, N. Polikarpova, and I. Sergey: Leveraging Rust Types for Program Synthesis
Programming Language Design and Implementation (PLDI), Proc. ACM Program. Lang., 2023.[PDF] [BIB] [Publisher]
M. Eilers, T. Dardinier, and P. Müller: CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
Programming Language Design and Implementation (PLDI), Proc. ACM Program. Lang., 2023.[PDF] [BIB] [Publisher]
T. Dardinier, G. Parthasarathy, and P. Müller: Verification-Preserving Inlining in Automatic Separation Logic Verifiers
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2023.[PDF] [BIB] [Publisher]
T. Dardinier and P. Müller: Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
Technical Report, arXiv 2023. [BIB] [arXiv]
L. Arquint, F. A. Wolf, J. Lallemand, R. Sasse, C. Sprenger, S. N. Wiesner, D. Basin, and P. Müller: Sound Verification of Security Protocols: From Design to Interoperable Implementations
2023 IEEE Symposium on Security and Privacy (SP), 2023.[PDF] [BIB] [Publisher] [Talk]
A. Bugariu, A. Ter-Gabrielyan, and P. Müller: Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (extended version)
Form. Asp. Comput., 2023.[PDF] [BIB] [Publisher]
2022
L. Arquint, F. A. Wolf, J. Lallemand, R. Sasse, C. Sprenger, S. N. Wiesner, D. Basin, and P. Müller: Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)
Technical Report, arXiv 2022.[PDF] [BIB] [arXiv]
M. Eilers, T. Dardinier, and P. Müller: CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
Technical Report, arXiv 2022.[PDF] [BIB] [arXiv]
T. Dardinier, P. Müller, and A. J. Summers: Fractional Resources in Unbounded Separation Logic
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2022.[PDF] [BIB] [Publisher]
A. Bílý, J. Hansen, P. Müller, and A. J. Summers: Compositional Reasoning for Side-effectful Iterators and Iterator Adapters
Technical Report, arXiv 2022.[PDF] [BIB] [arXiv]
J. Dohrau: Automatic Inference of Permission Specifications
Ph.D. Thesis, 2022.[PDF] [BIB]
M. Eilers: Modular Specification and Verification of Security Properties for Mainstream Languages
Ph.D. Thesis, 2022.[PDF] [BIB]
D. Basin, T. Dardinier, N. Hauser, L. Heimes, J. J. Huerta y Munive, N. Kaletsch, S. Krstić, E. Marsicano, M. Raszyk, J. Schneider, D. L. Tirore, D. Traytel, and S. Zingg: VeriMon: A Formally Verified Monitoring Tool
Theoretical Aspects of Computing (ICTAC), 2022.[PDF] [BIB] [Publisher]
T. Dardinier, G. Parthasarathy, and P. Müller: Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
Technical Report, arXiv 2022. [BIB] [arXiv]
T. Dardinier, G. Parthasarathy, N. Weeks, A. J. Summers, and P. Müller: Sound Automation of Magic Wands
Computer Aided Verification (CAV), 2022.[PDF] [BIB] [Publisher]
T. Dardinier, G. Parthasarathy, N. Weeks, A. J. Summers, and P. Müller: Sound Automation of Magic Wands (extended version)
Technical Report, arXiv 2022.[PDF] [BIB] [arXiv]
V. Astrauskas, A. Bílý, J. Fiala, Z. Grannan, C. Matheja, P. Müller, F. Poli, and A. J. Summers: The Prusti Project: Formal Verification for Rust
NASA Formal Methods (14th International Symposium), 2022.[PDF] [BIB] [Publisher]
L. Chuat, M. Legner, D. Basin, D. Hausheer, S. Hitz, P. Müller, and A. Perrig: The Complete Guide to SCION
2022. [BIB] [Publisher]
A. Bugariu: Automatically Identifying Soundness and Completeness Errors in Program Analysis Tools
Ph.D. Thesis, 2022.[PDF] [BIB]
2021
A. Ter-Gabrielyan: Compositional Verification of Rich Program Properties in Separation Logic
Ph.D. Thesis, 2021.[PDF] [BIB]
J. Bornholt, R. Joshi, V. Astrauskas, B. Cully, B. Kragl, S. Markle, K. Sauri, D. Schleit, G. Slatton, S. Tasiran, J. Van Geffen, and A. Warfield: Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3
Symposium on Operating Systems Principles (SOSP), 2021.[PDF] [BIB] [Publisher]
A. Bílý, C. Matheja, and P. Müller: Flexible Refinement Proofs in Separation Logic
Technical Report, arXiv 2021.[PDF] [BIB] [arXiv]
P. Müller and N. Shankar: The First Fifteen Years of the Verified Software Project
Theories of Programming: The Life and Works of Tony Hoare, 2021.[PDF] [BIB] [Publisher]
F. Wolff, A. Bílý, C. Matheja, P. Müller, and A. J. Summers: Modular Specification and Verification of Closures in Rust
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2021.[PDF] [BIB] [Talk]
C. Bräm, M. Eilers, P. Müller, R. Sierra, and A. J. Summers: Rich Specifications for Ethereum Smart Contract Verification
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2021.[PDF] [BIB] [Talk]
F. A. Wolf, M. Schwerhoff, and P. Müller: Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA
Formal Methods (FM), 2021.[PDF] [BIB] [Publisher]
A. Bugariu, A. Ter-Gabrielyan, and P. Müller: Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (extended version)
Technical Report, arXiv 2021.[PDF] [BIB] [arXiv]
A. Bugariu, A. Ter-Gabrielyan, and P. Müller: Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers
Formal Methods (FM), 2021.[PDF] [BIB] [Publisher]
F. A. Wolf, L. Arquint, M. Clochard, W. Oortwijn, J. C. Pereira, and P. Müller: Gobra: Modular Specification and Verification of Go Programs
Computer Aided Verification (CAV), 2021.[PDF] [BIB] [Publisher] [Talk]
F. A. Wolf, L. Arquint, M. Clochard, W. Oortwijn, J. C. Pereira, and P. Müller: Gobra: Modular Specification and Verification of Go Programs (extended version)
Technical Report, arXiv 2021. [BIB] [arXiv]
G. Parthasarathy, P. Müller, and A. J. Summers: Formally Validating a Practical Verification Condition Generator
Computer Aided Verification (CAV), 2021.[PDF] [BIB] [Publisher]
G. Parthasarathy, P. Müller, and A. J. Summers: Formally Validating a Practical Verification Condition Generator (extended version)
Technical Report, arXiv 2021.[PDF] [BIB] [arXiv]
C. Dross, C. A. Furia, M. Huisman, R. Monahan, and P. Müller: VerifyThis 2019: a program verification competition
International Journal on Software Tools for Technology Transfer (STTT), 2021.[PDF] [BIB] [Publisher]
M. Eilers, S. Meier, and P. Müller: Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security
Computer Aided Verification (CAV), 2021.[PDF] [BIB] [Publisher]
K. Batz, M. Chen, B. Kaminski, J.-P. Katoen, C. Matheja, and P. Schr\"oer: Latticed k-Induction with an Application to Probabilistic Programs
Computer Aided Verification (CAV), 2021.[PDF] [BIB] [Publisher]
I. Fesefeldt, C. Matheja, T. Noll, and J. Schulte: Automated Checking and Completion of Backward Confluence for Hyperedge
Replacement Grammars
International Conference on Graph Transformation (ICGT), 2021.[PDF] [BIB] [Publisher]
K. Batz, B. L. Kaminski, J.-P. Katoen, and C. Matheja: Relatively Complete Verification of Probabilistic Programs: An Expressive Language for Expectation-Based Reasoning
Principles of Programming Languages (POPL), Proc. ACM Program. Lang., 2021.[PDF] [BIB] [Publisher]
A. Aguirre, G. Barthe, J. Hsu, B. L. Kaminski, J.-P. Katoen, and C. Matheja: A Pre-Expectation Calculus for Probabilistic Sensitivity
Principles of Programming Languages (POPL), Proc. ACM Program. Lang., 2021.[PDF] [BIB] [Publisher]
2020
F. A. Wolf, M. Schwerhoff, and P. Müller: Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA (Full Paper)
Technical Report, arXiv 2020.[PDF] [BIB] [arXiv]
V. Astrauskas, C. Matheja, P. Müller, F. Poli, and A. J. Summers: How Do Programmers Use Unsafe Rust?
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2020.[PDF] [BIB] [Talk]
C. Sprenger, T. Klenze, M. Eilers, F. A. Wolf, P. Müller, M. Clochard, and D. Basin: Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2020.[PDF] [BIB] [Talk]
C. Sprenger, T. Klenze, M. Eilers, F. A. Wolf, P. Müller, M. Clochard, and D. Basin: Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
Technical Report, arXiv 2020.[PDF] [BIB] [arXiv]
C. Dross, C.A. Furia, M. Huisman, R. Monahan, and P. Müller: VerifyThis 2019: A Program Verification Competition (Extended Report)
Technical Report, arXiv 2020.[PDF] [BIB] [arXiv]
S. Krishna, A. J. Summers, and T. Wies: Local Reasoning for Global Graph Properties
European Symposium on Programming (ESOP), 2020.[PDF] [BIB]
Oortwijn, W., Huisman, M., Joosten, S., and Pol, J. van de: Automated Verification of Parallel Nested DFS
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2020.[PDF] [BIB]
A. J. Summers and P. Müller: Automating Deductive Verification for Weak-Memory Programs (extended version)
International Journal on Software Tools for Technology Transfer (STTT), 2020.[PDF] [BIB]
Bugariu, Alexandra and Müller, Peter: Automatically Testing String Solvers
Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE), 2020.[PDF] [BIB] [Publisher]
Clochard, Martin, Marché, Claude, and Paskevich, Andrei: Deductive Verification with Ghost Monitors
Principles of Programming Languages (POPL), 2020.[PDF] [BIB] [Publisher]
R. Jung, R. Lepigre, G. Parthasarathy, M. Rapoport, A. Timany, D. Dreyer, and B. Jacobs: The Future is Ours: Prophecy Variables in Separation Logic
Principles of Programming Languages (POPL), 2020.[PDF] [BIB]
Oortwijn, W., Gurov, D., and Huisman, M.: Practical Abstractions for Automated Verification of Shared-Memory Concurrency
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2020.[PDF] [BIB] [Publisher]
2019
P. Müller: Building Deductive Program Verifiers (Lecture Notes)
Engineering Secure and Dependable Software Systems, 2019.[PDF] [BIB]
M. Eilers, P. Müller, and S. Hitz: Modular Product Programs
ACM Trans. Program. Lang. Syst., 2019.[PDF] [BIB] [Publisher]
V. Astrauskas, P. Müller, F. Poli, and A. J. Summers: Leveraging Rust Types for Modular Specification and Verification
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2019.[PDF] [BIB] [Publisher]
A. Ter-Gabrielyan, A. J. Summers, and P. Müller: Modular Verification of Heap Reachability Properties in Separation Logic
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang., 2019.[PDF] [BIB] [Publisher]
V. Astrauskas, P. Müller, F. Poli, and A. J. Summers: Leveraging Rust Types for Modular Specification and Verification
Technical Report, ETH Zurich 2019.[PDF] [BIB] [ETH Collection]
N. Becker, P. Müller, and A. J. Summers: The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2019.[PDF] [BIB]
2018
P. Müller: The Binomial Heap Verification Challenge in Viper
Principled Software Development, 2018.[PDF] [BIB] [Publisher]
F. Guth, V. Wüstholz, M. Christakis, and P. Müller: Specification Mining for Smart Contracts with Automatic Abstraction Tuning
Technical Report, arXiv 2018.[PDF] [BIB] [arXiv]
A. Bugariu, V. Wüstholz, M. Christakis, and P. Müller: Automatically Testing Implementations of Numerical Abstract Domains
Automated Software Engineering (ASE), 2018.[PDF] [BIB] [Publisher]
C. Urban, S. Ueltschi, and P. Müller: Abstract Interpretation of CTL Properties
Static Analysis Symposium (SAS), 2018.[PDF] [BIB] [Publisher]
L. Brutschy, D. Dimitrov, P. Müller, and M. Vechev: Static Serializability Analysis for Causal Consistency
Programming Language Design and Implementation (PLDI), 2018.[PDF] [BIB] [Publisher]
J. Dohrau, A. J. Summers, C. Urban, S. Münger, and P. Müller: Permission Inference for Array Programs
Computer Aided Verification (CAV), 2018.[PDF] [BIB] [Publisher]
J. Dohrau, A. J. Summers, C. Urban, S. Münger, and P. Müller: Permission Inference for Array Programs (extended version)
Technical Report, arXiv 2018.[PDF] [BIB] [arXiv]
M. Eilers and P. Müller: Nagini: A Static Verifier for Python
Computer Aided Verification (CAV), 2018.[PDF] [BIB] [Publisher]
M. Hassan, C. Urban, M. Eilers, and P. Müller: MaxSMT-Based Type Inference for Python 3
Computer Aided Verification (CAV), 2018.[PDF] [BIB] [Publisher]
A. J. Summers and P. Müller: Automating Deductive Verification for Weak-Memory Programs
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018.[PDF] [BIB] [Publisher]
A. J. Summers and P. Müller: Automating Deductive Verification for Weak-Memory Programs (extended version)
Technical Report, arXiv 2018.[PDF] [BIB] Link
M. Eilers, P. Müller, and S. Hitz: Modular Product Programs
European Symposium on Programming (ESOP), 2018.[PDF] [BIB] [Publisher]
C. Urban and P. Müller: An Abstract Interpretation Framework for Input Data Usage
European Symposium on Programming (ESOP), 2018.[PDF] [BIB] [Publisher]
2017
M. Christakis, P. Emmisberger, P. Godefroid, and P. Müller: A General Framework for Dynamic Stub Injection
International Conference on Software Engineering (ICSE), 2017.[PDF] [BIB] [Publisher]
D. Asenov: Envision: Reinventing the Integrated Development Environment
Ph.D. Thesis, 2017.[PDF] [BIB]
D. Asenov, B. Guenat, P. Müller, and M. Otth: Precise Version Control of Trees with Line-based Version Control Systems
Fundamental Approaches to Software Engineering (FASE), 2017.[PDF] [BIB] [Publisher]
N. Courant and C. Urban: Precise Widening Operators for Proving Termination by Abstract Interpretation
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017.[PDF] [BIB] [Publisher]
L. Brutschy, D. Dimitrov, P. Müller, and M. Vechev: Serializability for Eventual Consistency: Criterion, Analysis, and Applications
Principles of Programming Languages (POPL), 2017.[PDF] [BIB] [Publisher]
V. D'Silva and C. Urban: Abstract Interpretation as Automated Deduction
Journal of Automated Reasoning, 2017. [BIB] [Publisher]
C. Urban and A. Miné: Inference of Ranking Functions for Proving Temporal Properties by Abstract Interpretation
Computer Languages, Systems & Structures, 2017.[PDF] [BIB] [Publisher]
2016
U. Juhasz: Incremental Verification
Ph.D. Thesis, 2016.[PDF] [BIB]
M. Schwerhoff: Advancing Automated, Permission-Based Program Verification Using Symbolic Execution
Ph.D. Thesis, 2016.[PDF] [BIB]
M. Christakis, P. Emmisberger, P. Godefroid, and P. Müller: A General Framework for Dynamic Stub Injection
Technical Report, Microsoft Research 2016.[PDF] [BIB]
D. Asenov, P. Müller, and L. Vogel: The IDE As a Scriptable Information System
Automated Software Engineering (ASE), 2016.[PDF] [BIB] [Publisher]
D. Asenov, P. Müller, and L. Vogel: The IDE as a Scriptable Information System (extended version)
arXiv:1607.04452 [cs.SE], 2016.[PDF] [BIB]
P. Müller, M. Schwerhoff, and A. J. Summers: Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
Computer Aided Verification (CAV), 2016.[PDF] [BIB] [Publisher]
M. Huisman, R. Monahan, P. Müller, and E. Poll: VerifyThis 2016: A Program Verification Competition
Technical Report, Centre for Telematics and Information Technology, University of Twente 2016.[PDF] [BIB] Link
V. D'Silva and C. Urban: Büchi, Lindenbaum, Tarski: A Program Analysis Appetizer
International Joint Conference on Artificial Intelligence (IJCAI), 2016.[PDF] [BIB] [Publisher]
M. Christakis, P. Müller, and V. Wüstholz: Guiding Dynamic Symbolic Execution toward Unverified Program Executions
International Conference on Software Engineering (ICSE), 2016.[PDF] [BIB] [Publisher]
D. Asenov, O. Hilliges, and P. Müller: The Effect of Richer Visualizations on Code Comprehension
Human Factors in Computing Systems (CHI), 2016.[PDF] [BIB] [Publisher]
A. J. Summers and P. Müller: Actor Services: Modular Verification of Message Passing Programs
European Symposium on Programming (ESOP), 2016.[PDF] [BIB] [Publisher]
M. Christakis, K. R. M. Leino, P. Müller, and V. Wüstholz: Integrated Environment for Diagnosing Verification Errors
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016.[PDF] [BIB] [Publisher]
C. Favre, H. V\"olzer, and P. Müller: Diagnostic Information for Control-Flow Analysis of Workflow Graphs (aka Free-ChoiceWorkflow Nets)
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016.[PDF] [BIB] [Publisher]
C. Urban, A. Gurfinkel, and T. Kahsai: Synthesizing Ranking Functions from Bits and Pieces
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016.[PDF] [BIB] [Publisher]
P. Müller, M. Schwerhoff, and A. J. Summers: Viper: A Verification Infrastructure for Permission-Based Reasoning
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2016.[PDF] [BIB] [Publisher]
2015
V. Wüstholz: Partial Verification Results
Ph.D. Thesis, 2015.[PDF] [BIB]
L. Brutschy, P. Ferrara, O. Tripp, and M. Pistoia: ShamDroid: Gracefully Degrading Functionality in the Presence of Limited Resource Access
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2015.[PDF] [BIB] [Publisher]
Maria Christakis: Narrowing the Gap between Verification and Systematic Testing
Ph.D. Thesis, 2015.[PDF] [BIB]
C. Favre, H. V\"olzer, and P. Müller: Diagnostic Information for Control-Flow Analysis of Workflow Graphs (aka Free-Choice Workflow Nets)
Technical Report, ETH Zurich 2015.[PDF] [BIB]
M. Christakis and P. Godefroid: IC-Cut: A Compositional Search Strategy for Dynamic Test Generation
SPIN Symposium on Model Checking of Software (SPIN), 2015.[PDF] [BIB] [Publisher]
K. R. M. Leino and V. Wüstholz: Fine-grained Caching of Verification Results
Computer Aided Verification (CAV), 2015.[PDF] [BIB] [Publisher]
M. Christakis, P. Müller, and V. Wüstholz: Guiding Dynamic Symbolic Execution toward Unverified Program Executions
Technical Report, ETH Zurich 2015.[PDF] [BIB]
M. Schwerhoff and A. J. Summers: Lightweight Support for Magic Wands in an Automatic Verifier
European Conference on Object-Oriented Programming (ECOOP), 2015.[PDF] [BIB] [Publisher]
P. Bostr\"om and P. Müller: Modular Verification of Finite Blocking in Non-terminating Programs
European Conference on Object-Oriented Programming (ECOOP), 2015.[PDF] [BIB] [Publisher]
M. Christakis and P. Godefroid: IC-Cut: A Compositional Search Strategy for Dynamic Test Generation
Technical Report, Microsoft Research 2015.[PDF] [BIB]
P. Ferrara, P. Müller, and M. Novacek: Automatic Inference of Heap Properties Exploiting Value Domains
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015.[PDF] [BIB] [Publisher]
M. Christakis and P. Godefroid: Proving Memory Safety of the ANI Windows Image Parser using Compositional Exhaustive Testing
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015.[PDF] [BIB] [Publisher]
M. Christakis, P. Müller, and V. Wüstholz: An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015.[PDF] [BIB] [Publisher]
2014
P. Bostr\"om and P. Müller: Modular Verification of Finite Blocking in Non-terminating Programs
Technical Report, ETH Zurich 2014.[PDF] [BIB]
L. Brutschy, P. Ferrara, and P. Müller: Static Analysis for Independent App Developers
Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2014.[PDF] [BIB] [Publisher]
L. Brutschy, P. Ferrara, and P. Müller: TouchGuru: Integrating Static Analysis with a Mobile Development Environment
Mobile Development Lifecycle (MobileDeLi), 2014.[PDF] [BIB] [Publisher]
J. Boyland, P. Müller, M. Schwerhoff, and A. J. Summers: Constraint Semantics for Abstract Read Permissions
Formal Techniques for Java-like Programs (FTfJP), 2014.[PDF] [BIB] [Publisher]
M. Christakis, P. Emmisberger, and P. Müller: Dynamic Test Generation with Static Fields and Initializers
Runtime Verification (RV), 2014.[PDF] [BIB] [Publisher]
M. Christakis, P. Müller, and V. Wüstholz: An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer
Technical Report, ETH Zurich 2014.[PDF] [BIB]
M. Christakis, P. Müller, and V. Wüstholz: Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations
Software Engineering and Formal Methods (SEFM), 2014.[PDF] [BIB] [Publisher]
M. Christakis, K. R. M. Leino, and W. Schulte: Formalizing and Verifying a Modern Build Language
Formal Methods (FM), 2014.[PDF] [BIB] [Publisher]
J. T. Boyland, P. Müller, M. Schwerhoff, and A. J. Summers: Constraint Semantics for Abstract Read Permissions
Technical Report, ETH Zurich 2014.[PDF] [BIB]
U. Juhasz, I. T. Kassios, P. Müller, M. Novacek, M. Schwerhoff, and A. J. Summers: Viper: A Verification Infrastructure for Permission-Based Reasoning
Technical Report, ETH Zurich 2014.[PDF] [BIB]
D. Asenov and P. Müller: Envision: A Fast and Flexible Visual Code Editor with Fluid Interactions (Overview)
Visual Languages and Human-Centric Computing (VL/HCC), 2014.[PDF] [BIB] [Publisher]
D. Asenov and P. Müller: Envision: A Fast and Flexible Visual Code Editor with Fluid Interactions
Technical Report, ETH Zurich 2014.[PDF] [BIB]
M. Schwerhoff and A. J. Summers: Lightweight Support for Magic Wands in an Automatic Verifier
Technical Report, ETH Zurich 2014.[PDF] [BIB]
K. R. M. Leino and V. Wüstholz: The Dafny Integrated Development Environment
1st Workshop on Formal Integrated Development Environment, 2014.[PDF] [BIB] [Publisher]
P. Ferrara, D. Schweizer, and L. Brutschy: TouchCost: Cost Analysis of TouchDevelop Scripts
Fundamental Approaches to Software Engineering (FASE), 2014.[PDF] [BIB] [Publisher]
P. Ferrara: Generic Combination of Heap and Value Analyses in Abstract Interpretation
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2014.[PDF] [BIB] [Publisher]
2013
M. Christakis and P. Godefroid: Proving Memory Safety of the ANI Windows Image Parser using Compositional Exhaustive Testing
Technical Report, Microsoft Research 2013.[PDF] [BIB]
M. Christakis, A. Gotovos, and K. Sagonas: Systematic Testing for Detecting Concurrency Errors in Erlang Programs
International Conference on Software Testing, Verification and Validation (ICST), 2013.[PDF] [BIB] [Publisher]
P. Ferrara, P. Müller, and M. Novacek: Automatic Inference of Heap Properties Exploiting Value Domains
Technical Report, ETH Zurich 2013.[PDF] [BIB]
D. Jost and A. J. Summers: An automatic encoding from VeriFast Predicates into Implicit Dynamic Frames
Verified Software: Theories, Tools and Experiments (VSTTE), 2013.[PDF] [BIB] [Publisher]
A. Cortesi, P. Ferrara, and N. Chaki: Static Analysis Techniques for Robotics Software Verification
International Symposium of Robotics (ISR), 2013.[PDF] [BIB] [Publisher]
G. Costantini, P. Ferrara, A. Cortesi, and G. Maggiore: The Domain of Parametric Hypercubes for Static Analysis of Computer Games Software
International Conference on Formal Engineering Methods (ICFEM), 2013.[PDF] [BIB] [Publisher]
D. Asenov and P. Müller: Customizing the Visualization and Interaction for Embedded Domain-Specific Languages in a Structured Editor
Visual Languages and Human-Centric Computing (VL/HCC), 2013.[PDF] [BIB] [Publisher]
S. Heule, I. T. Kassios, P. Müller, and A. J. Summers: Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions
European Conference on Object-Oriented Programming (ECOOP), 2013.[PDF] [BIB] [Publisher]
A. J. Summers and S. Drossopoulou: A Formal Semantics for Isorecursive
and Equirecursive State Abstractions
European Conference on Object-Oriented Programming (ECOOP), 2013.[PDF] [BIB] [Publisher]
W. Dietl and P. Müller: Object Ownership in Program Verification
Aliasing in Object-Oriented Programming, 2013.[PDF] [BIB] [Publisher]
P. Ferrara: A generic static analyzer for multithreaded Java programs
Software: Practice and Experience, 2013.[PDF] [BIB] [Publisher]
I. T. Kassios and E. Kritikos: A Discipline for Program Verification based on Backpointers and its Use in Observational Disjointness
European Symposium of Programming (ESOP), 2013.[PDF] [BIB] [Publisher]
S. Heule, K. R. M. Leino, P. Müller, and A. J. Summers: Abstract Read Permissions: Fractional Permissions without the Fractions
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013.[PDF] [BIB] [Publisher]
2012
S. Heule, I. T. Kassios, P. Müller, and A. J. Summers: Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions
Technical Report, ETH Zurich 2012.[PDF] [BIB]
A. J. Summers and S. Drossopoulou: A Formal Semantics for Isorecursive and Equirecursive State Abstractions
Technical Report, ETH Zurich 2012.[PDF] [BIB]
I. T. Kassios and E. Kritikos: A Discipline for Program Verification based on Backpointers and its Use in Observational Disjointness
Technical Report, ETH Zurich 2012.[PDF] [BIB]
S. Balzer, T. Gross, and P. Müller: Selective Ownership: Combining Object and Type Hierarchies for Flexible Sharing
Foundations of Object-Oriented Languages (FOOL), 2012.[PDF] [BIB]
G. Costantini, P. Ferrara, and A. Cortesi: Linear approximation of continuous systems with Trapezoid Step Functions
Asian Symposium on Programming Languages and Systems (APLAS), 2012.[PDF] [BIB] [Publisher]
E. M. Clarke, W. Klieber, M. Novacek, and P. Zuliani: Model Checking and the State Explosion Problem
Tools for Practical Software Verification, 2012.[PDF] [BIB] [Publisher]
J. N. Ruskiewicz: Localizing and Understanding Verification Errors
Ph.D. Thesis, 2012.[PDF] [BIB]
P. Ferrara, R. Fuchs, and U. Juhasz: TVAL+ : TVLA and Value Analyses Together
Software Engineering and Formal Methods (SEFM), 2012.[PDF] [BIB] [Publisher]
M. Christakis, P. Müller, and V. Wüstholz: Collaborative Verification and Testing with Explicit Assumptions
Formal Methods (FM), 2012.[PDF] [BIB] [Publisher]
S. Heule, I. T. Kassios, P. Müller, and A. J. Summers: Verification Condition Generation for Permission Logics with Abstraction Functions
Technical Report, ETH Zurich 2012.[PDF] [BIB]
M. J. Parkinson and A. J. Summers: The Relationship Between Separation Logic and Implicit Dynamic Frames
Logical Methods in Computer Science, 2012.[PDF] [BIB] [Publisher]
J. Hatcliff, G. T. Leavens, K. R. M. Leino, P. Müller, and M. Parkinson: Behavioral Interface Specification Languages
Computing Surveys, 2012.[PDF] [BIB] [Publisher]
I. T. Kassios, P. Müller, and M. Schwerhoff: Comparing Verification Condition Generation with Symbolic Execution: an Experience Report
Verified Software Theories Tools Experiments (VSTTE), 2012.[PDF] [BIB] [Publisher]
M. Zanioli, P. Ferrara, and A. Cortesi: SAILS: static analysis of information leakage with Sample
ACM Symposium on Applied Computing (SAC), 2012.[PDF] [BIB] [Publisher]
P. Ferrara and P. Müller: Automatic inference of access permissions
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2012.[PDF] [BIB] [Publisher]
2011
A. Rudich: Automatic Verification of Heap Structures with Stereotypes
Ph.D. Thesis, 2011.[PDF] [BIB]
W. Dietl, S. Drossopoulou, and P. Müller: Separating ownership topology and encapsulation with generic universe types
ACM Trans. Program. Lang. Syst., 2011.[PDF] [BIB] [Publisher]
H. Lehner: A Formal Definition of JML in Coq and its Application to Runtime Assertion Checking
Ph.D. Thesis, 2011.[PDF] [BIB] Coq Sources
A. J. Summers and P. Müller: Freedom Before Commitment - A Lightweight Type System for Object Initialisation
Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2011.[PDF] [BIB] [Publisher]
I. T. Kassios: Dynamic Frames and Automated Verification
2011.[PDF] [BIB]
G. Costantini, P. Ferrara, and A. Cortesi: Static Analysis of String Values
International Conference on Formal Engineering Methods (ICFEM), 2011.[PDF] [BIB] [Publisher]
S. Heule, K. R. M. Leino, P. Müller, and A. J. Summers: Fractional Permissions Without the Fractions
Formal Techniques for Java-like Programs (FTfJP), 2011.[PDF] [BIB] [Publisher]
W. Dietl, M. Ernst, and P. Müller: Tunable Static Inference for Generic Universe Types
European Conference on Object-Oriented Programming (ECOOP), 2011.[PDF] [BIB] [Publisher]
P. Müller and J. N. Ruskiewicz: Using Debuggers to Understand Failed Verification Attempts
Formal Methods (FM), 2011.[PDF] [BIB] [Publisher]
V. Klebanov, P. Müller, N. Shankar, G. T. Leavens, V. Wüstholz, E. Alkassar, R. Arthan, D. Bronish, R. Chapman, E. Cohen, M. Hillebrand, B. Jacobs, K. R. M. Leino, R. Monahan, F. Piessens, N. Polikarpova, T. Ridge, J. Smans, S. Tobies, T. Tuerk, M. Ulbrich, and B. Weiss: The 1st Verified Software Competition: Experience Report
Formal Methods (FM), 2011.[PDF] [BIB] [Publisher]
I. T. Kassios and P. Müller: Modular Specification and Verification of Delegation with SMT Solvers
Technical Report, ETH Zurich 2011.[PDF] [BIB]
I. T. Kassios: The Dynamic Frames Theory
Formal Aspects of Computing, 2011.[PDF] [BIB] [Publisher]
A. J. Summers and P. Müller: Freedom Before Commitment :
Simple Flexible Initialisation for Non-Null Types
Technical Report, ETH Zurich 2011.[PDF] [BIB]
P. Müller and J. N. Ruskiewicz: Using Debuggers to Understand Failed Verification Attempts
Technical Report, ETH Zurich 2011.[PDF] [BIB]
M. J. Parkinson and A. J. Summers: The Relationship Between Separation Logic and Implicit Dynamic Frames
European Symposium on Programming (ESOP), 2011.[PDF] [BIB] [Publisher]
M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter: Specification and Verification: The Spec\# Experience
Communications of the ACM, 2011.[PDF] [BIB] [Publisher]
2010
R. Joshi, T. Margaria, P. Müller, D. Naumann, and H. Yang: VSTTE 2010 Workshop Proceedings
Technical Report, ETH Zurich 2010.[PDF] [BIB]
M. Nordio, C. Calcagno, B. Meyer, P. Müller, and J. Tschannen: Reasoning about Function Objects
TOOLS-EUROPE, 2010.[PDF] [BIB] [Publisher]
P. Ferrara: Static Type Analysis of Pattern Matching by Abstract Interpretation
Formal Techniques for Distributed Systems (FMOODS/FORTE), 2010.[PDF] [BIB] [Publisher]
W. Dietl, M. Ernst, and P. Müller: Tunable Universe Type Inference
Technical Report, ETH Zurich 2010.[PDF] [BIB]
I. T. Kassios and P. Müller: Specification and Verification of Closures
Technical Report, ETH Zurich 2010.[PDF] [BIB]
A. J. Summers: Soundness and Principal Contexts for a Shallow Polymorphic Type System based on Classical Logic
Logic Journal of IGPL, 2010.[PDF] [BIB] [Publisher]
K. R. M. Leino, P. Müller, and J. Smans: Deadlock-free Channels and Locks
European Symposium on Programming (ESOP), 2010.[PDF] [BIB] [Publisher]
K. R. M. Leino, P. Müller, and J. Smans: Deadlock-free Channels and Locks
Technical Report, Department of Computer Science, K.U.Leuven 2010.[PDF] [BIB] Link
H. Lehner and P. Müller: Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups
Fundamental Approaches to Software Engineering (FASE), 2010.[PDF] [BIB] [Publisher]
\'A. Darvas and P. Müller: Proving Consistency and Completeness of Model Classes Using Theory Interpretation
Fundamental Approaches to Software Engineering (FASE), 2010.[PDF] [BIB] [Publisher]
T. A. Henzinger, T. Hottelier, L. Kovacs, and A. Voronkov: Invariant and Type Inference for Matrices
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2010.[PDF] [BIB] [Publisher]
A. J. Summers and S. Drossopoulou: Considerate Reasoning and the Composite Design Pattern
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2010.[PDF] [BIB] [Publisher]
K. R. M. Leino and P. Müller: Using the Spec\# Language, Methodology, and Tools to Write Bug-Free Programs
Advanced Lectures on Software Engineering---LASER Summer School 2007/2008, 2010.[PDF] [BIB] [Publisher]
2009
P. Müller and J. N. Ruskiewicz: A modular verification methodology for C\# delegates
Rigorous Methods for Software Construction and Analysis, 2009.[PDF] [BIB] [Publisher]
P. Ferrara: Checkmate: a Generic Static Analyzer of Java Multithreaded Programs
Software Engineering and Formal Methods (SEFM), 2009.[PDF] [BIB] [Publisher]
Arsenii Rudich and Peter Müller: Using stereotypes to verify complex heap structures in regional logic
Technical Report, ETH Zurich 2009.[PDF] [BIB]
Werner M. Dietl: Universe Types: Topology, Encapsulation, Genericity, and Tools
Ph.D. Thesis, 2009.[PDF] [BIB]
\'Adám Darvas: Reasoning About Data Abstraction in Contract Languages
Ph.D. Thesis, 2009.[PDF] [BIB]
K. R. M. Leino, P. Müller, and J. Smans: Verification of Concurrent Programs with Chalice
Foundations of Security Analysis and Design~V, 2009.[PDF] [BIB] [Publisher]
A. J. Summers, S. Drossopoulou, and P. Müller: The Need for Flexible Object Invariants
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2009.[PDF] [BIB]
A. J. Summers, S. Drossopoulou, and P. Müller: Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods
Journal of Object Technology (JOT), 2009.[PDF] [BIB] [Publisher]
K. R. M. Leino and P. Müller: A Basis for Verifying Multi-Threaded Programs
European Symposium on Programming (ESOP), 2009.[PDF] [BIB] [Publisher]
M. Nordio, C. Calcagno, P. Müller, and B. Meyer: A Sound and Complete Program Logic for Eiffel
TOOLS-EUROPE, 2009.[PDF] [BIB] [Publisher]
M. Nordio, C. Calcagno, P. Müller, and B. Meyer: Soundness and Completeness of a Program Logic for Eiffel
Technical Report, ETH Zurich 2009.[PDF] [BIB]
M. Nordio, C. Calcagno, B. Meyer, and P. Müller: Reasoning about Function Objects
Technical Report, ETH Zurich 2009.[PDF] [BIB]
Peter Müller and Joseph N. Ruskiewicz: A Modular Verification Methodology for C\# Delegates
Rigorous Methods for Software Construction and Analysis, Essays Dedicated to Egon B\"orger on the Occasion of His 60th Birthday, 2009.[PDF] [BIB] [Publisher]
2008
D. Clarke, S. Drossopoulou, P. Müller, J. Noble, and T. Wrigstad: Aliasing, Confinement, and Ownership in Object-Oriented Programming (IWACO)
Object-Oriented Technology. ECOOP~2008 Workshop Reader, 2008.[PDF] [BIB] [Publisher]
E. Albert, A. Banerjee, S. Drossopoulou, M. Huisman, A. Igarashi, G. T. Leavens, P. Müller, and T. Wrigstad: Formal Techniques for Java-Like Programs (FTfJP)
Object-Oriented Technology. ECOOP~2008 Workshop Reader, 2008.[PDF] [BIB] [Publisher]
Darvas, \'A. and Müller, P.: Faithful mapping of model classes to mathematical structures
IET Software, 2008.[PDF] [BIB] [Publisher]
Leino, K. R. M., Müller, P., and Wallenburg, A.: Flexible Immutability with Frozen Objects
Verified Software: Theories, Tools, and Experiments (VSTTE), 2008.[PDF] [BIB] [Publisher]
D. Cunningham, W. Dietl, S. Drossopoulou, A. Francalanza, P. Müller, and A. J. Summers: Universe Types for Topology and Encapsulation
Formal Methods for Components and Objects (FMCO), 2008.[PDF] [BIB] [Publisher]
A. J. Summers, S. Drossopoulou, and P. Müller: A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods
Formal Techniques for Java-like Programs, 2008.[PDF] [BIB]
\'A. Darvas, F. Mehta, and A. Rudich: Efficient Well-Definedness Checking
International Joint Conference on Automated Reasoning (IJCAR), 2008.[PDF] [BIB] [Publisher]
S. Drossopoulou, A. Francalanza, P. Müller, and A. J. Summers: A Unified Framework for Verification Techniques for Object Invariants
European Conference on Object-Oriented Programming (ECOOP), 2008.[PDF] [BIB] [Publisher]
Nordio, M., Müller, P., and Meyer, B.: Proof-Transforming Compilation of Eiffel Programs
TOOLS-EUROPE, 2008.[PDF] [BIB] [Publisher]
A. Rudich, \'A. Darvas, and Müller, P.: Checking Well-Formedness of Pure-Method Specifications
Formal Methods (FM), 2008.[PDF] [BIB] [Publisher]
A. Rudich, \'A. Darvas, and Müller, P.: Checking Well-Formedness of Pure-Method Specifications (Full Paper)
Technical Report, ETH Zurich 2008.[PDF] [BIB]
Leino, K. R. M. and Müller, P.: Verification of Equivalent-Results Methods
European Symposium on Programming (ESOP), 2008.[PDF] [BIB] [Publisher]
M. Nordio, P. Müller, and B. Meyer: Formalizing Proof-Transforming Compilation of Eiffel Programs
Technical Report, ETH Zurich 2008.[PDF] [BIB] Isabelle formalization
S. Drossopoulou, A. Francalanza, and P. Müller: A Unified Framework for Verification Techniques for Object Invariants
Foundations of Object-Oriented Languages (FOOL), 2008.[PDF] [BIB] [Publisher]
W. Dietl and P. Müller: Ownership Type Systems and Dependent Classes
Foundations of Object-Oriented Languages (FOOL), 2008.[PDF] [BIB]
2007
N. G. Fruja and P. Müller: Translating Invariant Proofs between Spec\# and JML
Technical Report, ETH Zurich 2007.[PDF] [BIB]
P. Müller and A. Rudich: Ownership Transfer in Universe Types
Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2007.[PDF] [BIB] [Publisher]
B. Jacobs, P. Müller, and F. Piessens: Sound reasoning about unchecked exceptions
Software Engineering and Formal Methods (SEFM), 2007.[PDF] [BIB] [Publisher]
P. Müller and M. Nordio: Proof-Transforming Compilation of Programs with Abrupt Termination
Specification and Verification of Component-Based Systems (SAVCBS), 2007.[PDF] [BIB] [Publisher]
\'A. Darvas and P. Müller: Faithful mapping of model classes to mathematical structures
Specification and Verification of Component-Based Systems (SAVCBS), 2007.[PDF] [BIB] [Publisher]
W. Dietl and P. Müller: Runtime Universe Type Inference
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2007.[PDF] [BIB] [Publisher]
W. Dietl and P. Müller: 2007 State of the Universe Address
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2007.[PDF] [BIB] [Publisher]
P. Müller and M. Nordio: Proof-Transforming Compilation of Programs with Abrupt Termination
Technical Report, ETH Zurich 2007.[PDF] [BIB]
P. Müller and A. Rudich: Formalization of Ownership Transfer in Universe Types
Technical Report, ETH Zurich 2007.[PDF] [BIB] Link
W. Dietl, S. Drossopoulou, and P. Müller: Generic Universe Types
European Conference on Object-Oriented Programming
(ECOOP), 2007.[PDF] [BIB] [Publisher]
G. T. Leavens and P. Müller: Information Hiding and Visibility in Interface Specifications
International Conference on Software Engineering (ICSE), 2007.[PDF] [BIB] [Publisher]
\'A. Darvas and K. R. M. Leino: Practical reasoning about invocations and implementations of pure methods
Fundamental Approaches to Software Engineering (FASE), 2007.[PDF] [BIB] [Publisher]
G. T. Leavens, K. R. M. Leino, and P. Müller: Specification and verification challenges for sequential object-oriented programs
Formal Aspects of Computing, 2007.[PDF] [BIB] [Publisher]
Müller, P.: Reasoning about Object Structures Using Ownership
Verified Software: Theories, Tools, Experiments, 2007.[PDF] [BIB] [Publisher]
Darvas, \'A. and Müller, P.: Formal encoding of JML Level 0 specifications in \sc Jive
Technical Report, Software Engineering 2007, ETH Zurich 2007.[PDF] [BIB]
W. Dietl, S. Drossopoulou, and P. Müller: Generic Universe Types
Foundations and Developments of Object-Oriented Languages (FOOL/WOOD '07), 2007.[PDF] [BIB] [Publisher]
H. Lehner and P. Müller: Formal Translation of Bytecode into BoogiePL
Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE), 2007.[PDF] [BIB]
2006
W. Dietl, S. Drossopoulou, and P. Müller: Formalization of Generic Universe Types
Technical Report, ETH Zurich 2006.[PDF] [BIB] Link
Müller, P., Poetzsch-Heffter, A., and Leavens, G. T.: Modular Invariants for Layered Object Structures
Science of Computer Programming, 2006.[PDF] [BIB]
Bannwart, F. and Müller, P.: Changing Programs Correctly: Refactoring with Specifications
Formal Methods (FM), 2006.[PDF] [BIB] [Publisher]
Grolimund, D. and Müller, P.: A Pattern Language for Overlay Networks in Peer-to-Peer Systems
European Conference on Pattern Languages of Programs (EuroPLoP), 2006.[PDF] [BIB]
Darvas, \'A. and Müller, P.: Reasoning About Method Calls in Interface Specifications
Journal of Object Technology (JOT), 2006. [BIB] [Publisher]
Leino, K. R. M. and Müller, P.: A verification methodology for model fields
European Symposium on Programming (ESOP), 2006.[PDF] [BIB] [Publisher]
2005
Leino, K. R. M. and Müller, P.: Modular verification of static class invariants
Formal Methods (FM), 2005.[PDF] [BIB] [Publisher]
Dietl, W. and Müller, P.: Universes: Lightweight Ownership for JML
Journal of Object Technology (JOT), 2005. [BIB] [Publisher]
F. Y. Bannwart and P. Müller: A Logic for Bytecode
Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE), 2005.[PDF] [BIB] Publisher
Darvas, \'A. and Müller, P.: Reasoning About Method Calls in JML Specifications
Formal Techniques for Java-like Programs, 2005.[PDF] [BIB]
2004
Leino, K. R. M. and Müller, P.: Object Invariants in Dynamic Contexts
European Conference on Object-Oriented Programming
(ECOOP), 2004.[PDF] [BIB] [Publisher]
Dietl, W., Müller, P., and Poetzsch-Heffter, A.: A Type System for Checking Applet Isolation in Java Card
Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS), 2004.[PDF] [BIB] [Publisher]
Leino, K. R. M. and Müller, P.: Modular verification of global module invariants in
object-oriented programs
Technical Report, ETH Zurich 2004.[PDF] [BIB] Link
Müller, P., Poetzsch-Heffter, A., and Leavens, G. T.: Modular Invariants for Layered Object Structures
Technical Report, Department of Computer Science, ETH Zurich 2004.[PDF] [BIB]
F. Y. Bannwart and P. Müller: A Logic for Bytecode
Technical Report, ETH Zurich 2004.[PDF] [BIB] Link
Dietl, W. and Müller, P.: Exceptions in Ownership Type Systems
Formal Techniques for Java-like Programs, 2004.[PDF] [BIB]
A. Coglio, M. Huisman, J. Kiniry, P. Müller, and E. Poll: Formal Techniques for Java-Like Programs (FTfJP)
Object-Oriented Technology. ECOOP~2004 Workshop Reader, 2005.[PDF] [BIB] [Publisher]
Eisenbach, S., Leavens, G. T., Müller, P., Poetzsch-Heffter, A., and Poll, E.: Formal Techniques for Java-like Programs
Object-Oriented Technology. ECOOP'03 Workshop Reader, 2004. [BIB] [Publisher]
2003
Müller, P., Poetzsch-Heffter, A., and Leavens, G. T.: Modular Specification of Frame Properties in JML
Concurrency and Computation: Practice and
Experience, 2003.[PDF] [BIB] Link
2002
Müller, P.: Modular Specification and Verification of
Object-Oriented Programs
2002.[PDF] [BIB] [Publisher]
2001
Müller, P., Poetzsch-Heffter, A., and Leavens, G. T.: Modular Specification of Frame Properties in JML
Formal Techniques for Java Programs, 2001.[PDF] [BIB] [Publisher]
Müller, P. and Poetzsch-Heffter, A.: A Type System for Checking Applet Isolation in
Java Card
Formal Techniques for Java Programs, 2001.[PDF] [BIB]
Müller, P. and Poetzsch-Heffter, A.: Universes: A Type System for Alias and Dependency
Control
Technical Report, Fernuniversit\"at Hagen 2001.[PDF] [BIB]
Müller, P.: Modular Specification and Verification of
Object-Oriented Programs
Ph.D. Thesis, 2001.[PDF] [BIB]
2000
Müller, P. and Poetzsch-Heffter, A.: Modular Specification and Verification Techniques
for Object-Oriented Software Components
Foundations of Component-Based Systems, 2000.[PDF] [BIB]
Müller, P. and Poetzsch-Heffter, A.: A Type System for Controlling Representation
Exposure in Java
Formal Techniques for Java Programs, 2000.[PDF] [BIB] Link
Meyer, J., Müller, P., and Poetzsch-Heffter, A.: The \sc Jive System---Implementation Description
2000.[PDF] [BIB] Link
Labeth, M., Meyer, J., Müller, P., and Poetzsch-Heffter, A.: Formal Verification of a Doubly Linked List
Implementation: A Case Study Using the \sc Jive System
Technical Report, Fernuniversit\"at Hagen 2000.[PDF] [BIB] Link
Drossopoulou, S., Eisenbach, S., Jacobs, B., Leavens, G. T., Müller, P., and Poetzsch-Heffter, A.: Formal Techniques for Java Programs
Object-Oriented Technology. ECOOP~2000 Workshop Reader, 2000. [BIB] [Publisher]
1999
Poetzsch-Heffter, A. and Müller, P.: A Programming Logic for Sequential Java
European Symposium on Programming Languages and Systems (ESOP) , 1999.[PDF] [BIB] [Publisher]
Müller, P. and Poetzsch-Heffter, A.: Alias Control is Crucial for Modular Verification
Object-Oriented Technology. ECOOP'99 Workshop Reader, 1999. [BIB] [Publisher]
Müller, P. and Poetzsch-Heffter, A.: Universes: A Type System for Controlling Representation Exposure
Programming Languages and Fundamentals of Programming, 1999.[PDF] [BIB] Link
Müller, P., Meyer, J., and Poetzsch-Heffter, A.: Making Executable Interface Specifications More Expressive
Java-Informations-Tage (JIT), 1999.[PDF] [BIB] [Publisher]
Jacobs, B., Leavens, G. T., Müller, P., and Poetzsch-Heffter, A.: Formal Techniques for Java Programs
Object-Oriented Technology. ECOOP'99 Workshop Reader, 1999. [BIB] [Publisher]
1998
Poetzsch-Heffter, A. and Müller, P.: Logical Foundations for Typed Object-Oriented
Languages
Programming Concepts and Methods (PROCOMET) , 1998.[PDF] [BIB]
Müller, P. and Poetzsch-Heffter, A.: Kapselung und Methodenbindung: Javas Designprobleme und ihre Korrektur
Java-Informations-Tage (JIT), 1998.[PDF] [BIB] [Publisher]
1997
Müller, P. and Poetzsch-Heffter, A.: Formal Specification Techniques for Object-Oriented Programs
Informatik~97: Informatik als Innovationsmotor, 1997.[PDF] [BIB] [Publisher]
Müller, P. and Poetzsch-Heffter, A.: Developing Provably Correct Programs From Object-Oriented Components
Foundations of Component-Based Systems, 1997. [BIB] Link
Poetzsch-Heffter, A. and Müller, P.: A Logic for the Verification of Object-Oriented Programs
Programming Languages and Fundamentals of Programming, 1997. [BIB]
Müller, P. and Poetzsch-Heffter, A.: Preserving the Correctness of Object-Oriented
Programs under Extension
Programming Languages and Fundamentals of
Programming, 1997.[PDF] [BIB]
Müller, P., Meyer, J., and Poetzsch-Heffter, A.: Programming and Interface Specification Language of
\sc Jive---Specification and Design Rationale
Technical Report, Fernuniversit\"at Hagen 1997.[PDF] [BIB]
1996
Müller, P. and Poetzsch-Heffter, A.: A Brief Study in Automating Proofs Based on a
Refined Hoare-logic
Technical Report, Technische Universit\"at M\"unchen 1996.[PDF] [BIB]
1995