Proyecto de la asignatura SDG2 - Calidad del aire en un quirófano

A system validation model written in Promela

Model of a concurrent train interlocking system for formal verification

Homework and in-class exercises for CS 511: Concurrent Programming, Fall 2018

Materials for "Mathematical basis of software verification" course of BMSTU Software Engineering last year

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

Model checking with SPIN

Logic in Computer Science 2018/2019

Study for mah thesis

ImSpin is an advanced and modernized version of the classic iSpin frontend, leveraging the power and flexibility of ImGui to provide a superior user experience. Designed as the frontend for the SPIN model checker, ImSpin aims to offer an intuitive, efficient, and visually appealing interface for model checking enthusiasts and professionals.

A coursework on formal methods

Find all(= 92) eight queens answers with Spin/Promela.

Model of a concurrent FIFO queue written in Promela for the Spin model checker

Using PROMELA and SPIN to check the dining philosophers' problem for race conditions.

Distributed computing course projects

Repository for a trash bin control software in SPIN

Моделирование и верификация распределенных алгоритмов с использованием языка Promela и верификатора Spin. Модели алгоритмов решения задачи взаимоисключающего доступа: Алгоритм Деккера, Алгоритм Петерсона, Алгоритм Дейкстра. Модель алгоритма контроллера светофора на сложном перекрестке.

Describing Platooning in the language of MWB (Mobility Workbench), a tool for manipulating and analyzing mobile concurrent systems described in pi-calculus (tool written in standard SML and runs on SML/NJ compiler). Then describing it in Promela to model check using SPIN and Isabelle

📌 The Dining Philosophers Problem / 食事する哲学者の問題