João Pereira's Projects
The Go programming language
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
Github Action to verify Go code with Gobra directly in a CI workflow
Tests for the gobra-action
Standard library for the Gobra verifier for Go. Contains definitions and lemmas useful for verifying large projects.
Source code of Goolong, from "Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs"
An IRConverter from WALA IR to Soot IR (Jimple)
IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
MagpieBridge LSP Framework --- A simple solution for your IDE integration
Fork of minha-benchmarks, a suit of tests for the MINHA framework
A verified version of SCION's go source code
ownCloud network deployment
Examples and exercises from the book Program Proofs translated to Gobra
A tool for transforming Rust code using rules
Code made in high school for my Robotic's team, to participate in National Festival of Robotics 2014
SCION Internet Architecture
Definition of the Viper intermediate verification language.
Automated data race detection from a distributed trace via SMT constraint solving
uMatrix: Point and click matrix to filter net requests according to source, destination and type
A framework for formally verifying distributed systems implementations in Coq
Verifying the SCION architecture using Gobra
Verified Rust for low-level systems code
HTTP server that manages verification requests to different tools from the Viper tool stack.
Slide deck and examples from my talk on Gobra @ Zürich Gophers, 26.10.2022