SubjectsSubjects(version: 845)
Course, academic year 2018/2019
   Login via CAS
Decision Procedures and Verification - NAIL094
Title in English: Rozhodovací procedury a verifikace
Guaranteed by: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty: Faculty of Mathematics and Physics
Actual: from 2018 to 2018
Semester: summer
E-Credits: 6
Hours per week, examination: summer s.:2/2 C+Ex [hours/week]
Capacity: unlimited
Min. number of students: unlimited
State of the course: not taught
Language: Czech
Teaching methods: full-time
Additional information: http://d3s.mff.cuni.cz/teaching/decision_procedures/
Guarantor: prof. RNDr. Roman Barták, Ph.D.
Class: Informatika Mgr. - volitelný
Classification: Informatics > Theoretical Computer Science
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.

 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html