Logo ČVUT
ČESKÉ VYSOKÉ UČENÍ TECHNICKÉ V PRAZE
STUDIJNÍ PLÁNY
2020/2021

Computer Assisted Formal Reasoning

Předmět není vypsán Nerozvrhuje se
Kód Zakončení Kredity Rozsah
PI-CFR ZK 4 3C
Přednášející:
Cvičící:
Stefan Ratschan (gar.)
Předmět zajišťuje:
katedra číslicového návrhu
Anotace:

The goal of this course is to provide the student with the ability to

- completely formalize research problems in the field of their Ph.D. study, to

- prove the correctness of solutions to such problems, and to

- prepare the resulting proofs for publication,

while supporting this process using state-of-the-art software tools.

The course will take the form of consultations. The teacher will work with the student on

concrete research problems from the student's field of research.

Požadavky:

Prerequisites:

- The student must have completed a basic course in logic (e.g., BI-MLO).

- The student already has some preliminary results in the field of his or her research.

Osnova přednášek:

List of topics:

1. natural deduction proof calculus

2. logical theories, decision procedures, and SMT solvers

3. model checking

4. algorithm verification

5. interactive proof assistants (e.g., Isabelle, Coq)

6. formal modeling and abstraction

7. proofs in technical writing

Osnova cvičení:
Cíle studia:

The objective of this course is different from all courses at bachelor or master‘s level,

concentrating on skills for scientific research instead of skills for industrial practice. While

some topics do have some overlap (MI-TES: model checking, MI-FME: natural deduction,

algorithm verification), the focus on the process and artifacts of scientific research results in

an entirely different approach to those topics.

Studijní materiály:

- John Harrison: Handbook of Practical Logic and Automated Reasoning, Cambridge

University Press, 2009

- Michael Huth and Mark Ryan: Logic in Computer Science, Cambridge University

Press, 2004

- Daniel Kroening and Ofer Strichman. Decision procedures. Springer-Verlag Berlin

Heidelberg, 2016.

Poznámka:
Další informace:
Pro tento předmět se rozvrh nepřipravuje
Předmět je součástí následujících studijních plánů:
Platnost dat k 18. 1. 2021
Aktualizace výše uvedených informací naleznete na adrese http://bilakniha.cvut.cz/cs/predmet6323506.html