Go to the content (press return)

Formal reasoning for enabling and emerging technologies

Total activity: 9
Type of activity
Competitive project
Funding entity
Funding entity code
181.500,00 €
Start date
End date
The use of techniques based on formal reasoning has succeeded in ensuring the reliability, the efficiency and the security of technological
products. This type of guarantees is vital in order to achieve many of the challenges in Information Technology and, especially, in
emerging applications such as smart-contracts, used in blockchain technology or communication protocols, where the absence of security
has resulted in major economic loss (e.g., the well-known DAO attack caused heavy losses). In addition, the use of logic-based tools to
solve planning problems has generated important benefits in many different contexts such as passenger transport, management of
industrial processes or the organization of sports events and competitions widely distributed.
In spite of the above-mentioned advantages, the development of formal reasoning techniques for enabling technologies (term used to refer
to the existing technologies that are essential for achieving specific results) and emerging technologies, as well as the creation of tools
based on formal reasoning, present important challenges to be solved. The approach of the project FREETech to achieve these
milestones is as follows: (1) development of techniques based on program analysis, verification, testing and debugging that allow
reasoning about correctness, efficiency and potential vulnerabilities both in existing and emerging applications. These applications include
software-defined networks and smart-contracts, for which the resource consumption and the security are very relevant, as well as the
communication protocols with physical properties such as real time or distances; (2) the use of data science and machine learning
techniques to obtain, develop and/or manipulate models of the current applications; (3) the use of formal reasoning to improve search
techniques in genomic sequences; or (4) the use of constraint resolution and optimization tools and techniques (SAT, SMT and CP) to
target complex scheduling and rescheduling problems.
To face this challenge we will rely on the following formal reasoning techniques: we will consider static analysis techniques based on
abstract interpretation, which have proven to be rigorous and effective in inferring complex code properties (such as resource
consumption). To address the validation of concurrent and distributed applications we will use techniques of model checking and symbolic
execution of programs combined with the theory of Dynamic Partial Order Reduction that allows exploring the execution of this type of
applications in a scalable way. SAT and SMT solvers and CP techniques will be mainly used. We will also use program analysis and
transformation techniques to optimize different aspects.
In this way, our project covers from basic theory for the development and application of existing enabling technologies, to the current
challenges introduced by the emerging information technologies in the digital society.
análisis estático, aprendizaje, constraint solving, contratos inteligentes, formal reasoning, learning, optimización, optimization, razomiento formal, resolución de restricciones, security, seguridad, smart contracts, static analysis, testing, transformación, transformation, verificación, verification
Adm. Estat
Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020
Resoluton year
Funcding program
Programa Estatal de I+D+i Orientada a los Retos de la Sociedad
Funding call
Retos de Investigación: Proyectos de I+D+i
Grant institution
Agencia Estatal De Investigacion


Scientific and technological production

1 to 9 of 9 results