2008 Jan-Jun

• Counterexample with Loops for Predicate Abstraction

  Kim, Yunho / 20 Jun, 2008 / [Presentation Material]

  Original Paper : Counterxample with Loops for Predicate Abstraction by Daniel Kroening and Georg Weissenbacher, CAV 2006 

• Counterexample-Guided Abstraction Refinement

     Kim, Yunho / 3 Jun, 2008 / [Presentation Material]

     Original Paper : Counterexample-Guided Abstraction Refinement by Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith, CAV, volume 1855 of LNCS, pages 154-169, Springer Verlag, 2000 

• Introduction of Principles of Program Analysis

      Hong,Changki / 24 Jun, 2008 / [Presentation Material]

      Principles of Program Analysis, by Flemming Nielson, Hanne Riis Nielson and Chris Hankin

• Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions

     Hong,Shin / 19 June, 2008 / [Presentation Material]

     Original paper: Checking System Rules using System-Specific, Programmer-Written Compiler Extensions, D. Engler et al, OSDI2000

• Programs: Semantics and Verification

      Hong,Changki / 18 Jun, 2008 / [Presentation Material]

      Mathematical Logic for Computer Science, by Mordechai Ben-Ari

• Concurrent Bug Patterns and How to Test Them

      Hong,Shin / 5 June, 2008 / [Presentation Material]

      Original paper: Concurrent Bug Patterns and How to Test Them, by Eitan Farchi, Yarden Nir, Shmuel Ur, PADTAD 2003

• An Introduction to PVS

      Hong,Changki / 4 Jun, 2008 / [Presentation Material]

      Original paper: A Tutorial Introduction to PVS by Judy Crow, Sam Owre, John Rushby, Natarajan Shankar and Mandayam Srivas, WIFT 1995

• Counterexample-Guided Abstraction Refinement

      Kim,Yunho / 3 Jun, 2008 / [Presentation Material]

      Original paper: Counterexample-Guided Abstraction Refinement by Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith, CAV 2000

• Generalized Symbolic Execution for Model Checking and Testing

      Hong,Changki / 13 May, 2008 / [Presentation Material]

      Original paper: Generalized Symbolic Execution for Model Checking and Testing by Sarfraz Khurshid, Corina S. Pasareanu, and    

      Willem Visser, TACAS 2003

• Predicate Abstraction of ANSI-C Programs Using SAT

      Kim,Yunho / 6 May, 2008 / [Presentation Material]

      Original paper: Predicate Abstraction of ANSI-C Programs Using SAT, FMSD 2004

• Symbolic Execution and Program Testing

      Hong,Changki / 1 May, 2008 / [Presentation Material]

      Original paper: Symbolic Execution and Program Testing by James C.King, Communications of the ACM 1976

• Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs

      Hong,Shin / 24 April, 2008 / [Presentation Material]

      Original paper: Atomizer: A Dynamic Atomicity Checker for Mulithreaded Programs by By Cormac Flanagan and Stephen N. Freund, POPL 2004

• Process Algebra

      Hong,Changki / 17 Apr, 2008 / [Presentation Material]

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

• Potential Deadlock Detection

      Hong,Shin / 2 April, 2008 / [Presentation Material]

      Original papers:

        Using runtime analysis to guide model checking of Java programs, Klaus Havelund, SPIN WORKSHOP 2000

        Detecting Potential Deadlocks with Static Analysis and Run-Time Monitoring, R. Agarwal L.Wang S.D.Stoller, HVC 2005

• Eraser: A Dynamic Data Race Detector for Multithreaded Programs

      Hong,Shin / 5 Mar, 2008 / [Presentation Material]

      Original paper: Eraser: A Dynamic Data Race Detector for Multithreaded Programs by Stefan Savage et al, ACM TOCS 1997

• Type-Based Race Detection for JAVA

     Hong,Shin / 22 Feb, 2008 / [Presentation Material]

     Original paper: Type-Based Race Detection for JAVA by Cormac Flanagan and Stephen N. Freund, PLDI 2000

• An Introduction to MiniSAT v1.14

    Kim,Yunho / 9 Jan, 2008 / [Presentation Material]

    Original paper: An Extensible SAT-solver by Niklas Een and Niklas Sörensson, SAT 2003