Publications

2012

• Hatcliff, J. and Leavens, G. T. and Leino, K. R. M. and Müller, P. and Parkinson, M.: Behavioral Interface Specification Languages
  Computing Surveys, 2012. To appear. [PDF] [BIB]

• I. T. Kassios and 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] Springer-Online

• M. Zanioli and P. Ferrara and A. Cortesi: SAILS: static analysis of information leakage with Sample
  ACM Symposium on Applied Computing (SAC), 2012. [PDF] [BIB]

• P. Ferrara and P. Müller: Automatic inference of access permissions
  Verification, Model Checking, and Abstract Interpretation (VMCAI), 2012. [PDF] [BIB] Springer-Online

2011

• W. Dietl and S. Drossopoulou and P. Müller: Separating ownership topology and encapsulation with generic universe types
  ACM Trans. Program. Lang. Syst., 2011. [PDF] [BIB]

• Hermann 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]

• I. T. Kassios: Dynamic Frames and Automated Verification
  2011. Tutorial for the 2nd COST Action IC0701 Training School, Limerick 6/11, Ireland. [PDF] [BIB]

• G. Costantini and P. Ferrara and A. Cortesi: Static Analysis of String Values
  International Conference on Formal Engineering Methods (ICFEM), 2011. [PDF] [BIB] Springer-Online

• S. Heule and K. R. M. Leino and P. Müller and A. J. Summers: Fractional Permissions Without the Fractions
  Formal Techniques for Java-like Programs (FTfJP), 2011. [PDF] [BIB]

• W. Dietl and M. Ernst and P. Müller: Tunable Static Inference for Generic Universe Types
  European Conference on Object-Oriented Programming (ECOOP), 2011. [PDF] [BIB] Springer-Online

• P. Müller and J. N. Ruskiewicz: Using Debuggers to Understand Failed Verification Attempts
  Formal Methods (FM), 2011. [PDF] [BIB] Springer-Online

• V. Klebanov and P. Müller and N. Shankar and G. T. Leavens and V. Wüstholz and E. Alkassar and R. Arthan and D. Bronish and R. Chapman and E. Cohen and M. Hillebrand and B. Jacobs and K. R. M. Leino and R. Monahan and F. Piessens and N. Polikarpova and T. Ridge and J. Smans and S. Tobies and T. Tuerk and M. Ulbrich and B. Weiss: The 1st Verified Software Competition: Experience Report
  Formal Methods (FM), 2011. [PDF] [BIB] Springer-Online

• 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]

• 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] Springer Online

• M. Barnett and M. Fähndrich and K. R. M. Leino and P. Müller and W. Schulte and H. Venter: Specification and Verification: The Spec# Experience
  Communications of the ACM, 2011. [PDF] [BIB]

2010

• R. Joshi and T. Margaria and P. Müller and D. Naumann and H. Yang: VSTTE 2010 Workshop Proceedings
  Technical Report, ETH Zurich, 2010. [PDF] [BIB]

• M. Nordio and C. Calcagno and B. Meyer and P. Müller and J. Tschannen: Reasoning about Function Objects
  TOOLS-EUROPE, 2010. [PDF] [BIB] Springer-Online

• P. Ferrara: Static Type Analysis of Pattern Matching by Abstract Interpretation
  Formal Techniques for Distributed Systems (FMOODS/FORTE), 2010. [PDF] [BIB] Springer-Online

• W. Dietl and 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]

• K. R. M. Leino and P. Müller and J. Smans: Deadlock-free Channels and Locks
  European Symposium on Programming (ESOP), 2010. [PDF] [BIB] Springer-Online

• K. R. M. Leino and P. Müller and J. Smans: Deadlock-free Channels and Locks
  Technical Report, Department of Computer Science, K.U.Leuven, 2010. Extended version of the ESOP 2010 paper. [PDF] [BIB]

• H. Lehner and P. Müller: Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups
  Fundamental Approaches to Software Engineering (FASE), 2010. [PDF] [BIB] Springer-Online

