Tzach's Portfolio
Fast LTL Satisfiability Checking by SAT Solvers
July 3, 2020 (5y ago)
Tool that loads LTL formulas and check their satisfiability by using an accelerated algorithm which I implemented by following the paper: https://arxiv.org/pdf/1401.5677.pdf.
Then execution time and satisfiability result per formula is logged.
In addition, the tool calculates and analyzing statistics about the efficiency of this method.

100 Forumulas Input

Algorithm Execution

Results Analysis
Technologies and Frameworks
Backend: C++ 14.
Frontend: JavaScript (ES6), React.js with Hooks and Redux for states management.
External Libraries:
- Microsoft Z3 – Theorem prover with the capabilities of a SAT solver.
- Spot - High performance framework for working and manipulating LTL formulas.
- Crow – Microframework for REST API server implementation.

Software Design