5 citations · 13 across the 7 of their papers we have counts for
13 papers
A Set-Theoretic Decision Procedure for Quantifier-Free, Decidable Languages Extended with Restricted Quantifiers
Maximiliano Cristiá, Gianfranco Rossi
Let be the language of first-order, decidable theory . Consider the language, , that extends $\mat…
Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
Maximiliano Cristiá, Gianfranco Rossi
In this paper we show how prescritive type checking and constraint solving can be combined to increase automation during software verification. We do so by defining a type system a…
An Automatically Verified Prototype of a Landing Gear System
Maximiliano Cristiá, Gianfranco Rossi
In this paper we show how (read `setlog'), a Constraint Logic Programming (CLP) language based on set theory, can be used as an automated verifier for B specifications. I…
A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
Maximiliano Cristiá, Gianfranco Rossi
In this paper we extend a decision procedure for the Boolean algebra of finite sets with cardinality constraints () to a decision procedure for $\m…
: Set Formulas as Programs
Maximiliano Cristiá, Gianfranco Rossi
is a programming language at the intersection of Constraint Logic Programming, set programming and declarative programming. But is also a satisfiability solver…
: Applications to Software Specification, Prototyping and Verification
Maximiliano Cristiá, Gianfranco Rossi
This document shows how Z specifications can be translated into and, later, on how can be used to run simulations and automated proofs. This can help users of o…
Integrating Cardinality Constraints into Constraint Logic Programming with Sets
Maximiliano Cristiá, Gianfranco Rossi
Formal reasoning about finite sets and cardinality is an important tool for many applications, including software verification, where very often one needs to reason about the size…
Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra
Maximiliano Cristiá, Ricardo D. Katz, Gianfranco Rossi
{log} ('setlog') is a satisfiability solver for formulas of the theory of finite sets and finite set relation algebra (FSTRA). As such, it can be used as an automated theorem prove…
An Automatically Verified Prototype of the Tokeneer ID Station Specification
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 apply…
Declarative Programming with Intensional Sets in Java Using JSetL
Maximiliano Cristiá, Andrea Fois, Gianfranco Rossi
Intensional sets are sets given by a property rather than by enumerating their elements. In previous work, we have proposed a decision procedure for a first-order logic language wh…
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…
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…