WS 2018/19: Decision Procedures for Verification

Exercise sheets

Exercise sheet 1 [ex1.pdf] (submission until 30.10.2018, 17:00)

Exercise sheet 2 [ex2.pdf] (submission until 6.11.2018, 17:00, to be discussed on 8.11.2018)

Exercise sheet 3 [ex3.pdf] (submission until 14.11.2018, 16:00; to be discussed on 15.11.2018)

Linear algorithm for checking the satisfiability of Horn Clauses [horn.pdf]

Exercise sheet 4 [ex4.pdf] (submission until 20.11.2018, 17:00; to be discussed on 22.11.2018)

Solution to the suplementary exercise 4.6: PTIME algorithm for checking the satisfiability of 2-CNF Clauses [2-dat.pdf]

Exercise sheet 5 [ex5.pdf] (submission until 27.11.2018, 17:00; will be discussed on 29.11.2018)

Exercise sheet 6 [ex6.pdf] (submission until 5.12.2018; will be discussed on Thu 6.12.2018)

Exercise sheet 7 [ex7.pdf] (submission until 11.12.2018; will be discussed on Thu 13.12.2018)

Recapitulative exercises [collection-of-exercises-part1.pdf]

(will be discussed on Thursday, 20.12.2018 only if needed -
you can submit the solutions until Tuesday, 18.12.2018 at 16:00)

On Thursday, 20.12.2018 we will probably have a lecture, not an exercise session.

Some aspects in the recapitulative exercises will be briefly discussed at the beginning if needed.

Exercise sheet 8 [ex8.pdf] (due on Wed 9.01.2019, 12:00; will be discussed on Thu 10.01.2019) -

Exercise sheet 9 [ex9.pdf] (due on Wed 16.01.2019 at 13:00; exercises 9.1-9.4 will be discussed on Thu, 17.01.2019; Depending on time constraints we might discuss exercise 9.5 either on 17.01.19 or on 24.01.19).

Exercise sheet 10 [ex10.pdf] (due on Wed 23.01.2019; will be discussed on Thu 24.01.2019)

Exercise sheet 11 [ex11.pdf] (due on Wed 30.01.2019; will be discussed on Thu 31.01.2019)

Exercise sheet 12 [ex12.pdf] (due on Wed 6.02.2019; will be discussed on Thu 7.02.2019)

Solution: Nelson-Oppen procedure

[solution-nelson-oppen.pdf]

Collection of exercises

Part 1: [collection-of-exercises-part1.pdf]

Part 2: [collection-of-exercises-part2.pdf]