Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 14:00 - 14:30 at Templars - Onward! Papers 2 Chair(s): Hidehiko Masuhara

Relational model finding is a successful technique which has been used in a wide range of problems during the last decade. This success is partly due to the fact that many problems contain relational structure which can be explored using relational model finders. Although these model finders allow for the exploration of such structures they often struggle with incorporating the non-relational elements.

In this paper we introduce AlleAlle, a method and language that integrates reasoning on both relational structure and non-relational elements —the data— of a problem. By combining first order logic with Codd’s relational algebra, transitive closure, and optimization criteria, we obtain a rich input language for expressing constraints on both relational and scalar values.

We present the semantics of AlleAlle and the translation of AlleAlle specifications to SMT constraints, and use the off-the-shelf SMT solver Z3 to find solutions. We evaluate AlleAlle by comparing its performance with Kodkod, a state-of-the-art relational model finder, and by encoding a solution to the optimal package resolution problem. Initial benchmarking show that although the translation times of AlleAlle can be improved, the resulting SMT constraints can efficiently be solved by the underlying solver.

Wed 23 Oct

splash-2019-Onward-papers
14:00 - 15:30: Onward! Papers - Onward! Papers 2 at Templars
Chair(s): Hidehiko MasuharaTokyo Institute of Technology
splash-2019-Onward-papers14:00 - 14:30
Talk
Jouke StoelCWI, Tijs van der StormCWI & University of Groningen, Netherlands, Jurgen VinjuCWI, Netherlands
Link to publication DOI Pre-print
splash-2019-Onward-papers14:30 - 15:00
Talk
Jose CambroneroMIT, Thurston HY DangMIT, Nikos VasilakisMIT CSAIL, USA, Jiasi ShenMassachusetts Institute of Technology, Jerry WuMIT, Martin RinardMIT