Experiments on Infinite Model Finding in SMT Solving

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F23%3A00372208" target="_blank" >RIV/68407700:21730/23:00372208 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.29007/slrm" target="_blank" >https://doi.org/10.29007/slrm</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/slrm" target="_blank" >10.29007/slrm</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Experiments on Infinite Model Finding in SMT Solving

Popis výsledku v původním jazyce

We propose infinite model finding as a new task for SMT-Solving. Model finding has a long-standing tradition in SMT and automated reasoning in general. Yet, most of the current tools are limited to finite models despite the fact that many theories only admit infinite models. This paper shows a variety of such problems and evaluates synthesis approaches on them. Interestingly, state-of-the-art SMT solvers fail even on very small and simple problems. We target such problems by SyGuS tools as well as heuristic approaches.

Název v anglickém jazyce

Experiments on Infinite Model Finding in SMT Solving

Popis výsledku anglicky

We propose infinite model finding as a new task for SMT-Solving. Model finding has a long-standing tradition in SMT and automated reasoning in general. Yet, most of the current tools are limited to finite models despite the fact that many theories only admit infinite models. This paper shows a variety of such problems and evaluates synthesis approaches on them. Interestingly, state-of-the-art SMT solvers fail even on very small and simple problems. We target such problems by SyGuS tools as well as heuristic approaches.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/LL1902" target="_blank" >LL1902: Obohacování SMT řešičů pomocí strojového učení</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2023

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)

ISBN

—

ISSN

2398-7340

e-ISSN

2398-7340

Počet stran výsledku

12

Strana od-do

317-328

Název nakladatele

EasyChair Publications

Místo vydání

Manchester

Místo konání akce

Manizales

Datum konání akce

4. 6. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—