João C. Pereira

Hi, I am João C. Pereira.

I am a PhD student at the Programming Methodology Group at ETH Zurich, supervised by Peter Müller.

In my research, I develop practical program verifiers and verification techniques to verify implementations of distributed systems. I co-develop Gobra, a deductive program verifier for the Go programming language, and I have been using it in the VerifiedSCION project to show the correctness of the official open-source implementation of a critical component of the SCION protocol.

During my PhD, I interned at Microsoft Research. Before this, I obtained an MSc degree in Informatics Engineering from the University of Minho. During my MSc, I interned at the National Institute of Informatics of Japan and at the Automated Reasoning Group at Amazon Web Services.

My publications can be found below and on Google Scholar. Contact details are here.

Publications

Conferences

Gobra: Modular Specification and Verification of Go Programs

Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, João C. Pereira, Peter Müller

CAV'21, PDF, Extended Version, Artifact, Presentation
Testing for Race Conditions in Distributed Systems via SMT Solving

João C. Pereira, Nuno Machado, Jorge Sousa Pinto

TAP'20, PDF

Book Chapters

The Complete Guide to SCION: From Design Principles to Formal Verification
Springer, 2024, Publisher's page
Co-authored chapters:
- Code-Level Verification
  
  Linard Arquint, Peter Müller, Wytse Oortwijn, João C. Pereira, Felix Wolf
  Chapter
- Current Status and Plans
  
  Linard Arquint, David Basin, Tobias Klenze, Si Liu, Peter Müller, João C. Pereira, Christoph Sprenger, Felix Wolf
  Chapter

Preprints

Protocols to Code: Formal Verification of a Next-Generation Internet Router

João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, Adrian Perrig

arXiv, 2024, Preprint
Refinement Proofs in Rust Using Ghost Locks

Aurel Bílý, João C. Pereira, Jan Schär, Peter Müller

arXiv, 2023, Preprint

Talks

Safely translating C to idiomatic Rust using LLMs, End-of-internship talk at Microsoft Research, Redmond, August 2023
Proving Programs Correct with Gobra at Zürich Gophers Meetup, October 2022, Slides, Code Examples
VerifiedSCION: Verified Secure Routing, 2021, Presentation

Teaching

Concepts of Object-Oriented Programming
MSc Course, ETH Zurich, Course Website
Head teaching assistant (AS’23, AS’22), Teaching assistant (AS’21)
Formal Methods and Functional Programming
BSc Course, ETH Zurich, Course Website
Teaching assistant (FS'23, FS'22, FS’21)
Laboratórios de Informática III
BSc Course, University of Minho
Teaching assistant (FS'18)

Supervised Students

Ongoing

Specifying and Verifying Static Initialization in Deductive Program Verifiers

Patricia Firlejczyk, co-supervised with Marco Eilers

BSc Thesis
Verifying the IO Behaviour of the SCION Router

Markus Limbeck, co-supervised with Dionysios Spiliopoulos

Practical Work Project
A Standard Library for Gobra

Daniel Nezamabadi

Practical Work Project

Completed

A Linear Typesystem for a Go Verifier

Liming Han, co-supervised with Felix Wolf

MSc Thesis, 2023, PDF
Translating Pedagogical Verification Exercises to Viper

Benjamin Frei, co-supervised with Nicolas Klose

BSc Thesis, 2023, PDF
Proving Refinement in a Rust Verifier

Jan Schär, co-supervised with Aurel Bílý

MSc Thesis, 2023, PDF
Verifying Go’s Standard Library

Adrian Jenny

Practical Work project, 2022, PDF
Translating Pedagogical Exercises to Viper’s Go Front-end

Timon Egli

BSc Thesis, 2022, PDF
Modularly Verifying and Specifying Initialization Code

Daneshvar Amrollahi

Internship Project, 2022
Specifying and Verifying the IO Behavior of the SCION Border Router

Lino Telschow, co-supervised with Felix Wolf

MSc Thesis, 2021, PDF
Program Verification in Continuous Integration Workflows

Johannes Gasser, co-supervised with Linard Arquint

BSc Thesis, 2021, PDF
Verifying Termination of Go Programs

Cheng Xuan, co-supervised with Linard Arquint

BSc Thesis, 2021, PDF
Cloud-based Verification IDE

Dennis Buitendijk, co-supervised with Linard Arquint

BSc Thesis, 2021, PDF
Verification of Practical Go Programs

Luca Halm, co-supervised with Felix Wolf

BSc Thesis, 2021, PDF