Master Tesia

The software development and the increase of software complexity has shown that an automation of the software verification process can be very helpful. Among several methods of verification, the formal ver- ification methods have emerged as the ones with sound mathematical foundations, allowing reasoning about system properties. Temporal logics are formal systems for reasoning about time, for that, they use temporal operators. Temporal logics have found extensive application in computer science, because the behavior of both hardware and software systems can be seen as a sequence of events that evolves along time. Model Checking is one of the most popular methods for automated verification of concurrent systems. Model checking using formulas to represent the system is called Symbolic Model Checking. Properties to be ver- ified are usually expressed in some temporal logic. Moreover, if the property does not hold, the checker returns a counterexample. For larger systems, model checkers need too many resources. To try to reduce the impact of this problem we propose advances in previous works in symbolic model checking. We blend the concept of propositional satisfiability (SAT) solvers for efficient auxiliary tools with linear temporal logic. We use tableaux method for temporal logics to check whether a system satisfies a property. Modern SAT-Solvers are used for the non-temporal reasoning part of the tableau construction. In this master thesis we have developed in Python an algorithm that uses SAT solvers to solve purely propositional formulas leaving the temporary ones for tableaux methods.