This repository serves as the authoritative source for the specification of the ABZ27 Case Study, which focuses on the domain of law.
The Case Study challenges formal methods practitioners to explore possible instantiations of domestic laws implementing the 1961 UN Convention on the Reduction of Statelessness, and to investigate what guarantees they can provide for effectively reducing or eliminating statelessness. The goal is to formally model such laws, specify the expected guarantees, and use formal methods to validate and verify the resulting models and their properties.
Latest version: Specification v1.1
The specification is developed iteratively, and feedback is welcome throughout the preparation of the Case Study.
For clarifications, general questions, identified problems, or suggestions for improvement, please open an issue. Public discussion is encouraged, as it may help clarify the specification for other participants. When possible, indicate the relevant section and provide sufficient context.
Participants are also encouraged to propose new validation scenarios that they consider interesting or challenging and that may provide additional opportunities for modelling, validation, and verification.
Issues are categorized using the following labels:
question— Clarification or interpretation requestproblem— Error, inconsistency, or ambiguity in the specificationsuggestion— Proposed improvement or additionscenario— Proposed new scenario
The Case Study co-chairs will review issues regularly and respond directly in the corresponding issue. Once an issue has been resolved, any resulting changes to the specification will be incorporated, where appropriate, into the next planned release.
Issues may be closed once the question or concern has been addressed. Document releases will be associated with the milestones of the Case Study and will incorporate the relevant changes accumulated since the previous release.
The specification is maintained as a living document throughout the preparation of the Case Study. Each published version is associated with a Git tag and GitHub release, allowing previous versions to be identified and retrieved.
See the Releases page for the complete version history.
Release notes will summarize the main changes introduced in each version and, where applicable, reference the issues that led to those changes.
The ABZ conference brings together researchers and practitioners working on formal methods and their applications. Each edition releases a case study challenge for the application of formal methods, with Statelessness Elimination being the 8th such case study. Case study contributions are presented at the conference and published in the formal proceedings.
