Gianfranco Rossi

Maximiliano Cristiá, Gianfranco Rossi

We encode arrays as functions which, in turn, are encoded as sets of ordered pairs. The set cardinality of each of these functions coincides with the length of the array it is representing. Then we define a fragment of set theory that is used to give the specifications of a non-trivial class of programs with arrays. In this way, array reasoning becomes set reasoning. Furthermore, a decision procedure for this fragment is also provided and implemented as part of the {log} (read 'setlog') tool. {log} is a constraint logic programming language and satisfiability solver where sets and binary relations are first-class citizens. The tool already implements a few decision procedures for different fragments of set theory. In this way, arrays are seamlessly integrated into {log} thus allowing users to reason about sets, functions and arrays all in the same language and with the same solver. The decision procedure presented in this paper is an extension of decision procedures defined in earlier works not supporting arrays.

Maximiliano Cristiá, Alfredo Capozucca, Gianfranco Rossi

{log} (read 'setlog') was born as a Constraint Logic Programming (CLP) language where sets and binary relations are first-class citizens, thus fostering set programming. Internally, {log} is a constraint satisfiability solver implementing decision procedures for several fragments of set theory. Hence, {log} can be used as a declarative, set, logic programming language and as an automated theorem prover for set theory. Over time {log} has been extended with some components integrated to the satisfiability solver thus providing a formal verification environment. In this paper we make a comprehensive presentation of this environment which includes a language for the description of state machines based on set theory, an interactive environment for the execution of functional scenarios over state machines, a generator of verification conditions for state machines, automated verification of state machines, and test case generation. State machines are both, programs and specifications; exactly the same code works as a program and as its specification. In this way, with a few additions, a CLP language turned into a seamlessly integrated programming and automated proof system.

Maximiliano Cristiá, Gianfranco Rossi

In this paper we show how $\{log\}$ (read `setlog'), a Constraint Logic Programming (CLP) language based on set theory, can be used as an automated verifier for B specifications. In particular we encode in $\{log\}$ an Event-B specification, developed by Mammar and Laleau, of the case study known as the Landing Gear System (LGS). Next we use $\{log\}$ to discharge all the proof obligations proposed in the Event-B specification by the Rodin platform. In this way, the $\{log\}$ program can be regarded as an automatically verified prototype of the LGS. We believe this case study provides empirical evidence on how CLP and set theory can be used in tandem as a vehicle for program verification.

Maximiliano Cristiá, Gianfranco Rossi

In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints ($\mathcal{L}_{\lvert\cdot\rvert}$) to a decision procedure for $\mathcal{L}_{\lvert\cdot\rvert}$ extended with set terms denoting finite integer intervals ($\mathcal{L}_{[\,]}$). In $\mathcal{L}_{[\,]}$ interval limits can be integer linear terms including \emph{unbounded variables}. These intervals are a useful extension because they allow to express non-trivial set operators such as the minimum and maximum of a set, still in a quantifier-free logic. Hence, by providing a decision procedure for $\mathcal{L}_{[\,]}$ it is possible to automatically reason about a new class of quantifier-free formulas. The decision procedure is implemented as part of the $\{log\}$ tool. The paper includes a case study based on the elevator algorithm showing that $\{log\}$ can automatically discharge all its invariance lemmas some of which involve intervals.

Maximiliano Cristiá, Gianfranco Rossi

$\{log\}$ is a programming language at the intersection of Constraint Logic Programming, set programming and declarative programming. But $\{log\}$ is also a satisfiability solver for a theory of finite sets and finite binary relations. With $\{log\}$ programmers can write abstract programs using all the power of set theory and binary relations. These programs are not very efficient but they are very close to specifications. Then, their correctness is more evident. Furthermore, $\{log\}$ programs are also set formulas. Hence, programmers can use $\{log\}$ again to automatically prove their programs verify non trivial properties. In this paper we show this development methodology by means of several examples.

Maximiliano Cristiá, Gianfranco Rossi

This document shows how Z specifications can be translated into $\{log\}$ and, later, on how $\{log\}$ can be used to run simulations and automated proofs. This can help users of other specification languages such as B and VDM to use $\{log\}$ along the same lines. The presentation is rather informal and user-oriented. More technical and formal presentations can be found in the papers published by the authors. We also assume the reader has at least a basic knowledge of the Z notation.

Maximiliano Cristiá, Gianfranco Rossi

The Tokeneer project was an initiative set forth by the National Security Agency (NSA, USA) to be used as a demonstration that developing highly secure systems can be made by applying rigorous methods in a cost effective manner. Altran Praxis (UK) was selected by NSA to carry out the development of the Tokeneer ID Station. The company wrote a Z specification later implemented in the SPARK Ada programming language, which was verified using the SPARK Examiner toolset. In this paper, we show that the Z specification can be easily and naturally encoded in the {log} set constraint language, thus generating a functional prototype. Furthermore, we show that {log}'s automated proving capabilities can discharge all the proof obligations concerning state invariants as well as important security properties. As a consequence, the prototype can be regarded as correct with respect to the verified properties. This provides empirical evidence that Z users can use {log} to generate correct prototypes from their Z specifications. In turn, these prototypes enable or simplify some verificatio activities discussed in the paper.

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 machine by means of first-order logic and set theory. The authors also formalize two state invariants known as security condition and *-property. Bell and LaPadula prove that all the state transitions preserve these invariants. In this paper we present a fully automated proof of the security condition and the *-property for all the model operations. The model and the proofs are coded in the {log} tool. As far as we know this is the first time such proofs are automated. Besides, we show that the {log} model is also an executable prototype. Therefore we are providing an automatically verified executable prototype of BLP.