A Formal Method playground for limboole, Z3, nuXmv, Alloy, and Spectra

A test generator application designed to create performance benchmarks for SymploeoPC

My master thesis on information flow control on a minimal version of the RISC-V architecture with a model checker

transpiler from (a subset of) python to nuXmv

A model designed for an elevator that also checks the constraints and specifications for a finite state machine. Also contains a finite state machine for multiplication.

Transform XML traces generated by nuXmv or NuSMV into a html table

Trabalho 2 de Métodos Formais.

(Unofficial) Python interface to nuXmv

All the exersice from Formal Methods for Software Engineering course @ Bauhaus University Weimar