2 citations · 8 across the 8 of their papers we have counts for
7 papers · 1 filter
Encoding and Reasoning about Arrays in Constraint Logic Programming with Sets
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 repr…
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…
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…
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…