EN | DE
Theoretische Informatik

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

ws18:fmsoft [2019/01/14 16:00]
tadeusz [Slides]
ws18:fmsoft [2019/02/12 19:15] (current)
tadeusz [Slides]
Line 13: Line 13:
  
   * {{:ws18:fmsoft:firstlectureoct16enc.pdf|The opening slides with sales talk}}   * {{:ws18:fmsoft:firstlectureoct16enc.pdf|The opening slides with sales talk}}
-  * {{:ws18:fmsoft_oct16handout.pdf|General introduction to model checking and temporal logic (16 Oct)}} +  * {{:ws18:fmsoft_oct16handout.pdf|General introduction to model checking and temporal logic (16 Oct)}}{{:ws18:fmsoft:fmsoft_oct16PRE.pdf|pre-lecture version}} 
-  * {{:ws18:fmsoft:fmsoft_oct23handout.pdf|Introducing LTL (23 Oct)}}+  * {{:ws18:fmsoft:fmsoft_oct23handout.pdf|Introducing LTL (23 Oct)}}{{:ws18:fmsoft:fmsoft_oct23PRE.pdf|pre-lecture version}}
   * {{:ws18:fmsoft:fmsoft_oct30_prelecture.pdf|Introducing CTL (30 Oct, pre-lecture version)}}   * {{:ws18:fmsoft:fmsoft_oct30_prelecture.pdf|Introducing CTL (30 Oct, pre-lecture version)}}
-  * {{:ws18:fmsoft:fmsoft_nov6pre.pdf|Recursive equations and fixpoints (6 Nov, pre-lecture version)}} +  * {{:ws18:fmsoft:fmsoft_nov6post.pdf|Introducing CTL (6 Nov, lecture version)}}{{:ws18:fmsoft:fmsoft_nov6pre.pdf|pre-lecture version}} 
-  * {{:ws18:fmsoft:fmsoft_nov13pre.pdf|Model checking for CTL (13 Nov, pre-lecture version)}} +  * {{:ws18:fmsoft:fmsoft_nov13post.pdf|Model checking for CTL (13 Nov, lecture version)}} {{:ws18:fmsoft:fmsoft_nov13pre.pdf|pre-lecture version}}  
-  * {{:ws18:fmsoft:fmsoft_nov20pre.pdf|Unifying CTL and LTL: CTL^* (20 Nov, pre-lecture version)}} +  * {{:ws18:fmsoft:fmsoft_nov20post.pdf|Unifying CTL and LTL: CTL^* (20 Nov, lecture version)}}{{:ws18:fmsoft:fmsoft_nov20pre.pdf|pre-lecture version}} 
-  * {{:ws18:fmsoft:fmsoft_nov27pre.pdf|Bounded model checking (27 Nov, pre-lecture version)}}+  * {{:ws18:fmsoft:fmsoft_nov27post.pdf|Bounded model checking (27 Nov, lecture version)}}{{:ws18:fmsoft:fmsoft_nov27pre.pdf|pre-lecture version}}
   * {{:ws18:fmsoft:fmsoft_dec4_post.pdf|Beginning Hoare logic (4 Dec, lecture version)}}   * {{:ws18:fmsoft:fmsoft_dec4_post.pdf|Beginning Hoare logic (4 Dec, lecture version)}}
-  * {{:ws18:fmsoft:fmsoft_dec11post.pdf|Frame your reasoning (11 Dec, lecture version)}}+  * {{:ws18:fmsoft:fmsoft_dec11post.pdf|Frame your reasoning (11 Dec, lecture version)}}{{:ws18:fmsoft:fmsoft_dec11pre.pdf|pre-lecture version}}
   * {{:ws18:fmsoft:fmsoft_dec18handout.pdf|Beginning denotational semantics (18 Dec, handout version)}}   * {{:ws18:fmsoft:fmsoft_dec18handout.pdf|Beginning denotational semantics (18 Dec, handout version)}}
   * {{:ws18:fmsoft:fmsoft_jan8post.pdf|Kleene Theorem and denotational semantics of loops (Jan 8)}}   * {{:ws18:fmsoft:fmsoft_jan8post.pdf|Kleene Theorem and denotational semantics of loops (Jan 8)}}
 +  * {{:ws18:fmsoft:fmsoft_jan15post.pdf|Weakest liberal preconditions and relative completeness (Jan 15)}}
 +  * {{:ws18:fmsoft:fmsoft_jan22post.pdf|Expressivity, total correctness, decorated programs (Jan 22)}}
 +  * {{:ws18:fmsoft:fmsoft_jan29post.pdf|Weakest preconditions in separation logic (Jan 29)}}{{:ws18:fmsoft:fmsoft_jan29pre.pdf|pre-lecture version}}
 +  * {{:ws18:fmsoft:fmsoft_feb5pre.pdf|Annotated programs and verification conditions in separation logic (Feb 5, handout version)}}