Characteristics

A.Y. 2010
Code 25421
Credits 3
Lecturer Roberto Sebastiani
Language English
Period N/D

Course objectives and contents

We aim at providing a background on efficient Boolean reasoning techniques, in particular relating to SAT and SMT technologies. The attendee is required to have some background on Boolean logic and on algorithms.

Keywords

SW Engineering and formal meythods, Embedded systems, automated reasoning, knowledge representation

Program

The ability of efficiently reasoning with boolean values and operators is a core feature of many applications in various fields of Artificial Intelligence, Formal Verification and Digital Electronics, including, e.g., Automated Reasoning and Planning, Formal verification of Hardware and Software devices, Knowledge Representation and Reasoning. The last two decades have witnessed a striking interest in boolean reasoning (boolean SATisfiability, SAT, from now on), with a boost in the performances of SAT solvers, which has brought large previously intractable problems at the reach of state-of-the-art solvers. As a consequence, some hard real-world problems ---like, e.g., boolean circuit verification, planning and model checking--- have been successfully solved by encoding them into SAT. More recently, SAT techniques have been shown to be very useful not only for solving boolean expressions, but also as basic reasoning engines for solving expressions in more expressive domains like, e.g., reasoning with multi-agent modal expressions and knowledge bases, conformant planning, resource planning, temporal reasoning, formal verification of real-time and hybrid systems, verification of Hardware at RTL level. This discipline is referred to as Satisfiability Modulo Theories (SMT)

Notes

PERIOD: SCHEDULE: 01/03/2010, 14:00 - 16:00, room 106 02/03/2010, 17:00 - 19:00, room 208 03/03/2010, 13:00 - 15:00, room 106 04/03/2010, 11.30 - 13.30, room 7 05/03/2010, 14:00 - 17:00, room 208 08/03/2010, 14:00 - 16:00, room 101 09/03/2010, 15:00 - 18:00, room 106 10/03/2010, 13:00 - 15:00, room 101 11/03/2010, 17:15 - 19:15, room 205