Loading...
Loading...

Go to the content (press return)

Logic-Based Smart Solutions

Type of activity
Competitive project
Acronym
LoBaSS
Funding entity
MIN DE ECONOMIA Y COMPETITIVIDAD
Funding entity code
TIN2015-69175-C4-3-R
Amount
87.483,00 €
Start date
2016-01-01
End date
2019-12-31
Keywords
análisis y verificación de programas, constraint solving, formula satisfiability, logics, lógicas, program analysis and verification, resolución de restricciones, satisfacibilidad de fórmulas
Abstract
Facing the challenges that software systems pose today requires innovative smart solutions. Many challenges in Information Technology
for the Digital Society involve the analysis of complex systems, e.g., scheduling problems in a smart factory, resource and security analysis
in distributed systems, safety and liveness concerns in multi-threaded programs or dynamic resource allocation in a cloud system, among
others. Such complex interdependent systems are growing in smart cities, the healthcare industry, or sustainable transport. Most of these
systems are safety critical and economically vital. However, building robust tools to analyze them still remains a major endeavour.
Our approach follows the next three steps: first, a real complex system is modeled using a more abstract representation; second, smart
solutions are obtained by expressing the problems in some logical framework; and then, finally, powerful logic-based technologies are
applied to analyze and/or solve the problems. The LoBaSS project contributes in all three directions: modeling real problems, finding
representations in some appropriate logical framework, and developing tools and techniques to better solve or optimize the resulting
problems. This overall approach allows us to apply the same techniques in multiple application domains (e.g., cloud computing, smart
factories, protocol analysis), which makes the development of tools to solve hard real problems significantly easier and faster.
As logical frameworks we are mainly using extensions and combinations of propositional and first-order logic and algebraic structures. In
particular, we are considering: SAT (satisfaction of propositional formulas), SAT modulo theories (SMT, where propositions are replaced
by atoms in a given theory), Constraint Programming (CP, where clauses are replaced by predicates over a pre-defined language), Fuzzy
Logic (FL, where clauses have some uncertainty), Rewrite Logic (RWL, with modelling and programming advanced capabilities), Logic
Programming (LP), Fuzzy Logic Programming (FLP) and Abstract Interpretation (AI, based on monotonic functions over lattices). In this
project we will focus on the combination and extension of these successful formal languages to get the necessary expressiveness for our
practical applications. Today's challenges in Information Technology will guide our work in scheduling and planning, security, machine
learning, complex systems analysis, bio-informatics or XML manipulation, developing efficient algorithms and tools to solve them.
As specific application domains we consider: (a) sports scheduling as done with KNVB, (b) optimization and planning in collaboration with
Barcelogic Solutions and with the interest of companies like SIMO and E2F, (c) analysis of complex systems in collaboration with Microsoft
Research and with the interest of many national and international companies (IBM, Thales, Clearsy, Vossloh, Edicom and Semantic
Systems), (d) security in collaboration with the University of Illinois and the Naval Research Laboratory, (e) fuzzy scheduling for resource
usage within cloud data centers with the Umea University and (f) analysis of transcript sequences in collaboration with the IMIM.
All in all, our project covers all the way in the development and application of computer technologies from the basic theory and techniques
to the current challenges of information technologies in the digital society and the smart, green and integrated transport.
Scope
Adm. Estat
Plan
Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016
Call year
2016
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
Gobierno De España. Ministerio De Economía Y Competitividad, Mineco

Participants