Video-Server > Vorlesungen > Logik und Verifikation

Logik und Verifikation


Kamera Anja Michaela Kaiser
von Prof. Dr. rer. nat. Jürgen Dix

im Sommersemester 2016

Vorlesungskennung: S 1165

This course is about logic based formal methods and how to use them for verification in computer science.
It rigorously defines the language and semantics of sentential logic (SL) and first-order logic (FOL).
We introduce the notion of a model, and show how hardware and software systems can be modelled within this framework. We also consider
semantic entailment vs. syntactic derivability of formulae and how these two notions are related through correctness and completeness. Completeness is formally proved for SL and extensively discussed for FOL (in the form of refutation completeness).
Both logics are applied to important verification problems: SL and its extension LTL for verifying linear temporal properties in concurrent systems, and
FOL for verifying input/output properties of programs (the Hoare calculus).
We show how the resolution calculus for FOL leads to PROLOG, a programming language based on FOL.
We also show that SL leads to a declarative version of PROLOG: Answer Set Programming (ASP), that can be used to solve problems expressible on the second level of the polynomial hierarchy.
While ASP is not a full-fledged programming language, it can be used for many naturally ocurring problems and it allows to model them in a purely declarative way.

1. Introduction
2. Sentential Logic (SL)
3. Verification I: Reactive Systems
4. First-Order Logic (FOL)
5. Verification II: Hoare Calculus
6. From FOL to PROLOG
7. PROLOG

Weitere Informationen zur Vorlesung:
Institut für Informatik oder im Vorlesungsverzeichnis

52 Aufrufe

Vorlesungen


1. Introduction

Vorlesung Nr. 1
Aufgezeichnet am 11.04.2016 | 9 Aufrufe

01:33:08

Vorlesung starten

Inhalt:
What is AI?; Logic: From Plato To Zuse; Verification: Verifying reactive systems, Verifying programs

1. Introduction - 2. Sentential Logic (SL) - Übung 1: Sentential Logic

Vorlesung Nr. 2
Aufgezeichnet am 12.04.2016 | 5 Aufrufe

01:36:35

Vorlesung starten

Inhalt:
1.3 Verification; 2.1 Motivation; 2.2 Syntax and Semantics

2. Sentential Logic (SL)

Vorlesung Nr. 3
Aufgezeichnet am 18.04.2016 | 5 Aufrufe

01:25:18

Vorlesung starten

Inhalt:
2.2 Syntax and Semantics, 2.3 Some Examples, 2.4 Hilbert Calculus

2. Sentential Logic (SL)

Vorlesung Nr. 4
Aufgezeichnet am 19.04.2016 | 7 Aufrufe

01:28:51

Vorlesung starten

Inhalt:
2.4 Hilbert Calculus, Resolution Calculus,

3. Verification I: LT properties

Vorlesung Nr. 5
Aufgezeichnet am 25.04.2016 | 3 Aufrufe

01:13:12

Vorlesung starten

Inhalt:
3.1 Motivation, 3.2 Basic transition systems, 3.3 Interleaving and handshaking

3. Verification I: LT properties

Vorlesung Nr. 6
Aufgezeichnet am 02.05.2016 | 2 Aufrufe

01:28:42

Vorlesung starten

Inhalt:
3.2 Basic transitions systems, 3.3 Interleaving and handshaking, 3.4 State-space explosions, 3.5 LT properties in gerneral

3. Verification I: LT properties

Vorlesung Nr. 7
Aufgezeichnet am 03.05.2016 | 0 Aufrufe

01:36:53

Vorlesung starten

Inhalt:
3.5 LT properties in general, 3.6 LTL

4. First-Order Logic: Semantics

Vorlesung Nr. 8
Aufgezeichnet am 09.05.2016 | 4 Aufrufe

01:31:41

Vorlesung starten

Inhalt:
4.1 Motivation, 4.2 FOL: Syntax, 4.3 FOL: Models, 4.4 Exampes: LTL and arithmetic

4. First-Order Logic: Semantics

Vorlesung Nr. 9
Aufgezeichnet am 23.05.2016 | 4 Aufrufe

01:20:24

Vorlesung starten

Inhalt:
4.1 Motivation, 4.2 FOL: Syntax, 4.3 FOL: Models, 4.4 Examples: LTL and arithmetic, 4.5 Prenex normal form and clauses

4. First-Order Logic: Semantics; 5. Verification II: Hoare calculus

Vorlesung Nr. 10
Aufgezeichnet am 30.05.2016 | 4 Aufrufe

01:27:27

Vorlesung starten

Inhalt:
4. First-Order Logic: Semantics: 4.5 Prenex normal form and clauses; 4.6 Sit-Calculus; 4.7 The Blocksworld; 4.8 Higher order logic. 5. Verification II: Hoare calculus: 5.1 Motivation; 5.2 Core Programming Language

5. Verification II: Hoare calculus

Vorlesung Nr. 11
Aufgezeichnet am 31.05.2016 | 1 Aufrufe

01:20:35

Vorlesung starten

Inhalt:
5.2 Core Programming Language; 5.3 Hoare Logic; 5.4 Proof Calculi: Partial Correctness

5. Verification II: Hoare calculus

Vorlesung Nr. 12
Aufgezeichnet am 06.06.2016 | 0 Aufrufe

01:06:49

Vorlesung starten

Inhalt:
5.4 Proof Calculi: Partial Correctness, 5.5 Proof Calculi: Total Correctnes, 5.6 Sound and Completeness

6. From FOL to PROLOG

Vorlesung Nr. 13
Aufgezeichnet am 13.06.2016 | 4 Aufrufe

01:21:03

Vorlesung starten

Inhalt:
6. Form FOL to PROLOG: 6.1 Motivation, 6.2 A calculus for FOL, 6.3 Resolution

6. Form FOL to PROLOG; 7. PROLOG

Vorlesung Nr. 14
Aufgezeichnet am 14.06.2016 | 1 Aufrufe

01:20:22

Vorlesung starten

Inhalt:
6. Form FOL to PROLOG: 6.4 Herbrand, 6.5 Variants of resolution, 6.6 SLD resolution; 7. PROLOG: 7.1 Motivation, 7.2 Syntax

7. Queries and Matching, PROLOG; Search Trees and Negation

Vorlesung Nr. 15
Aufgezeichnet am 20.06.2016 | 3 Aufrufe

01:32:45

Vorlesung starten

Inhalt:
7.3 Queries and Matching, Einführung PROLOG, Beispiele; 7.4 Search Trees and Negation, Beispiele

7. PROLOG

Vorlesung Nr. 16
Aufgezeichnet am 27.06.2016 | 0 Aufrufe

01:07:52

Vorlesung starten

Inhalt:
7.4 Search Trees and Negation; 7.5 Recursion and Lists; 7.6 Arithmetic; 7.7 Programming; Übung 6 und Übung 7

Hinweise zum Player

Bitte aktivieren Sie zur Wiedergabe JavaScript.


Impressum · Kontakt© TU Clausthal 2017