4 papers
Reusability and Modifiability in Robotics Software (Extended Version)
Laura Pomponio, Maximiliano Cristiá, Estanislao Ruiz Sorazábal +1
We show the design of the software of the microcontroller unit of a weeding robot based on the Process Control architectural style and design patterns. The design consists of 133 m…
From B Specifications to \}$ Forgrams
Maximiliano Cristiá
In this class notes students can learn how B specifications can be translated into \}$ forgrams, how these forgrams can be executed and how they can be proved to verify some…
Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation
Alfredo Capozucca, Maximiliano Cristiá, Ross Horne +1
This paper revisits the Brewer-Nash security policy model inspired by ethical Chinese Wall policies. We draw attention to the fact that write access can be revoked in the Brewer-Na…
Comparing EventB, and Why3 Models of Sparse Sets
Maximiliano Cristiá, Catherine Dubois
Many representations for sets are available in programming languages libraries. The paper focuses on sparse sets used, e.g., in some constraint solvers for representing integer var…