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

Protocols to Code: Formal Verification of a Secure 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

CCS 2025, PDF, Artifact
Distinguished Artifact Award
Modular Reasoning about Global Variables and Their Initialization

João C. Pereira, Isaac van Bakel, Patricia Firlejczyk, Marco Eilers, Peter Müller

OOPSLA 2025, PDF, Artifact, Presentation (by Marco)
A Refinement Methodology for Distributed Programs in Rust

Aurea Bílá, João C. Pereira, Peter Müller

OOPSLA 2025, PDF, Artifact, Presentation (by Aurea)
Distinguished Artifact Award
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 2021, PDF, Extended Version, Artifact, Presentation (by Linard)
Testing for Race Conditions in Distributed Systems via SMT Solving

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

TAP 2020, 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

Talks

Protocols to Code: Formal verification of a secure next-generation Internet router, CCS, Taipei, October 2025
Verifying programs with global state in separation logic, Swiss Verification Day, Lugano, February 2025
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 (2023, 2022), Teaching assistant (2021)
Formal Methods and Functional Programming
BSc Course, ETH Zurich, Course Website
Teaching assistant (2025, 2023, 2022, 2021)
Laboratórios de Informática III
BSc Course, University of Minho
Teaching assistant (2018)

Supervised Students

Verification of Mutex implmentation from the Go Standard Library,

Axel Montini

Practical Work Project, 2025
A Specification Linter for Gobra

Amos Herz, co-supervised with Salome Brugger

Practical Work Project, 2025, PDF
Analyzing Assumptions with Automated Verification Tools

Andrea Keusch, co-supervised with Salome Brugger

MSc Thesis, 2025, PDF
An empirical assessment of proof strategies in large-scale verification projects

Florian Marek

Summer Fellowship, 2025
Verifying Secure Information Flow for the VerifiedSCION Router

Henri Inndorf

Practical Work Project & Internship, 2025, PDF
Evolving the VerifiedSCION Codebase

Aaron Bojarski

Practical Work Project, 2025
The Gobra Book: Creating a Didactic Online Resource for Gobra

Ali Gottschall

BSc thesis, 2024, PDF
Verifying Parts of the Go Standard Library

Conradin Laux

BSc thesis, 2024, PDF
Translating Cryptographic Code from C to Rust using LLMs

Micha Buri

BSc thesis, 2024
Specifying and Verifying Static Initialization in Deductive Program Verifiers

Patricia Firlejczyk, co-supervised with Marco Eilers

BSc Thesis, 2024, PDF
Verifying the IO Behaviour of the SCION Router

Markus Limbeck, co-supervised with Dionysios Spiliopoulos

Internship & Practical Work Project, 2024, PDF
A Standard Library for Gobra

Daniel Nezamabadi

Practical Work Project, 2024, PDF
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 Aurea 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