Congress detail

Authors: Cristiá, Maximiliano; Rossi, Gianfranco.

Resumen: In this paper we present a decision procedure for RestrictedIntensional Sets (RIS), i.e. sets given by a property rather than by enu-merating their elements, similar to set comprehensions available in speci-fication languages such as B and Z. The proposed procedure is parametricwith respect to a first-order language and theory X , providing at leastequality and a decision procedure to check for satisfiability of X -formulas.We show how this framework can be applied when X is the theory ofhereditarily finite sets as is supported by the language CLP(SET ). Wealso present a working implementation of RIS as part of the {log} tooland we show how it compares with a mainstream solver and how it helpsin the automatic verification of code fragments.

Meeting type: Conferencia.

Type of job: Artículo Completo.

Production: A Decision Procedure for Restricted Intensional Sets.

Scientific meeting: 26th International Conference on Automated Deduction.

Meeting place: Gotemburgo.

It's published?: Yes

Publication place: Berlín

Meeting month: 8

Year: 2017.