Subjects

Your browser does not support JavaScript, or its support is disabled. Some features may not be available.

Decision Procedures and Verification - NAIL094

Title:	Rozhodovací procedury a verifikace
Guaranteed by:	Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty:	Faculty of Mathematics and Physics
Actual:	from 2016 to 2016
Semester:	winter
E-Credits:	6
Hours per week, examination:	winter s.:2/2, C+Ex [HT]
Capacity:	unlimited
Min. number of students:	unlimited
4EU+:	no
Virtual mobility / capacity:	no
State of the course:	not taught
Language:	Czech
Teaching methods:	full-time
Teaching methods:	full-time

Guarantor:	doc. RNDr. Pavel Surynek, Ph.D.
Class:	Informatika Mgr. - volitelný
Classification:	Informatics > Theoretical Computer Science

Opinion survey results Examination dates Schedule Noticeboard

Annotation -

Last update: T_KTI (04.05.2012)

A course on logic theories and procedures for deciding satisfiability in these theories with emphasis on the application in program verification. Construction of an efficient SAT solver (DPLL, conflict-directed clause learning), local algorithms for satisfiability (WalkSAT, survey propagation), decisions in logic with equality, uninterpreted functions and pointers, quantified Boolean formulae (QBF), combining logic theories, SAT-modulo solvers.

Literature -

Last update: T_KTI (04.05.2012)

Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View. Springer, 2008.

Aaron R. Bradley, Zohar Manna: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.

Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. The MIT Press, 2008.

Edmund M. Clarke Jr., Orna Grumberg, Doron A. Peled: Model Checking. The MIT Press, 1999.

Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of

Satisfiability, IOS Press, 2009.

Syllabus -

Last update: T_KTI (04.05.2012)

A course on logic theories and procedures for deciding satisfiability in

these theories with emphasis on the application in program verification.

Construction of an efficient SAT solver (DPLL, conflict-directed clause

learning), local algorithms for satisfiability (WalkSAT, survey

propagation), decisions in logic with equality, uninterpreted functions and

pointers, quantified Boolean formulae (QBF), combining logic theories,

SAT-modulo solvers.

The course is accompanied with a seminar. There will be tasks to exercise

the taught material as well as implementation tasks based on the existent

software libraries.