• Á. Darvas and P. Müller: Proving Consistency and Completeness of Model Classes Using Theory Interpretation
  Fundamental Approaches to Software Engineering (FASE), 2010. [PDF] [BIB] Springer-Online

• T. A. Henzinger and T. Hottelier and L. Kovacs and A. Voronkov: Invariant and Type Inference for Matrices
  Verification, Model Checking, and Abstract Interpretation (VMCAI), 2010. [PDF] [BIB] Springer-Online

• A. J. Summers and S. Drossopoulou: Considerate Reasoning and the Composite Design Pattern
  Verification, Model Checking, and Abstract Interpretation (VMCAI), 2010. [PDF] [BIB] Springer-Online

• 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] Springer-Online

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] Springer-Online

• P. Ferrara: Checkmate: a Generic Static Analyzer of Java Multithreaded Programs
  Software Engineering and Formal Methods (SEFM), 2009. [PDF] [BIB]

• 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]

• Ádám Darvas: Reasoning About Data Abstraction in Contract Languages
  Ph.D. Thesis, 2009. [PDF] [BIB]

• K. R. M. Leino and P. Müller and J. Smans: Verification of Concurrent Programs with Chalice
  Foundations of Security Analysis and Design V, 2009. [PDF] [BIB] Springer-Online

• A. J. Summers and 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 and 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]

• K. R. M. Leino and P. Müller: A Basis for Verifying Multi-Threaded Programs
  European Symposium on Programming (ESOP), 2009. [PDF] [BIB] Springer-Online

• M. Nordio and C. Calcagno and P. Müller and B. Meyer: A Sound and Complete Program Logic for Eiffel
  TOOLS-EUROPE, 2009. [PDF] [BIB] Springer-Online

• M. Nordio and C. Calcagno and P. Müller and B. Meyer: Soundness and Completeness of a Program Logic for Eiffel
  Technical Report, ETH Zurich, 2009. [PDF] [BIB]

• M. Nordio and C. Calcagno and B. Meyer and P. Müller: Reasoning about Function Objects
  Technical Report, ETH Zurich, 2009. [PDF] [BIB]

2008

• D. Clarke and S. Drossopoulou and P. Müller and J. Noble and T. Wrigstad: Aliasing, Confinement, and Ownership in Object-Oriented Programming (IWACO)
  Object-Oriented Technology. ECOOP 2008 Workshop Reader, 2008. [PDF] [BIB] Springer-Online

• E. Albert and A. Banerjee and S. Drossopoulou and M. Huisman and A. Igarashi and G. T. Leavens and P. Müller and T. Wrigstad: Formal Techniques for Java-Like Programs (FTfJP)
  Object-Oriented Technology. ECOOP 2008 Workshop Reader, 2008. [PDF] [BIB] Springer-Online

• Darvas, Á. and Müller, P.: Faithful mapping of model classes to mathematical structures
  IET Software, 2008. [PDF] [BIB]

• Leino, K. R. M. and Müller, P. and Wallenburg, A.: Flexible Immutability with Frozen Objects
  Verified Software: Theories, Tools, and Experiments (VSTTE), 2008. [PDF] [BIB] Springer-Online

• D. Cunningham and W. Dietl and S. Drossopoulou and A. Francalanza and P. Müller and A. J. Summers: Universe Types for Topology and Encapsulation
  Formal Methods for Components and Objects (FMCO), 2008. [PDF] [BIB] Springer-Online

• A. J. Summers and 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]

• Á. Darvas and F. Mehta and A. Rudich: Efficient Well-Definedness Checking
  International Joint Conference on Automated Reasoning (IJCAR), 2008. [PDF] [BIB] Springer-Online

• S. Drossopoulou and A. Francalanza and 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] Springer-Online

• Nordio, M. and Müller, P. and Meyer, B.: Proof-Transforming Compilation of Eiffel Programs
  TOOLS-EUROPE, 2008. [PDF] [BIB] Springer-Online

• A. Rudich and Á. Darvas and Müller, P.: Checking Well-Formedness of Pure-Method Specifications
  Formal Methods (FM), 2008. [PDF] [BIB] Springer-Online

