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

Vorwissen

• NNF
• CNF

Block1 Pichler

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

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

Block2 Egly

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

Empfehlung der VL-Leitung:

Content

• 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

Formal semantics of programming languages, formal verification of programs.

Content

• 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

Model checking with applications to hardware and software verification.

Content

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