Detalle del congreso

Autores: 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.

Tipo de reunión: Conferencia.

Tipo de trabajo: Artículo Completo.

Producción: A Decision Procedure for Restricted Intensional Sets.

Reunión científica: 26th International Conference on Automated Deduction.

Lugar: Gotemburgo.

Publicado: Sí

Lugar publicación: Berlín

Mes de reunión: 8

Año: 2017.