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.