Reading Group: Seminal Papers in Verification (and Related Topics)

Table of Contents

1 General Information

1.1 Schedule

DateLocationNameTopicSlidesAttending
2012-02-03 FriP1213JariIntroduction
2012-02-10 FriP1146JariApt: Ten years of Hoare's logic: A survey — part ILinkCarl, Stavros, Yunyun, Andreina, Johannes, Fred, Othmane, Jonathan, Jari
2012-02-17 FriP1112JoeClarke et al.: Automatic verification of finite-state concurrent systems using temporal logic specificationsLink, Some material taken from these slidesEveryone
2012-02-24 FriP1113CarlVardi & Wolper: An automata-theoretic approach to automatic program verificationLinkSofia, Stavros, Joe, Andreina, Yunyun, Jari, Othmane, Ramunas, Johannes, Jonathan, Carl
2012-03-09 Fri 14:00P1112SofiaBryant: Graph-based algorithms for boolean function manipulationLink Additional material: (1, 2)
2012-03-23 FriP1112AndreinaClarke et al.: Symbolic model checking: \(10^{20}\) states and beyondLinkJonathan, Joe, Stavros, Yunyun, Ramunas, Johannes, Jari, Carl, Othmane, Sofia, Andreina
2012-04-13 FriP1145YunyunLamport: Time, clocks, and the ordering of events in a distributed systemLinkJonathan, Joe, Andreina, Sofia, Carl, Othmane, Jari, Johannes, Ramunas, Yunyun
2012-04-20 FriP1145JonathanSMT: Introduction and Applications (not a seminal paper, but a very good overview of SMT)LinkAndreina, Jonathan, Joe, Yunyun, Stavros, Carl, Jari, Othmane, Ramūnas
2012-05-11 FriP1112RamūnasReynolds: Separation logic: A logic for shared mutable data structuresLinkEveryone
2012-05-18 FriP1112StavrosClarke et al.: Symbolic model checking without BDDsLinkCarl, Jari, Yunyun, Ramunas, Stavros, Othmane, Joe
2012-06-01 FriP1112JohannesSangiorgi: An introduction to bisimulation and coinductionLinkJohannes, Jonathan, Stavros, Joe, Andreina, Othmane, Jari, Yunyun
2012-06-08 FriP1112OthmaneClarke et al.: Counterexample-guided abstraction refinement for symbolic model checkingLink

1.3 Exercises

1.3.1 Hoare Logic

Link

1.3.2 CTL

Link (if you want, use the LaTeX source)

1.3.3 LTL Model Checking

Link

1.3.4 BDDs

Link

1.3.5 Symbolic Model Checking

Link

1.3.6 Lamport

Link

1.3.7 SMT

Link

1.3.8 Separation Logic

Link

1.3.9 Bounded Model Checking

Link

1.3.10 Bisimulation

Link

1.3.11 CEGAR

Link

2 List of Papers

Apt: Ten years of Hoare's logic: A survey — part ILink
Clarke et al.: Automatic verification of finite-state concurrent systems using temporal logic specificationsLink
Vardi & Wolper: An automata-theoretic approach to automatic program verificationLink
Bryant: Graph-based algorithms for boolean function manipulationLink
Clarke et al.: Symbolic model checking: \(10^{20}\) states and beyondLink
Lamport: Time, clocks, and the ordering of events in a distributed systemLink
SMT: Introduction and Applications (not a seminal paper, but a very good overview of SMT)Link
Reynolds: Separation logic: A logic for shared mutable data structuresLink
Clarke et al.: Symbolic model checking without BDDsLink
Clarke et al.: Counterexample-guided abstraction refinement for symbolic model checkingLink
Sangiorgi: An introduction to bisimulation and coinductionLink

Date: 2012-06-11 01:27:15 CEST

Author: Jari Stenman

Org version 7.8.03 with Emacs version 24

Validate XHTML 1.0