WS 2016/17: Decision Procedures for Verification


Exercise sheets

  • Exercise sheet 1 [ex1.pdf] (submission until 2.11.2016, 12:00)
  • Exercise sheet 2 [ex2.pdf] (submission until 9.11.2016, 12:00)
  • Solutions to the supplementary exercises: [structure-preserving-translation-cnf.pdf]
  • Exercise sheet 3 [ex3.pdf] (submission until 16.11.2016, 11:00; to be discussed on 17.11.2016)
  • Exercise sheet 4 [ex4.pdf] (submission until 23.11.2016, 12:00; to be discussed on 24.11.2016)
  • Exercise sheet 5 [ex5.pdf] (submission until 31.11.2016, 12:00; will be discussed on Thu 1.12.2016)
  • Solution to the suplementary exercise: [solution-ex5-4.pdf]
  • Exercise sheet 6 [ex6.pdf] (submission until 7.12.2016; will be discussed on Thu 8.12.2016)
  • Exercise sheet 7 [ex7.pdf] (due on Wed 14.12.2016; will be discussed on Thu 15.12.2016)
  • Exercise sheet 8 [ex8.pdf] (due on Wed 18.01.2017; will be discussed on Thu 19.01.2017)
  • Exercise sheet 9 [ex9.pdf] (due on Tue 24.02.2017; will be discussed on Thu 26.01.2017)
  • Exercise sheet 10 [ex10.pdf] (due on Wed 8.02.2017; will be discussed on Thu 9.02.2017)
  • Exercise sheet 11 [ex11.pdf] (due on Wed 15.02.2017; will be discussed on Thu 16.02.2017)

  • Solution of the exercise with the Nelson-Oppen procedure discussed in the question-answer session:
  • [solution-nelson-oppen.pdf]

  • Collection of exercises
  • Part 1: [collection-of-exercises-part1.pdf]
  • Part 2: [collection-of-exercises-part2.pdf]