Szukasz praktycznych przykładów zastosowań SMT Z3 (jak DbC) i alternatywy open source dla Z3?

Question

Zainteresowałem się i szukałem praktycznych przykładów użycia SMT Z3 (np. DbC) z kodem i alternatywami open source do tego narzędzia. Tak, w istocie, jestem zainteresowany w podobnych Z3 narzędzi formalny rozwiązywania, ale:

• musi być open source
• zapewniają zarówno niskiego poziomu (API) oraz wysokiego poziomu (skryptowy Text) interakcji
• wsparcie SMT-LIB
• nadaje (użytkowej) w narzędzia/zapisywane w/w języków jak Java, Python, Ruby, Vala i nie Haskell
• ma stabilne (użyteczne w praktyce) narzędzia oparte na nim, jak projektowanie według umowy (DbC), statyczna weryfikacja typu itp.

Według SMT-lib głównej (patrz bit.ly pakiet szczegóły) lista 2010 SMT rozwiązują jest: „Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, satyna, Włócznia, STP, SWORD, UCLID, veriT, Yices, Z3. "

Proszę podać informacje zwrotne na temat korzystania z nich w praktyce (przykłady kodów są najlepsze)?

Wreszcie, wszelkie informacje na temat porównania go z możliwościami GHC byłyby użyteczne, ale tylko w przypadku, gdy istnieje przykład wdrożenia (a nie "funkcja" języka).

Więcej szybka informacja na Z3 tutaj http://bit.ly/bundles/ewiger/1

Answer 1

Zgodnie z moją najlepszą wiedzą, CVC3 przychodzi najbliżej swoich wymagań, w tym, że:

1. posiada zestaw funkcji, który jest podobny do Z3.
2. Ma BSD-style license
3. Jest podstawowym rozwiązaniem dla wielu istniejących projektów.

CVC3 ma bindings dla C++ i Java i prawdopodobnie innych języków. Ogólnie rzecz biorąc, myślę, że API jest znacznie trudniejsze w użyciu niż (tekstowy) input language. Ma to tę dodatkową zaletę, że jeśli będziesz trzymać język SMT-LIB2, możesz później w razie potrzeby przełączyć się na inne narzędzie. Duża próbka przykładów jest dostępna pod adresem SMT-LIB website.

Answer 2

Prosisz o alternatywnych opensource do Z3:

Według SMT-Wikipedia w 2011-08, mamy:

podstawie tych środków, wydaje się, że najbardziej żywy, dobrze zorganizowany projekty to OpenSMT, STP i CVC4.

Po prostu sprawdzam te rzeczy - do tej pory wszystkie trzy wydają się rozsądne, plus starszy kod CVC -> mam na myśli CVC3.