Automated Reasoning

A.Y. 2018/2019
Lesson for
6
Max ECTS
50
Overall hours
SSD
INF/01
Language
Italian
Learning objectives
We examine the main technologies employed in automated reasoning,
based both on saturation and on backtracking methods. Applications
covering computational algebra topics as well as formal verification
problems will be considered. The student will be introduced to some stateof-
the-art tools, like for instance SAT- and SMT-solvers, superposition
provers, model finders, finite and infinite state model checkers.
At the end of the course the sudent will be able to use basic tools for
automated reasoning, like superposition provers (SPASS, Eprover), SMT
solvers (Z3, Yices, MathSat) or infinite state model checkers (muZ,
nuXmv, MCMT).

Course structure and Syllabus

Active edition
Yes
Responsible
INF/01 - INFORMATICS - University credits: 6
Practicals: 10 hours
Laboratories: 12 hours
Lessons: 28 hours
Professor: Ghilardi Silvio
Syllabus
- Skolemization and clausal form reduction; unification algorithm and
resolution calculus. The refutational completeness theorem.
- Orderings and ordering constraints; ordered resolution.
- Paramodulation e Superposition. Reduction rules. The architecture of a
prover.
- Word problems: critical pairs, completion, Knuth-Bendix algorithm. Finite
presentations for groups and monoids. Groebner Bases and Buchberger
algorithm.
- SAT problems; DPLL procedure. Non-chronological backtracking, Conflict
Driven Clause Learning and further heuristics.
- From SAT to SMT; basic decision procedures. Combination of decision
procedures. The SMT-LIB standard.
- Applications to infinite state model-checking. Automated verification of
properties of sequential programs and of distributed protocols.
Lesson period
Second semester
Lesson period
Second semester
Assessment methods
Esame
Assessment result
voto verbalizzato in trentesimi
Educational website(s)
Professor(s)