PV2 Islagenerates a state graph or a test case from an architecture spec

Tool to evaluate relaxed-memory behaviour of instruction set architectures w.r.t. arbitrary axiomatic memory models

Application domain/field

Expected input



License: BSD 2-Clause
Binary level Concurrency


Related papers

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models (CAV '21)

Last publication date

15 July 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.