Assignments

  •  Assignment 1
  •  Assignment 2
  • Assignment 3 (Do exercise 1 of the attached link)
  • Experimental Exercises

  • Write an MSO formula over finite words defining the following language. Use MONA to generate and print a DFA for this language. "Set of all words over {a,b} such that there are three (possibly overlapping) occurrences of three consecutive b.
  • Exercise 2 of the attached link (Exercise 3 is optional)
  • Exercise 2 of the attached link
  • Solve the exercise in the given link
  • DO the project specified in the given link
  • Suggested Seminar Topics(Incomplete)

  • L. Zhang and S. Malik, The  quest for Efficient Boolean Satisfiability Solvers
  • Combining Heuristic and Symbolic Search: An efficient BDD based A* algorithm
  • Model Based Planning (Extending symbolic model checking techniques to planning)
  • On-the-fly LTL model checking  (source: Madhavan Tutorial on LTL model checking and model checking book chapter)
  • Deciding logic of Uninterpreted functions with Positive Equality
  • Abstraction (Model checking book chapter)

  •