TU Wien:Formale Methoden der Informatik VU (Egly)/Folien zusammenfassung

From VoWi
Jump to navigation Jump to search

Vorwissen[edit]

  • NNF
  • CNF

Block1 Pichler[edit]

Foundations of complexity theory.

Bücher:


Sections Papadimitriou sections
Computation and computability 2
Complexity of problems and algorithms 1, 4
Reduction 8
NP-completeness Sect. 9
Other important complexity classes Sect. 16, 19 (little bit)
Turing machines Sect. 2


Content[edit]

  • Decidability
  • Complexity
  • Reduction
  • NP-Complete problems
  • Turing machines
  • Prooving NP-hardness
  • Correctness of reductions

Block2 Egly[edit]

Satisfiability problems (SAT): Solution methods and applications to computer science.

Empfehlung der VL-Leitung:

Content[edit]

  • PL0 (Syntax, Semantics)
  • Propositional formulas as trees (with [Tseitin] | without [Plaisted] polarities)
  • NNF translation
  • CNF translation
  • DLL (tree creation, Backtracking, search)
  • DLIS ... dynamic largest individual sum [1]

Block3 Salzer[edit]

Formal semantics of programming languages, formal verification of programs.

Content[edit]

  • Definition of the SAT problem
  • the principle of faithful PTIME computable reductions from one complete problem into another complete problem of the same complexity class.
  • SAT solving basics (bounded model, checking)
  • Show syntactical Correctnes
  • SOS ... Structural operational Semantics

Block4 Veith[edit]

Model checking with applications to hardware and software verification.

Content[edit]

  • LTS ... Labeled transition System
  • LTL ... Linear Time Logic
  • Kripke Structures
  • Simulation relations
  • CTL ... Computation Tree Logics
  • (C)BMC ... Bounded Model Checker


References[edit]

  1. Christos H. Papadimitriou - Computational Complexity
  2. Decision Procedures–an Algorithmic Point of View, Springer, 2008
  3. The Formal Semantics of Programming Languages, Glynn Winskel
  4. semantics with applications, Riis, Nielson