Address

Jakob-Haringer-Str. 2

5020 Salzburg, Austria


Room 2.17


Phone

+43 (0)662 8044 6417

+43 (0)662 8044 611 (fax)


Skype ana_sokolova

Home

Papers

Talks

Teaching

Personal

Many thanks to Silviu Craciunas for the photo (RTAS 2010 in Stockholm) and his help with iWeb!

Theoretical Computer Science 911.024/025, Summer semester 2018

Schedule:           Thursdays 10am-1pm

                            starting 1.3.2018 in T03 see calendar


First meeting:       Thursday, March 1 at 10am in T03


Language:           English


Office hours:       Tuesdays 11am-12am 


Instructions:       Wednesdays 11am-1pm in T03

Literature: Reading material will be suggested in the schedule below -- each week after class, related to the covered topic.

Prerequisites:  Knowledge of the material covered by basic theory courses that are part of bachelor studies in computer science.

Exam:   The exam for the lecture part (911.024) is written. It consist of several exercises from the material covered during the course. There will be three exam possibilities (in July, September, and November).


In order to pass via one of the exam possibilities one needs to have 55% of the maximal points available at the exam. That is, if the exam brings maximally 100 points, in order to pass one needs to have at least 55 points.


The grade for the instructions (PS) part (911.025) will depend on the presentation / mini project. See information below.


Exam dates: August 10 at 10am (room t.b.a.)  and September 20 at 2p (room t.b.a.)

Course description:  This is an obligatory master course on selected topics in theoretical computer science: logic in computer science, verification methods, semantics. In this course we will learn the basics of formal methods, by focusing on selected topics. In particular we will learn different logics for reasoning about programs and systems, formal models of (software) systems, several basic verification techniques, semantic equivalences for fighting state-space explosion, decision procedures and the foundations of proof assistants and automated theory provers.

Slides:  Whenever slides are used, they will be made available on this webpage. The slides are by no means complete and only serve as help for better presentation. More material is covered during the class (on the blackboard) than visible on the slides.

Schedule (lectures):


