Lab Seminars
-
The software model checker BLAST(Refined version)
Kim, Yunho / 14 Jan, 2009 / [Presentation Material]
Original Paper : The software model checker BLAST: Applications ot software engineering by Dirk Beyer, Thomas A. Henzinger, Ranjit jhala and Rupak Majumdar, Int. Journal of Software Tools and Technology Transfer Vol 9 pp. 505-525, 2007
-
Bounded Model Checking of Concurrent Programs
Hong, Changki / 24 Dec, 2008 / [Presentation Material]
Original Paper : Bounded Model Checking of Concurrent Programs by Ishai Rabinovitz and Orna Grumberg, CAV 2005
-
Propositional Encodings
Hong, Changki / 9 Dec, 2008 / [Presentation Material]
Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
Deciding a Combination of Theories
Hong, Changki / 28 Nov, 2008 / [Presentation Material]
Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
The software model checker BLAST
Kim, Yunho / 12 Nov, 2008 / [Presentation Material]
Original Paper : The software model checker BLAST: Applications ot software engineering by Dirk Beyer, Thomas A. Henzinger, Ranjit jhala and Rupak Majumdar, Int. Journal of Software Tools and Technology Transfer Vol 9 pp. 505-525, 2007
-
Quantified Formulas
Hong, Changki / 7 Nov, 2008 / [Presentation Material]
Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems
Kim, Yunho / 5 Nov, 2008 / [Presentation Material]
Original Paper : Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems by Carla P. Gomes, Bart Selman, Nuno Crato and Henry Kautz, Journal of Automated Reasoning Vol 24 pp. 67-100, 2000
-
Pointer Logic
Hong, Changki / 31 Oct, 2008 / [Presentation Material]
Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
Thread-Modular Model Checking
Hong,Shin / 17 Oct, 2008 / [Presentation Material]
Original Paper: Thread-Modular Model Checking / Cormac Flanagan and Shaz Qadeer / SPIN worshop 2003
-
Arrays
Hong, Changki / 15 Oct, 2008 / [Presentation Material]
Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
Bit Vector
Hong, Changki / 10 Oct, 2008 / [Presentation Material]
Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
Evidence-Based Analysis Inferring Preconditions for Bug Detection
Hong, Shin / 3 Oct, 2008 / [Presentation Material]
Original Paper : Evidence-Based Analysis and Inferring Preconditions for Buf Detection by D.Brand, M.Buss and V.C.Sreedhar, ICSM 2007
-
Decision Procedures for Equality logic and Uninterpreted Functions and Linear Arithmetic
Hong, Changki / 3 Oct, 2008 / [Presentation Material]Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
How to fake an RSA signature by encoding modular root finding as a SAT problem
Kim, Yunho / 12 Sep, 2008 / [Presentation Material]Original Paper : How to fake an RSA signature by encoding modular root finding as a SAT problem by Claudia Fiorini, Enrico Martinelli, Fabio Massacci, Discrete Applied Mathematics 2003
-
Equality Logic and Uninterpreted Functions
Hong, Changki / 10 Sep, 2008 / [Presentation Material]Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
Decision procedures for propositional logic (BDDs)
Hong, Changki / 27 Aug, 2008 / [Presentation Material]Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
Decision procedures for propositional logic (SAT solver)
Hong, Changki / 20 Aug, 2008 / [Presentation Material]Textbook : Decision procedures An algorithmic Point of View by Daniel Kroening and Ofer Strichman, Springer
-
RacerX: Effective, Static Detection of Race Conditions and Deadlocks
Hong, Shin / 4 Jul, 2008 / [Presentation Material]
Original Paper : RacerX : Effective, Static Detection of Race Conditions and Deadlocks by Dawson Engler and Ken Ashcraft, SOSP03
-
Prameterized Unit Tests
Kim, Yunho / 29 Jul, 2008 / [Presentation Material]
Original Paper : Parameterized Unit Tests by Nikolai Tillmann and Wolfram Schulte, ESEC/FSE 2005
-
Bitstate Hashing
Kim, Yunho / 15 Jul, 2008 / [Presentation Material]
Original Papers & textbooks : The Spin Model Checker by Gerard J. Holzmann, Addison-Wesley, 2004
An Analysis of Bitstate Hashing by Gerard J. Holzmann, FMSD 1998
Fast and Accurate Bitstate Verification for SPIN by Peter C. Dillinger and Panagiotis Manolios, SPIN 2004
-
Boolean Programs : A Model and Process For Software Analysis
Kim, Yunho / 10 Jul, 2008 / [Presentation Material]
Original Paper : Boolean Programs : A Model and Process For Software Analysis by Thomas Ball and Sriram K. Rajamani, MSR-TR-2000-14
