Peter Müller

Dr. rer. nat.

Peter Müller
Dr. rer. nat.; Peter Müller
Nationality	Swiss, German
Alma mater	Technical University of Munich (MSc); University of Hagen (PhD);
	Scientific career
Fields	Formal verification; Programming Languages; Separation logic;
Institutions	ETH Zurich
Thesis	Modular Specification and Verification of Object-Oriented Programs (2001)
Doctoral advisor	Arnd Poetzsch-Heffter
Website	https://www.pm.inf.ethz.ch/people/personal/pmueller-pers.html

Peter Müller is a Swiss computer scientist and professor at ETH Zurich. He has been a Full Professor at the Department of Computer Science and head of the Programming Methodology group since 2008. His research focuses on languages, techniques, and tools for the development of correct software. Notable work includes Viper, an infrastructure for reasoning about the correctness of heap-manipulating programs. Previously, he held positions as Researcher at Microsoft Research in Redmond, Assistant Professor at ETH Zurich, and Project Manager at Deutsche Bank in Frankfurt.

Research[edit]

Peter Müller centers his research on modular specification and verification of heap-manipulating programs. Early work was on Chalice, a programming language and verifier for concurrent programs, which was developed together with K. Rustan M. Leino. Later on, Peter Müller worked on Viper^[1], which got first published in 2016^[2] and is actively maintained and regularly extended. In contrast to Chalice, Viper is an intermediate programming language aimed at verification and a suite of tools to verify Viper programs. By natively providing support for reasoning about mutable state using permissions or ownership (i.e. separation logic), Viper is designed to make it easy to implement verification techniques for sequential and concurrent programs with mutable state. In particular, Viper is used as a backbone in several program verifiers including Gobra^[3] for Go (programming language)|Go, Nagini^[4] for Python (programming language)|Python, Prusti^[5] for Rust (programming language)|Rust, and VerCors for C (programming language)|C and Java (programming language)|Java.

References[edit]

↑ "Viper". Retrieved 11 June 2024.
↑ Müller, Peter; Schwerhoff, Malte; Summers, Alexander J. (2016). Viper: A Verification Infrastructure for Permission-Based Reasoning. Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer-Verlag. pp. 41–62. doi:10.1007/978-3-662-49122-5_2.
↑ Wolf, Felix A.; Arquint, Linard; Clochard, Martin; Oortwijn, Wytse; Pereira, João C.; Müller, Peter (2021). Gobra: Modular Specification and Verification of Go Programs. Computer Aided Verification (CAV). Springer International Publishing. doi:10.1007/978-3-030-81685-8_17.
↑ Eilers, Marco; Müller, Peter (2018). Nagini: A Static Verifier for Python. Computer Aided Verification (CAV). Springer International Publishing. pp. 596–603. doi:10.1007/978-3-319-96145-3_33.
↑ Astrauskas, Vytautas; Müller, Peter; Poli, Federico; Summers, Alexander J. (2019). Leveraging Rust Types for Modular Specification and Verification. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). Association for Computing Machinery. doi:10.1145/3360573.

External links[edit]

Add External links

This article "Peter Müller" is from Wikipedia. The list of its authors can be seen in its historical. Articles taken from Draft Namespace on Wikipedia could be accessed on Wikipedia's Draft Namespace.

[1] "Viper". Retrieved 11 June 2024.

[2] Müller, Peter; Schwerhoff, Malte; Summers, Alexander J. (2016). Viper: A Verification Infrastructure for Permission-Based Reasoning. Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer-Verlag. pp. 41–62. doi:10.1007/978-3-662-49122-5_2.

[3] Wolf, Felix A.; Arquint, Linard; Clochard, Martin; Oortwijn, Wytse; Pereira, João C.; Müller, Peter (2021). Gobra: Modular Specification and Verification of Go Programs. Computer Aided Verification (CAV). Springer International Publishing. doi:10.1007/978-3-030-81685-8_17.

[4] Eilers, Marco; Müller, Peter (2018). Nagini: A Static Verifier for Python. Computer Aided Verification (CAV). Springer International Publishing. pp. 596–603. doi:10.1007/978-3-319-96145-3_33.

[5] Astrauskas, Vytautas; Müller, Peter; Poli, Federico; Summers, Alexander J. (2019). Leveraging Rust Types for Modular Specification and Verification. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). Association for Computing Machinery. doi:10.1145/3360573.

[1]

[2]

[3]

[4]

[5]