Due to traveling, we will not meet every Thursday, but in the weeks when we meet we will do 180 min of lectures. That means starting at 10:00am and ending at 1:15pm with a 15min break in the middle.


  1. •March 1: Introduction and Hoare triples for program verification. Slides for week 1. We proved the correctness of the Euclidean algorithm. Your homework assignment is on the last slide. Moreover, you are asked to pick a small well-known program of 10-20 lines of code and verify its correctness using Hoare Logic as another homework assignment. Reading material: please check the following links (and maybe links there further):
    https://en.wikipedia.org/wiki/Hoare_logic
    https://www.cs.cmu.edu/~aldrich/courses/654-sp07/slides/7-hoare.pdf
    https://www.cs.cmu.edu/~aldrich/courses/654-sp09/notes/3-hoare-notes.pdf
    https://cs.stanford.edu/people/eroberts/courses/soco/projects/2008-09/tony-hoare/logic.html
    https://users-cs.au.dk/amoeller/talks/hoare.pdf


        and of course the original paper by Hoare: https://dl.acm.org/citation.cfm?doid=363235.363259


  1. •March 8: Models and Logics. We learned how to model reactive systems and programs; learned LTS, Kripke structures, the equivalence of state-labelled vs transition-labelled models, discussed examples.
    Good reading material for this part is Chapter 2 of the book: Model Checking by E.M. Clarke, O. Grumberg, and D.A.Peled [MC]
    as well as Section 2.2.1 from the book: Reactive Systems by L. Aceto, A. Ingolfsdottir, K.G. Larsen, and J. Srba [RS]

    Then we discussed dynamic (program) logics in general, and focused on Hennessy-Milner Logic.
    Good reading material for this part is Section 5.1 from [RS]

    I will also send you my lecture notes per email as well as a set of homework taks for the next PS session (on March 15).

  2. •March 15: We continued with some more examples and properties of HML, and then turned to temporal logics (LTL and CTL via CTL*) used in model checking. We discussed examples, the expressive power of the logics and their limitations.
    Good reading material for this part is Chapter 3 of [MC] as well as any other source on temporal logics, including wikipedia articles.

    I will send you my lecture notes and the slides that we used in class, as well as a set of homework tasks for the next PS session (on April 11) per email.

  3. •April 12: We still proved one property that was in the HW tasks for April 11, but we did not manage to do yesterday (the caracterisation of “releases”). Next we discussed CTL in more detail, as we did not manage to do all that last time. Then we had a very high-level overview of all classical model checking algorithms, as well as more recent approaches. Finally, we discussed bounded model checking in detail (but did not manage to give the encoding fully -- we will do this next time).

    I will send you reading material via email, as well as an assignment for the next instruction class (on April 25).

  4. •April 26: First, Arno Wilhelm-Weidner visited us and presented the study in which we will all take place (on learning tools). For this occasion we also have new participants in the course -- thanks a lot (to all bachelor students and members of our group for helping out and taking part -- it will be fun :-)). Then we finished discussing the BMC encodings into SAT, and changed to a new (old) topic: Automata. We made a brief recalling of all of standard automata theory, with proof (sketch) of Kleene’s theorem and discussion of Kleene algebra. After dealing with the topics related to Arno’s study, we will return to automata on infinite words. Sorry for the non-straightforward line of topics, the schedule is fixed due to the study.

    In the instuctions on April 25 we went through some CBMC examples. This was interesting and lead to nice student presentations as well as useful discussion.

    I will send you reading material, slides of today, and assignments for the next instruction class (on May 2) per email.

  5. •May 3: This is the first class related to Arno’s study and in the larger group. We did behavioral equivalences (trace, bisimilarity, weak bisimilarity) and briefly preorders (trace, simulation, weak simulation), with emphasis on motivation and examples, but we also proved some properties. We followed the book [RS], Chapter 3. We also did the game characterization of bisimilarity.
    We also brifly mentioned basics of CCS, in order that you can follow some examples in the book when you read the material.

    In the instuctions on May 2 we solved the homework tasks on automata, from last week. This was a very nice class with lot of student activity and discussions on the board.

    The reading material of today is [RS] Chapter 3.  I will send you some assignments for the next instruction class (on May 9) per email.


  1. •May 17: The second class related to Arno’s study and in the larger group. We did fixed points, bisimilarity as a fixed point, with proofs and examples. We followed the book [RS], Chapter 4. Please fill in Arno’s second survey.

    In the instuctions on May 9 we solved the homework tasks on behavioural equivalences, from last time.

    The reading material of today is [RS] Chapter 4.  I will send you some assignments for the next instruction class (on May 30) per email. Our next lecture is on June 7 (due to traveling and public holidays).

  2. •June 8: Applications of fixed points in computer science. We discussed various examples: the semantics of CTL formulas via fixed points, recursive definition of a language, transitive closure, and denotational semantics of recursive programs. I will send you lecture notes via email.

    In the exercise session on May 30 we solved the tasks related to fixed points from [RS] Chapter 4 that I have sent you the week before.


  1. •June 14: We used this class as well as the PS class on June 13 for the first two student talks sessions. Also in the PS class on June 20 and June 27 we had further student talks. All student talks were very nice with long discussions.

  2. •June 21: Semantics for Concurrency. This was a nice class where I gave  tutorial on semantics for concurrency and an overview of the work that I and we (in the group) have done on concurrent data structures. I will present this and more in several weeks at MOVEP 2018 (summer school). I will send you the slides via email.


  1. •June 28: Last meeting, Q&A session. We discussed the sample exam problems that I sent you via email, and anything else that popped up as a question.



Ana Sokolova

Dr. TU Eindhoven, The Netherlands, 2005



Associate Professor


Computational Systems Group

Department of Computer Sciences

University of Salzburg

Austria


anas@cs.uni-salzburg.at

Instructions and homework:  Each week in the lectures you will be given small homework assignment, to help you check if you understood the topic that we dealt with in class. These excersises can / will be discussed in the instructions sessions, or in the office hours. We will also select papers to read / tools to experiment with, and use them as assignments for the instruction hours. The instruction hours will be blocked towards the end of the semester, and each student will give a one hour presentation on a selected paper or tool.