Informace o projektu
Vývoj nástroje Q3B s částečnými BDD
| Kód projektu | MUNI/33/0766/2022 CEP CORDIS MU WEB INET MU |
|---|---|
| Doba řešení | 01.07.2022–30.09.2023 |
| Stav | ukončený |
| Investor | Masarykova univerzita |
| Program | Interní projekty FI |
| Řešitel za FI | |
| Členové realizačního týmu za FI |
Anotace
Q3B je zavedený SMT-solver pro teorii kvantifikovaných bitvektorových formulí, který využívá k reprezentaci průběžných výsledků datovou strukturu BDD. V roce 2021 vznikla verze Q3B využívající částečné BDD se slibnými experimentálními výsledky. Cílem projektu je implementovat operace redukující velikost částečných BDD podle různých parametrů, což by mělo vést ke zrychlení výpočtu Q3B na některých typech formulí.