All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”
LL1902

Powering SMT Solvers by Machine Learning

Public support

  • Provider

    Ministry of Education, Youth and Sports

  • Programme

    ERC CZ

  • Call for proposals

    SMSM2019LL001

  • Main participants

    České vysoké učení technické v Praze / Český institut informatiky, robotiky a kybernetiky

  • Contest type

    VS - Public tender

  • Contract ID

    MSMT-35696/2019-1

Alternative language

  • Project name in Czech

    Obohacování SMT řešičů pomocí strojového učení

  • Annotation in Czech

    "Cílem projektu POSTMAN je dosáhnout průlomu v oblasti Splnitelnost Modulo Teorie (SMT) pomocí vývoje metod strojového učení cílených na kritické části dnešních procedur pro řešení SMT. Řešiče SMT jsou účinné nástroje, které uvažují nad fragmenty logiky prvního řádu se zaměřením na praktické aplikace. Tyto nástroje hrají stěžejní roli v ověřování a testování softwaru, hardwaru a příbuzných oblastech. K řešení problémů z reálného světa, mnoho nástrojů závisí na SMT tím, že překládají daný problém do formulace matematické logiky a delegují jeho řešení SMT řešiči. SMT se tímto ocitá v jádru dnešních verifikačních nástrojů, které se systematicky spouští na tisících procesorech ve velkých softwarových a hardwarových firmách. SMT systémy usilují o poskytnutí plné automatizace, ale oproti tomu musí řešit ze své podstaty těžké problémy. Pokud nástroj nevyřeší daný problém v požadovaném čase, uživatelé jsou nuceni reformulovat tento problém nebo poskytnout řešiči nápovědu. Oba scénáře jsou nežádoucí tím že vyžadují další úsilí a značnou znalost používaného nástroje. POSTMAN velmi výrazně pokročí v řešení SMT rozvíjením metod strojového učení, které prořezávají prohledávací prostor problému. Na rozdíl od současných metod prohledávání, strojové učení umožňuje brát v úvahu velký počet pozorování provedených během hledání důkazů a doporučit nejrelevantnější postup. Projekt bude rozvíjet učící metody na různých úrovních abstrakce se zaměřením na dva kritické problémy v SMT a jeho aplikacích: řešení kvantifikovaných formulí a řešení tříd formulí. Očekávaným výstupem projektu je řada nových výkonných metod kombinujících techniky strojového učení se současnými přístupy SMT založenými na logice, které poskytnou výrazné zlepšení oproti současnému stavu. Tyto metody budou integrovány do řady systémů a nasazeny ve významných SMT aplikacích, používaných ve velké části moderního formálního ověřování."

Scientific branches

  • R&D category

    ZV - Basic research

  • OECD FORD - main branch

    20202 - Communication engineering and systems

  • OECD FORD - secondary branch

  • OECD FORD - another secondary branch

  • CEP - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)

    JW - Navigation, connection, detection and countermeasure

Solution timeline

  • Realization period - beginning

    Jan 1, 2020

  • Realization period - end

    Dec 31, 2025

  • Project status

    B - Running multi-year project

  • Latest support payment

    Jan 10, 2024

Data delivery to CEP

  • Confidentiality

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

  • Data delivery code

    CEP24-MSM-LL-R

  • Data delivery date

    Feb 19, 2024

Finance

  • Total approved costs

    38,916 thou. CZK

  • Public financial support

    38,916 thou. CZK

  • Other public sources

    0 thou. CZK

  • Non public and foreign sources

    0 thou. CZK