TU Wien:Formale Methoden der Informatik VU (Egly)/Folien zusammenfassung
Jump to navigation
Jump to search
Vorwissen[edit | edit source]
- NNF
- CNF
Block1 Pichler[edit | edit source]
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 | edit source]
- Decidability
- Complexity
- Reduction
- NP-Complete problems
- Turing machines
- Prooving NP-hardness
- Correctness of reductions
Block2 Egly[edit | edit source]
Satisfiability problems (SAT): Solution methods and applications to computer science.
Empfehlung der VL-Leitung:
Content[edit | edit source]
- 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 | edit source]
Formal semantics of programming languages, formal verification of programs.
Content[edit | edit source]
- 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
Block4 Veith[edit | edit source]
Model checking with applications to hardware and software verification.
Content[edit | edit source]
- LTS ... Labeled transition System
- LTL ... Linear Time Logic
- Kripke Structures
- Simulation relations
- CTL ... Computation Tree Logics
- (C)BMC ... Bounded Model Checker