We published the PRISM framework

Bertrand Meyer and Reto Weber have published an extended and revised version of the theory of programs, now called PRISM. This work involved a complete rework from the ground up, refining definitions and, most importantly, rigorously proving the claims presented in the paper.

We replaced previously disproven theorems with correct formulations and provided a precise definition of concurrency. Additionally, during our research, we encountered the concept of “Choice Normal Form” (CNF), which proved valuable for establishing various properties and describing numerous behaviors.

I thoroughly enjoyed working on the proofs using Isabelle/HOL and will continue contributing to this project in the future. For more information and updates on PRISM, please visit our designated website.