Dockerfiles everywhere 🐳

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.

Project done for my B.Tech course on Formal Methods for System Verification

Formal Methods in Software Development Project 2019/2020 - Generation of a controller for a game grid with obstacle and goal cell. The controller is generated by interrogating NuSMV as a blackbox and using the output appropriately.

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

Evrostos: The rLTL Verifier

A K8s operator for Mastodon, written in OCaml and model checked by NuSMV.

Creating a model and then verifying it using the NuSMV

Visual path-based counterexample explanation for NuSMV function block diagrams

Solving the classic Ferryman problem via model-checking using NuSMV Modeller

Converter of function block models from NuSMV to Promela (SPIN)

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

Some scripts to learn NuSMV

The aim of this work is create a basic Implementation of "TruDaMul" framework and test it creating simple simulations; using "NuSMV" language.

In this repository you can find all of my projects for Verification of Reactive Systems Course when I was in 2nd semester of my master's at SUT.

NuSMV Examples for Software Model Verification

First project of Specification and Modelation (EM) - using NuSMV to model a landing system

Il presente codice NuSMV modella un sistema RFID composto da 3 tag RFID e un reader RFID. L'obiettivo del sistema è gestire la collisione tra i tag quando più di uno risponde contemporaneamente al reader. Per risolvere questo problema, sono stati utilizzati metodi non deterministici.

Project of Logic discipline (2018.2)