• A. Rudich and Á. 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] Springer-Online

• M. Nordio and P. Müller and B. Meyer: Formalizing Proof-Transforming Compilation of Eiffel Programs
  Technical Report, ETH Zurich, 2008. [PDF] [BIB] Isabelle formalization

• S. Drossopoulou and A. Francalanza and P. Müller: A Unified Framework for Verification Techniques for Object Invariants
  Foundations of Object-Oriented Languages (FOOL), 2008. [PDF] [BIB]

• 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]

• B. Jacobs and P. Müller and F. Piessens: Sound reasoning about unchecked exceptions
  Software Engineering and Formal Methods (SEFM), 2007. [PDF] [BIB]

• 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]

• Á. Darvas and P. Müller: Faithful mapping of model classes to mathematical structures
  Specification and Verification of Component-Based Systems (SAVCBS), 2007. [PDF] [BIB]

• 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] IWACO Website

• 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] IWACO Website

• 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]

• W. Dietl and S. Drossopoulou and P. Müller: Generic Universe Types
  European Conference on Object-Oriented Programming (ECOOP), 2007. [PDF] [BIB] Springer-Online

• G. T. Leavens and P. Müller: Information Hiding and Visibility in Interface Specifications
  International Conference on Software Engineering (ICSE), 2007. [PDF] [BIB]

• Ádám Darvas and K. Rustan M. Leino: Practical reasoning about invocations and implementations of pure methods
  Fundamental Approaches to Software Engineering (FASE), 2007. [PDF] [BIB] Springer-Online

• G. T. Leavens and K. R. M. Leino and P. Müller: Specification and verification challenges for sequential object-oriented programs
  Formal Aspects of Computing, 2007. [PDF] [BIB] Springer-Online

• Müller, P.: Reasoning about Object Structures Using Ownership
  Verified Software: Theories, Tools, Experiments, 2007. [PDF] [BIB] Springer-Online

• Darvas, Á. and Müller, P.: Formal encoding of JML Level 0 specifications in Jive
  Technical Report, Software Engineering 2007, ETH Zurich, 2007. Annual Report of the Chair of Software Engineering. 17 pages. [PDF] [BIB]

• W. Dietl and S. Drossopoulou and P. Müller: Generic Universe Types
  Foundations and Developments of Object-Oriented Languages (FOOL/WOOD '07), 2007. [PDF] [BIB]

• 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 and S. Drossopoulou and P. Müller: Formalization of Generic Universe Types
  Technical Report, ETH Zurich, 2006. [PDF] [BIB]

• Müller, P. and 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] Springer-Online

• 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, Á. and Müller, P.: Reasoning About Method Calls in Interface Specifications
  Journal of Object Technology (JOT), 2006. [BIB] JOT-Online

• Leino, K. R. M. and Müller, P.: A verification methodology for model fields
  European Symposium on Programming (ESOP), 2006. [PDF] [BIB] Springer-Online

2005

• Leino, K. R. M. and Müller, P.: Modular verification of static class invariants
  Formal Methods (FM), 2005. [PDF] [BIB] Springer-Online

• Dietl, W. and Müller, P.: Universes: Lightweight Ownership for JML
  Journal of Object Technology (JOT), 2005. [BIB] JOT-Online

• F. Y. Bannwart and P. Müller: A Logic for Bytecode
  Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE), 2005. [PDF] [BIB]

• Darvas, Á. and Müller, P.: Reasoning About Method Calls in JML Specifications
  Formal Techniques for Java-like Programs, 2005. [PDF] [BIB]

• A. Coglio and M. Huisman and J. Kiniry and P. Müller and E. Poll: Formal Techniques for Java-Like Programs (FTfJP)
  Object-Oriented Technology. ECOOP 2004 Workshop Reader, 2005. [PDF] [BIB] Springer-Online

2004

• Leino, K. R. M. and Müller, P.: Object Invariants in Dynamic Contexts
  European Conference on Object-Oriented Programming (ECOOP), 2004. [PDF] [BIB] Springer-Online

