Personal tools
You are here: Home › Lab Seminar › 2007

2007

  • SPIN Search Optimization

     Hong,Shin / 23 Nov, 2007 / [Presentation Material]

     Original paper: Chapter 9 of "THE SPIN MODEL CHECKER" by G. J. Holzmann

  • SPIN Search Algorithm

     Hong,Shin/ 9 Nov, 2007 / [Presentation Material]

     Original paper: Chapter 8 of "THE SPIN MODEL CHECKER" by G. J. Holzmann

  • Symbolic Model Checking without BDDs

     Changbeom, Choi / 3 November, 2007 / [Presentation Material]

     Original paper: "Symbolic Model Checking without BDDs" by A. Biere et al

  • PROMELA Semantics

     Hong,Shin / 5 October, 2007 / [Presentation Material]

     Original paper: Chapter 7 of "THE SPIN MODEL CHECKER" by G. J. Holzmann

  • Introduction to SAT-problem for newbie

     Chang-Beom, Choi/ 7 September, 2007/ [Presentation Material]

     Original paper:

  • Program Monitoring with LTL in EAGLE by K Havelund et al

     Hong, Shin/ 8 August, 2007/ [Presentation Material]

     Original paper:

     Program Monitoring with LTL in EAGLE

      H Barringer, A Goldberg, K Havelund, K Sen, PADTAD'04

  • Efficient Decentralized Monitoring of Safety in Distributed Systems by K Sen et al

     Hong,Shin / 20 July, 2007 / [Presentation Material]

     Original paper:

     Efficient Decentralized Monitoring of Safety in Distributed Systems
     K Sen et al, ICSE'04

  • Game, Bisimulation, and Model Checking

     Chang-Beom, Choi / July 07, 2007 / [Office 2007] [Office 2003]

     Original paper : 
     Bisimulation, Model Checking and Other Games 
     by Colin Stirling, In Notes for Mathfit instructional meeting on games and computation, Edinburgh, June 1997

     Games and Model Mu-Calculus
     by Colin Stirling, In TACAS 1996 Lecture Notes in Computer Science 1055, 298-312, 1996

  • On the Semantics of Matching Trace Monitoring Patterns

     Hong,Shin / June 29, 2007 / [Presentation Material]

     Original paper : On the Semantics of Matching Trace Monitoring Patterns, RV2007, P Avgustinov, J Tibble, O Moor

  • About Alternating Automata

     Chang-Beom, Choi / June 06, 2007 / [Office 2007][Office 2003]

     Original paper : An Automata Theoretic Approach to Linear Temporal Logic by Moshe Y. Vardi In BANFF’94

  • Case Studies of POTA

     Hong, Shin / May 25, 2007 / [Presentation Material]

     Original paper : Alper Sen&Vijay K. Garg, Partial Order Trace Analyzer(POTA) for Distributed Programs

  • Survey on Trace Analyzers (2) : JMPaX and POTA

     Hong, Shin / May 11, 2007 / [Presentation Material]

     Original papers :

     (1)  Alper Sen & Vijay K. Garg, Formal Verification of Simulation Traces Using Computation Slicing, 2007.

     (2) K Sen et al, Runtime Safety Analysis of Multithreaded Programs, 2003.

  • Tranlation of Linear Temporal Logic formulae into Büchi Automata

     Choi, Chang-Beom / May 9, 2007 / [Presentation Material]
     Location : Rm. #4448 at CS. Dept.
     Original papers :

     On the Relation of Programs and Computations to Models of Temporal Logic
     by Pierre Wolper, In Proc. Temporal Logic in Specification, vol. 398 of LNCS, pages 75-123. Springer-Verlag, 1989.

     Constructing Automata from Temporal Logic Formulas: A Tutorial
     by Pierre Wolper In Lectures on Formal Methods in Performance Analysis, vol. 2090 of LNCS, pages 261-277. Springer-Verlag, July 2001.     
     Summary :

  • Survey on Trace Analyzers

     Hong,Shin / April 27, 2007 / [Presentation Material]
     Original papers : Doron Drusinsky, The Temporal Rover and the ATG Rover.
                                Klaus Havelund&Grigore Rosu, Java PathExplorer - A Runtime Verification Tool.
     Summary :

  • Recognizing Safety an Liveness

     Choi, Chang-Beom / April 20,2007 / [Presentation Material]
     Original paper: B. Aleprn and F. Schneider.  Recognizing Safety and Liveness . In Distributed Computing, Volume 2, Number 3, 1987.
     Summary :

  • The Model Checker SPIN

     Hong,Shin / April 17, 2007 / [Presentation Material]

     Original paper : Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, vol.23, No. 5, May 1997.

     Summary :

  • A Theory of Interactive Computation

     Choi, Chang-Beom / April 13, 2007 / [Presentation Material]

     Original paper : Jan van Leeuwen and Jiri Wiedermann. A Theory of Interactive Computation. In Interactive Computation: The New Paradiam.

     Summary :

  • Process Algebra : Calculus of Communicating Systems

     Choi, Chang-Beom / April 6, 2007 / [Presentation Material]

     Original paper : Rance Cleaveland and Scott A. Smolka. In Process Algebra.

     Summary :

Document Actions