Spełnialność modulo teorie (SMT) to problem występujący często w praktycznych zagadnieniach weryfikacji sprzętu i oprogramowania. Problem polega zbadaniu spełnialności formuły logiki pierwszego rzędu, gdzie niektóre symbole funkcyjne są interpretowane (np. +, 1, <, write_array).
Więcej informacji o tym problemie można znaleźć na stronie SMT-lib.
Celem seminarium jest zaznajomienie słuchaczy z najnowszymi osiągnięciami w tej dziedzinie oraz implementacja systemu, który by ów problem rozwiązywał. Możliwe będzie zaliczenie przez uczestnictwo w implementacji lub przez zreferowanie jakieś konkretnej metody rozwiązywania owych problemów.
Dostępna na serwerze SVN. Wymaga najnowszej (z SVN lub snapshot) wersji Nemerle.
ChangeLog jest dostępny. Odnawiany co godzinę.
Theorem proving using lazy proof explication Ogólny opis metody rozwiązywania takich problemów z użyciem SAT solvera (właśnie tego używa fx7)
Simplify: A Theorem Prover for Program Checking dłuuuuuugi i dokłady raport techniczny o 10 letnim TP ciągle używanym w praktyce (Spec#, ESC/Java), napisanym w Moduli-3
An Explicating Theorem Prover for Quantified Formulas
A two-tier technique for supporting quantifiers in a lazily proof-explicating theorem provers to zamierzam implementować
Proof-producing Congruence Closure jak wybrać mały niespełnialny pozbiór zbioru równości (mniej lub bardziej zaimplementowane)
A Unit Two Variable Per Inequality Integer Constraint Solver for Constraint Logic Programming prosta metoda rozwiązywania więzów UTVPI (właśnie implementuję), UTVPI to nierówności na liczbach całkowitych postaci ax+by<=d gdzie a,b są -1, 1 lub 0
An Efficient Decision Procedure for UTVPI Constraints jak zredukować sprawdzanie więzów UTVPI do nieujemnych cykli w grafie (jeszcze tego nie rozumiem/nie czytałem dokładnie)
DPLL(T): Fast Decision Procedures Inne podejście do tego problemu, prawdopodobnie szybsze (tak do 100 razy), nie testowałem