# Master Tesia

Tituloa:

An implementation of PLTL-model-checking using context-based tableaux and SAT-solvers

Egilea:

Luis Pérez Guerrero

Abstract:

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.

Fitxategia:

Tutorea:

Montserrat Hermo & Paqui Lucio

Urtea:

2019

Esleitua: