Home / Formal Verification Lab
Formal Verification Lab
Making digital systems provably trustworthy — at the intersection of logic, algorithms, and systems engineering.
Making digital systems provably trustworthy — at the intersection of logic, algorithms, and systems engineering.
The Formal Verification Lab, led by Prof. Yakir Vizel in the Computer Science Department at the Technion, brings together students and researchers working to make hardware and software systems provably correct. We develop the algorithms and tools that allow engineers to specify a system precisely and prove that an implementation satisfies its specification.
Our tools and source code are available on GitHub: github.com/TechnionFV.
To translate advances in verification theory into practical tools that hardware and software engineers can use with confidence.
Model checkers, CHC solvers, interpolation engines, and abstraction frameworks, often released as open source on GitHub.
We collaborate with partners across academia and industry on problems in hardware and software verification.
If model checking, logic, and provably-correct systems excite you, we would like to hear from you. Please see the contact page to contact us.