search

levjj / esverify

ECMAScript verification with SMT solvers
https://esverify.org/
MIT License
122 stars 5 forks source link

support for vampire prover #3

Open nikhedonia opened 5 years ago

nikhedonia commented 5 years ago

Just wanted to raise awareness of Vampire Prover

Vampire prover uses z3 and minisat internally and performs significantly better in many tasks. One of its unique features is to can discover loop invariants and compute closed form solutions.

Here is the talk about Vampire Prover at FaceTAV from last week: https://www.facebook.com/ze.jaloto/videos/10157041551887975/

levjj commented 5 years ago

Thanks! I just noticed that the Vampire prover supports SMTLIB 2 input, so it might not be too difficult to use it for esverify.