• Dietl, W. and 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] Springer-Online

• 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]

• Müller, P. and 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]

• Dietl, W. and Müller, P.: Exceptions in Ownership Type Systems
  Formal Techniques for Java-like Programs, 2004. [PDF] [BIB]

• Eisenbach, S. and Leavens, G. T. and Müller, P. and Poetzsch-Heffter, A. and Poll, E.: Formal Techniques for Java-like Programs
  Object-Oriented Technology. ECOOP'03 Workshop Reader, 2004. [BIB] Springer-Online

2003

• Müller, P. and Poetzsch-Heffter, A. and Leavens, G. T.: Modular Specification of Frame Properties in JML
  Concurrency and Computation: Practice and Experience, 2003. [PDF] [BIB]

2002

• Müller, P.: Modular Specification and Verification of Object-Oriented Programs
  2002. [PDF] [BIB] Springer-Online

2001

• Müller, P. and Poetzsch-Heffter, A. and Leavens, G. T.: Modular Specification of Frame Properties in JML
  Formal Techniques for Java Programs, 2001. [PDF] [BIB]

• 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ät 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]

• Meyer, J. and Müller, P. and Poetzsch-Heffter, A.: The Jive System-Implementation Description
  2000. [PDF] [BIB]

• Labeth, M. and Meyer, J. and Müller, P. and Poetzsch-Heffter, A.: Formal Verification of a Doubly Linked List Implementation: A Case Study Using the Jive System
  Technical Report, Fernuniversität Hagen, 2000. [PDF] [BIB]

• Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and Müller, P. and Poetzsch-Heffter, A.: Formal Techniques for Java Programs
  Object-Oriented Technology. ECOOP 2000 Workshop Reader, 2000. [BIB] Springer-Online

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] Springer-Online

• Müller, P. and Poetzsch-Heffter, A.: Alias Control is Crucial for Modular Verification
  Object-Oriented Technology. ECOOP'99 Workshop Reader, 1999. [BIB] Springer-Online

• Müller, P. and Poetzsch-Heffter, A.: Universes: A Type System for Controlling Representation Exposure
  Programming Languages and Fundamentals of Programming, 1999. Technical Report 263. [PDF] [BIB]

• Müller, P. and Meyer, J. and Poetzsch-Heffter, A.: Making Executable Interface Specifications More Expressive
  Java-Informations-Tage (JIT), 1999. [PDF] [BIB]

• Jacobs, B. and Leavens, G. T. and Müller, P. and Poetzsch-Heffter, A.: Formal Techniques for Java Programs
  Object-Oriented Technology. ECOOP'99 Workshop Reader, 1999. [BIB] Springer-Online

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. (in German) . [PDF] [BIB]

1997

• Müller, P. and Poetzsch-Heffter, A. : Formal Specification Techniques for Object-Oriented Programs
  Informatik 97: Informatik als Innovationsmotor, 1997. [PDF] [BIB]

• Müller, P. and Poetzsch-Heffter, A. : Developing Provably Correct Programs From Object-Oriented Components
  Foundations of Component-Based Systems, 1997. [BIB]

• Poetzsch-Heffter, A. and Müller, P.: A Logic for the Verification of Object-Oriented Programs
  Programming Languages and Fundamentals of Programming, 1997. Technical Report 9717. [BIB]

• Müller, P. and Poetzsch-Heffter, A. : Preserving the Correctness of Object-Oriented Programs under Extension
  Programming Languages and Fundamentals of Programming, 1997. Technical Report 9717. [PDF] [BIB]

• Müller, P. and Meyer, J. and Poetzsch-Heffter, A.: Programming and Interface Specification Language of Jive-Specification and Design Rationale
  Technical Report, Fernuniversität 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ät München, 1996. [PDF] [BIB]

1995

• Müller, P. : Specification and Implementation of an Annotation Language for an Object-Oriented Programming Language
  Masters Thesis, 1995. (In German) . [PDF] [BIB]