This tool presents a novel approach to bolstering network protocol verification by integrating the Shadow network simulator with the Ivy formal verification tool to check time properties. Furthermore, it extends Ivy’s capabilities with a dedicated time module, enabling the verification of complex quantitative-time properties.

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

Evrostos: The rLTL Verifier

A formally verified implementation of a bolt-on security device for ICS networks. Designed with TLA+ and written/proved in F*

High-Performance Model Checker developed for multicore, multiprocessors machines (NUMA).

A formally specified UNO game using B-Method

An open-source refinement checker for CSP

Projeto realizado para matéria de Métodos Formais - O programa deve receber um arquivo de entrada que represente a situação inicial de um jogo de sudoku e, à partir dele, gerar uma fórmula lógica para servir de entrada ao programa "zchaff", resolvedor SAT

Tools for dependent variables in Linear Temporal Logic (LTL), including: Finding Dependent variables, Synthesis exploiting dependency. https://arxiv.org/abs/2401.11290

a simple virtual machine for VDM by VDM

Ruler of the Seas is a simulation of a competitive multiplayer table top game. This repository contains the Abstract Machines, Refinements and Implementation of the game.