Overview
In the transition from an industrial economy to a knowledge-based global economy, computer technologies have become a determining factor in productivity advances and, as a result, in economic growth. Many works are conclusive regarding the fact that, starting from the second half of the nineties, computer technologies have played a progressively important role in the productivity advances of the G7 countries. Especially in Spain, a major part of this process is currently still taking place, and this project aims at acting as a catalyst by means of the application of advanced techniques in areas of great economic and social impact. The common feature of these techniques is that they are all based on logical methods.
The main goal of this project is the development of logic-based theory, techniques and tools, and their application in different areas with important economic and social impact. The main techniques and tools that are considered in this project are:
- solvers for propositional logic (SAT), SAT Modulo Theories (SMT) and (fragments of) first-order logic,
- techniques and tools for abstract interpretation and model checking,
- algebraic techniques for constraint solving,
- automated certification techniques.
These techniques are fundamental in order to achieve the aforementioned goals, which in this project are concretized in applications with big economic and social impact:
- verification of safety and liveness/termination properties of all sorts of software, including Web applications,
- high-level hardware verification,
- data mining on heterogeneous data,
- cryptographic protocol analysis and security properties
- bioinformatics problem solving,
- industrial and sports scheduling.
