Thibault Dardinier and Jonas Fiala won the first prize at the verifyThis 2022 Competition using Viper. Congratulations!
Alexandra Bugariu defended her thesis on Automatically Identifying Soundness and Completeness Errors in Program Analysis Tools
Our two FM papers are now online. We also got two papers accepted at OOPSLA, which will appear shortly!
Our new verifier 2vyper for Etherium smart contracts written in Vyper won a Distinguished Artifact Award at OOPSLA 2021
We released a new stable version of the Viper verification infrastructure in February 2022
A verified security architecture. More
An automated verifier for Python. More
Formal verification of the SCION internet architecture implementation. More
Formal foundations of translational verifiers. More
An automated, modular verifier for Go. More
A verifier for Rust programs. More
A verification infrastructure for permission-based reasoning. More
