CS-E3220 - Declarative Programming D, Lecture, 15.9.2021-20.12.2021

General

• General
  

  General

  Lecturers	Jussi Rintanen Tommi Junttila
  Teaching assistant	Saurabh Fadnis
  Time & place	The material, exercises, and exercise sessions are all online. The exam organization (classroom or online) is yet to be decided.
  Topics	Constraint programming and constraint satisfaction The propositional satisfiability problem SAT Algorithms for solving SAT, CSP Normal forms and symbolic data structures such as Binary Decision Diagrams (BDD) Symbolic state-space traversal Linear Temporal Logic LTL, computer-aided verification Model-checking with LTL Arithmetic constraints and SAT modulo Theories (SMT) Real-world applications (software engineering, electronic design automation, artificial intelligence)

  The Autumn 2021 edition of the course starts on September 15, welcome!

  • Please see these slides for a high-level introduction to the topic.
  • The participation of the course includes reading the course material, viewing the lecture videos, completing online exercises, and taking an exam.
  • To get help in the exercises, weekly online exercise sessions are organized.
  • For the grading principles, and instructions for the online exercise sessions, please see the "Taking the course" section.
  • In order to get the credits and the course announcements, please remember to register to the course in Sisu.

  The 10 rounds of the course are as follows:

  1. Propositional logic [lecture notes, see "Material" in the online exercises of the round for more]
  2. Fundamentals of SAT solvers [lecture notes, see "Material" in the online exercises of the round for more]
  3. Constraint Satisfaction problems
  4. Transition systems
  5. Symbolic (Logic-Based) Search, Binary Decision Diagrams
  6. Symbolic Search with SAT
  7. Modal and temporal logics
  8. Model-checking in verification and validation
  9. Satisfiability Modulo Theories I
  10. Satisfiability Modulo Theories II

  • 

    ForumAnnouncements Forum