Inicio   >   Proyectos   >   FREETECH

FreeTech

Razonamiento Formal paraTecnologías Facilitadoras y Emergentes

Ámbito
Nacional
Fecha
01/01/2019 - 31/12/2021
Sector
  • Otros
  • Salud
Presupesto
242000
Finanaciador

Agencia Estatal de Investigación

Video

INFORMACIÓN DEL PROYECTO

DESCRIPCIÓN

El uso de técnicas basadas en razonamiento formal se ha usado con éxito para garantizar la fiabilidad, la eficiencia y la seguridad de los productos tecnológicos. El enfoque del proyecto FREETech es el siguiente: (1) el desarrollo de técnicas de análisis, verificación, testing y depuración de programas que permitan razonar sobre la corrección, la eficiencia y posibles vulnerabilidades tanto en aplicaciones existentes como emergentes. Entre estas aplicaciones se encuentran las redes definidas por software o los smart contracts para los que el consumo de recursos y la seguridad son muy relevantes, así como los protocolos de comunicaciones con propiedades físicas tales como el tiempo real o las distancias; (2) el uso de técnicas de data science y machine learning para obtener, desarrollar y/o manipular modelos de las aplicaciones actuales; (3) el uso de razonamiento formal para mejorar las técnicas de búsqueda en secuencias genómicas; o (4) el uso de herramientas y técnicas de resolución de restricciones y optimización (SAT, SMT y CP) para abordar problemas de planificación y replanificación complejos.
De esta forma, nuestro proyecto cubre desde la teoría básica para el desarrollo y la aplicación de las tecnologías facilitadoras existentes, hasta los retos actuales introducidos por las tecnologías de la información emergentes en la sociedad digital.

El uso de técnicas basadas en razonamiento formal se ha usado con éxito para garantizar la fiabilidad, la eficiencia y la seguridad de los productos tecnológicos. El enfoque del proyecto FREETech es el siguiente: (1) el desarrollo de técnicas de análisis, verificación, testing y depuración de programas que permitan razonar sobre la corrección, la eficiencia y posibles vulnerabilidades tanto en aplicaciones existentes como emergentes. Entre estas aplicaciones se encuentran las redes definidas por software o los smart contracts para los que el consumo de recursos y la seguridad son muy relevantes, así como los protocolos de comunicaciones con propiedades físicas tales como el tiempo real o las distancias; (2) el uso de técnicas de data science y machine learning para obtener, desarrollar y/o manipular modelos de las aplicaciones actuales; (3) el uso de razonamiento formal para mejorar las técnicas de búsqueda en secuencias genómicas; o (4) el uso de herramientas y técnicas de resolución de restricciones y optimización (SAT, SMT y CP) para abordar problemas de planificación y replanificación complejos.
De esta forma, nuestro proyecto cubre desde la teoría básica para el desarrollo y la aplicación de las tecnologías facilitadoras existentes, hasta los retos actuales introducidos por las tecnologías de la información emergentes en la sociedad digital.

Impacto

The techniques and tools that are based on formal reasoning are having a great impact on many areas of application of Information Technology, as well as in the search for solutions to the different computational problems that turn out in digital economy and society, and security and defense, but also the ones that arise in health, energy efficiency or smart and sustainable transport challenges.
The leading technology companies, as Facebook, Amazon and Google, are banking on the use of formal reasoning for the development and implementation of their technology. Recently, in the Federation of Conferences FLOC (Federated Logic Conference 2018), a
workshop on Formal Methods in Industry was held (https://www.floc2018.org/formal-methods-in-industry), where the leader researchers from the three above-mentioned companies explained how the formal reasoning has become the cornerstone of their technological development processes. Byron Cook, professor at University College of London and director of the Automated Reasoning Group (ARG) at Amazon Web Services (AWS) related, as an example of the enormous impact that these techniques can have in his sector, that AWS uses and develops tools based on formal reasoning to detect and avoid security problems both in AWS and in the systems that are created by the customers over AWS.
As another example of direct impact, the optimization techniques based on logic and formal reasoning may report an important benefit in the enterprise environment. The flexibility that characterizes these methods offers to the organizations a quick technology which is able to improve their results in a variety of scenarios.
Formal reasoning achieves even more importance in the most emerging areas of application, such as smart-contracts used in blockchain technologies, software-defined networks, bioinformatics, communication protocols or the more frequent use of learning techniques in a multitude of environments and applications. The techniques based on formal reasoning are essential to reach the objectives of the project, which result in applications with a major economic and social impact as blockchain technology, software-defined networks, industrial planning and programming or resources located in the cloud, program analysis, security, the discovery of knowledge and web data manipulation or the detection of some genome sequences.
As the scientific histories of the different research groups involved in the proposal guarantee, the expected scientific international impact of the objectives and results that the project pursues is expected to be large and it is expected to publish them in conferences and journals internationally recognized and with high impact. To conclude, it is expected that project FREETech reaches a significant national and international impact, both on the advance of science and technology and its transfer to public and private companies and organizations.

Entidades

* Universitat Politècnica de València
* Universidad de Castilla la Mancha
* Universitat Politècniac de Catalunya

DATOS DE CONTACTO

Santiago Escobar
Profesor

VRAIN

CAPACIDADES TECNOLÓGICAS

Ciberseguridad
Data security and privacy technologies