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
100 Forumulas Input
Algorithm Execution
Algorithm Execution
Results Analysis
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
Software Design