In computer science and software engineering, Alloy is a declarative
specification language for expressing complex structural constraints and
behavior in a software system. Alloy provides a simple structural modeling tool
based on first-order logic. Alloy is targeted at the creation of micro-models
that can then be automatically checked for correctness. Alloy specifications
can be checked using the Alloy Analyzer.
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
A Formal Method playground for limboole, Z3, nuXmv, Alloy, Spectra, Dafny, and more...
railML validation tool
Formal specification for Miniscript in Alloy
Formal Methods Project and Exercises with Alloy (2022 Course)
A debugger for transition systems modelled in Alloy
Z/Alloy formal specification for client identifying data regulation for banks in Switzerland
Some examples and notes while learning Alloy modeling language.
An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications
R&DD project for software engineering 2 course A.Y. 2024-2025
RASD/DD project developed in the course SOFTWARE ENGINEERING 2 of Politecnico di Milano during the academic year 2024/2025. RASD/DD mark: 14/14; Homeworks mark: 6/6.
Verification of Observational Determinism in ROS2-based systems using Alloy.
online exam and justice project
Prácticas en Alloy Modelling Language para Métodos Formales. Contiene modelos de ejercicios, situaciones y sistemas donde se valida su correctitud mediante Alloy Analyzer y model checking.
Especificação formal de uma distribuição de funcionários para a disciplina Lógica para Computação.
Software Verification and Validation - Open Ended Lab Task
Constraint preservation verification for Django database migrations, via Alloy