Formal Systems (DAT5, Autumn'07)

• To provide a deeper understanding of advanced topics within the area.
• To support the project work.
• To teach students how to present and assess academic research papers.

• An interesting beamer guide
  
  
• Henrik's modification of the Frankfurt theme:
  
  \mode<presentation>
  {
  \usetheme{Frankfurt}
  \usecolortheme{seahorse}
  \setbeamercovered{transparent}
  \setbeamertemplate{blocks}[rounded][shadow=true]
  \setbeamercolor{block title}{fg=black,bg=structure.fg!25!white}
  \setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
  }
  

Plan of Presentations

• 6.9.2007, Room 0.1.12, 9:00 to 12:00: Introduction to formal systems by Kim; introduction to paper presentation by Jiri. Slides on how to read a paper and give a presentation are here.
• 14.9.2007, Room 0.1.12, 9:00 to 12:00: Paper presentation session (35 minutes each presentation)
  • Joakim Byg; chair: Henrik; A Survey of Regular Model Checking by P.A. Abdulla, B. Jonsson, M. Nilsson and M. Saksena. [Slides]
  • Kenneth Yrke Joergensen; chair: Thomas; Abstract Regular Model Checking by A. Bouajjani, P. Habermehl and T. Vojnar.
  • Willard Rafnsson; chair: Robert; Mobile Values, New Names, and Secure Communication by M. Abadi and C. Fournet. [Slides]
• 24.9.2007, Room 0.1.12, 9:00 to 12:00: Paper presentation session (35 minutes each presentation)
  • Thomas Boegholm; chair Kenneth; Moby/RT: A Tool for Specification and Verificaltion of Real-Time Systems
  • Henrik Kragh-Hansen; chair Arild; TIMES: a Tool for Schedulability Analysis and Code Generation of Real-Time Systems [Slides]
• 2.10.2007, Room 0.1.12, 9:00 to 12:00: Paper presentation session (35 minutes each presentation)
  • Petur Olsen; chair Joakim; SaveCCM: An Analysable Component Model for Real-Time Systems [Slides]
  • Robert J. Olesen; chair Jacob; Automatic Verification of Real-time Systems with Discrete Probability Distributions [Slides]
  • Arild M. M. Haugstad; chair Willard; A logic for Reasoning about Time and Reliability [Slides]
• 8.10.2007, Room 0.1.12, 9:00 to 12:00: Paper presentation sessions (35 minutes each presentation)
  • Joakim Byg; chair: Henrik; Regular Model Checking Made Simple and Efficient by P.A. Abdulla, B. Jonsson, M. Nilsson and J. Orso. [Slides]
  • Kenneth Yrke Joergensen; chair: Thomas; Iterating Transducers in the Large by B. Boigelot, A. Legay and P. Wolper.
  • Willard Rafnsson; chair: Robert; A Semantics for a Logic of Authentication by M. Abadi and M. R. Tuttle.
• 12.10.2007, Room 0.1.12, 9:00 to 12:00: Paper presentation sessions (35 minutes each presentation)
  • Petur Olsen; chair Joakim; Automatic Predicate Abstraction of C Programs [Slides]
  • Henrik Kragh-Hansen; chair Arild; Bandera: Extractiong Finite-State Models from Java Source Code [Slides]
• 2.11.2007, Room 0.1.12, 8:15 to 11:15: Paper presentation session (35 minutes each presentation)
  • Thomas Boegholm; chair Kenneth; Lazy Abstraction
  • Robert J. Olesen; chair Petur; Polynomial Time Algorithms for Testing Probabilistic Bisimulation and Simulation [Slides]
  • Arild M. M. Haugstad; chair Willard; Bisimulation Through Probabilistic Testing
• 9.11.2007, Room 0.1.12, 9:00 to 12:00: Paper presentation session
  Sections 1.1, 1.3, 1.5, 1.6 and 1.7.
  • Joakim Byg; chair: Henrik; Abstract Regular Tree Model Checking of Complex Dynamic Data Structures.
  • Willard Rafnsson; chair: Robert; Deciding Knowledge in Security Protocols under Equational Theories. [Slides]
• 16.11.2007, Room 0.1.12, 8:15 to 11:15 : Paper presentation session
  • Arild M. M. Haugstad; chair Willard; Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach
  • Robert J. Olesen; chair Petur; A Markov Reward Model Checker and How Fast and Fat Is Your Probabilistic Model Checker? [Slides]
  • Kenneth Yrke Joergensen; chair: Thomas; Tree Automata Techniques and Applications, Sections 1.1, 1.3, 1.6 and 1.7.
• 3.12.2007, Room 0.1.12, 13:00 to 14:30: Kim will conclude the course by a talk: Verification: From Theory to Tools