Automated Reasoning
A.Y. 2018/2019
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.
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.
Expected learning outcomes
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).
automated reasoning, like superposition provers (SPASS, Eprover), SMT
solvers (Z3, Yices, MathSat) or infinite state model checkers (muZ,
nuXmv, MCMT).
Lesson period: Second semester
Assessment methods: Esame
Assessment result: voto verbalizzato in trentesimi
Single course
This course cannot be attended as a single course. Please check our list of single courses to find the ones available for enrolment.
Course syllabus and organization
Single session
Responsible
Lesson period
Second semester
Course 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.
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.
INF/01 - INFORMATICS - University credits: 6
Practicals: 10 hours
Laboratories: 12 hours
Lessons: 28 hours
Laboratories: 12 hours
Lessons: 28 hours
Professor:
Ghilardi Silvio
Professor(s)