Overview
The aim of this project is to act as a catalyst in the global impact of Information Technology (IT) in Spain by developing and applying advanced tools and techniques in areas of economic and social interest. The common feature of these techniques is that they are all based on logical methods. Logic-based theory, techniques and tools are playing an increasing role in different IT areas, as well as in finding solutions to numerous computational problems that arise in industry and sciences like Biology.
As its predecessor, this is a joint project between two large groups from the Technical Universities of Valencia and Catalonia, both with an extensive experience in the area. The main techniques and tools that are considered in this project are:
- Solvers for propositional logic (SAT) and SAT Modulo Theories (SMT) and optimization with these (Max-SAT/SMT and Branch and Bound for SAT/SMT with arbitrary cost functions),
- Logic-based Solvers and filtering algorithms for Constraint Programming,
- Mathematical programming tools applied as Theory Solvers for SMT,
- Techniques and tools for abstract interpretation and model checking,
- Algebraic methods for constraint solving; and verification and certification techniques.
All these logic-based techniques are fundamental in the achievement of goals of the project, which are concretized in applications with significant economic and social impact:
- Industrial planning, scheduling and timetabling, which are omnipresent in both public and private sectors, from healthcare or public order to virtually all branches of the logistics and transportation sectors, sports scheduling as well as scientific combinatorial optimization problems from e.g., Biology, Medicine or Linguistics. Methods to be used are SAT, SMT (with optimization) and other logic-based methods, in combination with Constraint and Mathematical Programming;
- Verification of safety and liveness/termination properties of all sorts of software, including Web applications;
- High-level hardware verification;
- Modeling complex systems involving agents;
- Analyzing security properties of web applications.
