CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories

CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories

We introduce an approach that aims to combine the usage of satisfiability modulo theories (SMT) solvers with the Combinatory Logic Synthesizer (CL)S framework. (CL)S is a tool for the automatic composition of software components from a user-specified repository. The framework yields a tree grammar...

Full description

Bibliographic Details
Main Authors: Fadil Kallat, Tristan Schäfer, Anna Vasileva
Format: Article
Language:English
Published: Open Publishing Association 2019-08-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1908.09481v1
id doaj-9136cd5bcbe0401ab50c41c736710019
record_format Article
spelling doaj-9136cd5bcbe0401ab50c41c7367100192020-11-25T02:12:44ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-08-01301Proc. PxTP 2019516510.4204/EPTCS.301.7:1CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo TheoriesFadil Kallat0Tristan Schäfer1Anna Vasileva2 Technical University of Dortmund, Germany Technical University of Dortmund, Germany Technical University of Dortmund, Germany We introduce an approach that aims to combine the usage of satisfiability modulo theories (SMT) solvers with the Combinatory Logic Synthesizer (CL)S framework. (CL)S is a tool for the automatic composition of software components from a user-specified repository. The framework yields a tree grammar that contains all composed terms that comply with a target type. Type specifications for (CL)S are based on combinatory logic with intersection types. Our approach translates the tree grammar into SMT functions, which allows the consideration of additional domain-specific constraints. We demonstrate the usefulness of our approach in several experiments.http://arxiv.org/pdf/1908.09481v1
collection DOAJ
language English
format Article
sources DOAJ
author Fadil Kallat
Tristan Schäfer
Anna Vasileva
spellingShingle Fadil Kallat
Tristan Schäfer
Anna Vasileva
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
Electronic Proceedings in Theoretical Computer Science
author_facet Fadil Kallat
Tristan Schäfer
Anna Vasileva
author_sort Fadil Kallat
title CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
title_short CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
title_full CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
title_fullStr CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
title_full_unstemmed CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
title_sort cls-smt: bringing together combinatory logic synthesis and satisfiability modulo theories
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2019-08-01
description We introduce an approach that aims to combine the usage of satisfiability modulo theories (SMT) solvers with the Combinatory Logic Synthesizer (CL)S framework. (CL)S is a tool for the automatic composition of software components from a user-specified repository. The framework yields a tree grammar that contains all composed terms that comply with a target type. Type specifications for (CL)S are based on combinatory logic with intersection types. Our approach translates the tree grammar into SMT functions, which allows the consideration of additional domain-specific constraints. We demonstrate the usefulness of our approach in several experiments.
url http://arxiv.org/pdf/1908.09481v1
work_keys_str_mv AT fadilkallat clssmtbringingtogethercombinatorylogicsynthesisandsatisfiabilitymodulotheories
AT tristanschafer clssmtbringingtogethercombinatorylogicsynthesisandsatisfiabilitymodulotheories
AT annavasileva clssmtbringingtogethercombinatorylogicsynthesisandsatisfiabilitymodulotheories
_version_ 1724908547542614016

Similar Items