8 citations · 14 across the 4 of their papers we have counts for
7 papers
Automated Proof of Bell-LaPadula Security Properties
Maximiliano Cristia, Gianfranco Rossi
Almost fifty years ago, D.E. Bell and L. LaPadula published the first formal model of a secure system, known today as the Bell-LaPadula (BLP) model. BLP is described as a state mac…
Automated Reasoning with Restricted Intensional Sets
Maximiliano Cristiá, Gianfranco Rossi
Intensional sets, i.e., sets given by a property rather than by enumerating elements, are widely recognized as a key feature to describe complex problems (see, e.g., specification…
Set-Based Models for Cryptocurrency Software
Gustavo Betarte, Maximiliano Cristiá, Carlos Luna +2
Emin Gün Sirer once said: It's clear that writing a robust, secure smart contract requires extreme amounts of diligence. It's more similar to writing code for a nuclear power react…
Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol
Gustavo Betarte, Maximiliano Cristiá, Carlos Luna +2
MimbleWimble is a privacy-oriented cryptocurrency technology encompassing security and scalability properties that distinguish it from other protocols of the kind. In this paper we…
Adding Partial Functions to Constraint Logic Programming with Sets
Maximiliano Cristia, Gianfranco Rossi, Claudia Frydman
Partial functions are common abstractions in formal specification notations such as Z, B and Alloy. Conversely, executable programming languages usually provide little or no suppor…
A Family of Simulation Criteria to Guide DEVS Models Validation Rigorously, Systematically and Semi-Automatically
Diego A. Hollmann, Maximiliano Cristiá, Claudia Frydman
The most common method to validate a DEVS model against the requirements is to simulate it several times under different conditions, with some simulation tool. The behavior of the…
Applying SMT Solvers to the Test Template Framework
Maximiliano Cristiá, Claudia Frydman
The Test Template Framework (TTF) is a model-based testing method for the Z notation. In the TTF, test cases are generated from test specifications, which are predicates written in…