2010-01-05 The Linear Temporal Logic of Rewriting Model Checker in Maude
Kyungmin Bae , Univ. of Illinois at Urbana-Champaign
2009-12-23 Constrained Environment Inference for Verification of Multi-Threaded Programs
Corneliu Popeea , Max Plank Institute for Software Systems
2009-12-22 Local Reasoning for Read-Copy-Update
Hongseok Yang , Queen Mary, Univ. of London [ talk slide ]
2009-12-16 Types and Recursion Schemes for Higher-Order Program Verification
Naoki Kobayashi , Tohoku University [ talk slide ]
2009-12-15 The Twilight Zone: from testing to formal specifications and back again
Koen Claessen , Chalmers University of Technology, Gothenburg, Sweden [ talk slide ]
2009-12-14 The Sketching Approach to Program Synthesis
Armando Solar-Lezama , Massachusetts Institute of Technology [ talk slide ]
2009-12-13 Parallel Programming in Fortress
Sukyoung Ryu , Computer Science, KAIST [ talk slide 1 / talk slide 2 ]
2009-12-13 Separation Logic from the Perspective of Program Analysis
Hongseok Yang , Queen Mary, University of London [ talk slide 1 / talk slide 2 ]
2009-11-06 Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
Keiko Nakata , Tallinn University of Technology [ talk slide ]
2009-10-29 An Evolution-Centric Perspective on Software Testing
Gregg Rothermel , University of Nebraska-Lincoln [ talk slide ]
2009-10-29 Automated Verification via Separation Logic
Cristina David , National University of Singapore [ talk slide ]
2009-10-14 Logical Relations and Compositional Compiler Correctness
Chung-Kil Hur , University of Cambridge [ talk slide ]
2009-09-08 Type Checking Program Generators Using the Record Calculus
Tankut Baris Aktemur , Ozyegin University, Turkey
2009-09-05 Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction
Bow-Yaw Wang , Institute of Information Science, Academia Sinica [ talk slide ]
2009-09-05 Comparative Study on Software Model Checkers as Unit Testing Tools based on an Industrial Case Study
Moonzoo Kim , Computer Science, KAIST [ talk slide ]
2009-08-31 Survey Workshop on Corpus-based Shape Analysis
ROPAS Members, Research on Corpus-based Shape Analysis , SNU [ web page ]
2009-08-31 Components and Static analysis
Bruno Oliveira , ROSAEC Center [ talk slide ]
2009-07-30 Approximate Inference: Decomposition Methods with Applications to Computer Vision
Kyomin Jung , Computer Science, KAIST [ talk slide ]
2009-07-08 A Brief Overview Assume-Guarantee Reasoning via Learning
Bow-Yaw Wang , Institute of Information Science, Academia Sinica [ talk slide ]
2009-06-19 Interactive proving and programming in Coq
Hugo Herbelin , INRIA, France [ talk slide ]
2009-06-02 WYSINWYX: What You See Is Not What You eXecute
Gogul Balakrishnan , NEC Laboratories America, Inc. [ talk slide ]
2009-05-12 Bi-abductive inference for reasoning about heaps
Peter O'Hearn , Queen Mary, University of London [ talk slide ]
2009-05-11 From Separation Logic to Systems Code
Peter O'Hearn , Queen Mary, University of London [ talk slide ]
2009-04-30 Symbolic Model Checking Property Specification Language
Ji Wang , National University of Defense Technology, China [ talk slide ]
2009-04-17 소형무인헬기용 임베디드 소프트웨어의 구조와 적용
김두현 , 건국대학교 인터넷미디어공학부 [ talk slide ]
2009-04-10 Relationship between Curry-Howard-correspondence and semantics
Gyesik Lee , ROSAEC Center [ talk slide ]
2009-02-13 Survey Workshop on Static Analysis of Binary Code
MES Lab. Members , SNU
2009-02-04 Survey Workshop on Static Analysis for Malware Detection
SE Lab. Members , SNU
2009-01-21 Domain-Specific Abstract Interpretations : Experience Reports
Jerome Feret , INRIA/ENS/CNRS, France [ speaker's page ]
2009-01-17 Survey Workshop on Class Analysis
ROPAS Members, Research On Program Analysis System , SNU [ web page ]
2009-01-14 P2P Botnet Enumeration and Banking Trojan Crimwares
Byung-Hoon Kang , University of North Carolina at Charlotte [ talk slike / paper ]
2008-12-30 Randomized Active Testing for Concurrent Programs
Chang-Seo Park , UC Berkeley [ slides ]
2008-12-24 Shared Subtypes : Subtyping recursive parameterized algebraic data types
Ki-Yung Ahn , Portland State University [ slides ]
2008-12-12 Alleviating False Alarm Problem of Static Buffer Overflow Analysis
Youil Kim , KAIST [ slides ]
2008-11-19 Analyzing and Inferring the Structure of Code Changes
Il-Chul Moon , Chrnegie Mellon University [ slides ]
2008-11-17 Analyzing and Inferring the Structure of Code Changes
Miryung Kim , University of Texas, Austin [ slides ]
2008-10-01 Statistical Machine Translation
Changbum Park , Seoul National University [ slides ]
2008-09-30 Abstract Interpretation and Application to the Static Analysis of Safety-Critical Embedded Computer Software
Patrick Cousot , ENS, France [ web page ]
2008-07-17 Predicting Bugs by Analyzing Software History
Dr. Sunghun Kim , Seoul National University [ slides ]
2008-06-18 Typical Error Patterns in C++
김의석 이사 , SVD [ slides ]
2008-02-19 Effective Pointer Error Detection using Shape Analysis
Prof. Oukseh Lee , Hanyang University [ slides ]
2007-05-29 Model Checking, From Hardware To Software And Back Again
Prof. Edmund M. Clarke , Carnegie Mellon University [ slides ]
2007-03-22 Program Validation by Symbolic and Reverse Execution
Dr. Jooyong Lee , BRICS, University of Aarhus, Aarhus, Denmark [ slides ]
2007-03-20Fortress: A New Programming Language for Scientific Computing
Dr. Sukyoung Ryu, Sun Microsystems Laboratories [ slides ]
2007-03-16Substitution Theorem
Prof. Makoto Tatsuta, National Institute of Informatics, Tokyo [ slides ]
2007-01-26A Modal Type System for Multi-Level Generating Extensions with Persistent Code
Prof. Atsushi Igarashi, Department of Intelligence Science and Technology, Graduate School of Informatics, Kyoto University
2006-08-07Software Protection : Validating Control Flow at Run Time
Gyungho Lee, Department of Electrical and Computer Engineering University, University of Illinois at Chicago [ slides ]
2006-08-04Logical Interpretation of Selective CPS Transformation
Hyeonseung Im, Department of Computer Science and Engineering, Pohang University of Science and Technology
2006-08-04A Polymorphic Type System for Staged Exceptions
Hyunjun Eo, School of Computer Science and Engineering, Seoul National University [ slides ]
2006-08-04A Logic of Direct Evidence
Sungwoo Park, Department of Computer Science and Engineering, Pohang University of Science and Technology
2006-08-04Challenge of Computer Mathematics
Gyesik Lee, INRIA, Ecole Polytechnique
2006-04-07A Modal Language for the Safety of Mobile Values
Sungwoo Park, Department of Computer Science and Engineering , Pohang University of Science and Technology [ slides ]
2006-03-21Row Polymorphism and First-class Matches
Matthias Blume, Toyota Technological Institute at Chicago
2006-01-10Toward a Grainless Semantics for Shared-Variable Concurrency
John Reynolds, School of Computer Science, Carnegie-Mellon University
2006-01-06A Next-Generation Platform for Analyzing Executables
Junghee Lim, Department of Computer Science, University of Wisconsin-Madison
2005-07-06A programming language for probabilistic computation
Sungwoo Park, School of Computer Science, Carnegie-Mellon University
2005-03-11Proofs about folklore: why model checking = reachability?
Nicolay V. Shilov, Division of Computer Science, KAIST
2004-12-13Markov Chain Monte Carlo Algorithms
Eric Vigoda, College of Computing, Georgia Institue of Technology
2004-09-16A Type Theory for Krivine-style Evaluation and Compilation
Kwanghoon Choi, School of Information Science, Japan Advanced Institute of Science and Technology
2004-09-16A Logical Approach to Compiler Construction
Atsushi Ohori, School of Information Science, Japan Advanced Institute of Science and Technology
2004-06-18Resources, Concurrency and Local Reasoning
Peter W. O'Hearn, Department of Computer Science, Queen Mary, University of London
2004-05-28ML-like Inference for Classifiers
Cristiano Calcagno, Department of Computing, Imperial College
2002-12-09The poisson cloning model for random k-SAT
Jeong Han Kim, Microsoft Research
2002-11-22Complex System: Are Cells Like the Internet?
Hawoong Jeong, Dept. of Physics, KAIST [ slides ]
2002-07-11Tutorial on Logical Relation and Relational Parametricity
Uday S. Reddy, School of Computer Science, University of Birmingham
2002-06-25Tutorial on Separation Logic
Peter W. O'Hearn, Department of Computer Science, Queen Mary, University of London
2001-06-05Rewriting Logic and Maude:An Approach to Formal Methods
Peter W.O'Hearn, CS,Stanford University
2001-05-31Oracle-Based Checking of Untrusted Software
George Necula, EECS,UCBerkeley
2001-05-29An Introduction to Implicit Computational Complexity
Luck Ong, Computing Laboratory,Oxford University [ slides 1 / slides 2 ]
2001-05-28Game Semantics and Memory Management
Luck Ong, Computing Laboratory,Oxford University
2001-04-30Types as Abstract Programes:Ageneric Type System for Concurrent Programs
Naoki Kobayashi, Tokyo Institute of Technology
2000-12-12Deterministic Java Replay Debugger for Jalapeno JVM
Jongdeok Choi, IBM T.J.Watson
2000-12-01XML Overview and Research Issues
Kyuseok Shim, Division of Computer Science, KAIST
2000-11-24The Functional Guts of the Kleisli Query System
Limsoon Wong, Kent Ridge Digital Lab, and National Singapore University
2000-09-18Survey Workshop on Typeful Compilation
ROPAS Members, Research On Program Analysis System, KAIST [ web pages ]
2000-07-19Parametricity Semantics of Symmetric Noninterference
Hongseok Yang, Dept. of Computer Science, UIUC, USA (also associated with School of Computer Science, Univ. of Birmingham, UK) [ slides ]
2000-07-10Tutorial on Twelf and LLF
Jeff Polakow, School of Computer Science, Carnegie Mellon Univeristy, USA [ 7-10 slides / 7-11 slides / 7-14 slides 1/2 / 7-14 slides 2/2 / Mini-ML Elf code / MLR Llf code ]
2000-06-21Tutorial on Program Logics
Nikolay V. Shilov
2000-06-14An Overview of Abstract Interpretation and Program Static Analysis
Patrick Cousot, ENS, Paris, France [ slides ]
2000-06-14Partial Completeness of Abstract Fixpoint Checking
Patrick Cousot, ENS, Paris, France [ paper ]
2000-04-28Introduction to Computer Algebra Systems in Education
Youngcook Jun, Department of Computer Education, Sunchon National University, Korea
2000-04-25Lambda-choice: a calculus for consistent alternatives
Matthias Blume, Research Institute for Mathematical Sciences, Kyoto University, Japan [ paper ]
2000-04-06Survey Workshop on Resource Bound Checking
ROPAS Members, Research On Program Analysis System, KAIST [ web page ]
1999-11-19An Illustration of Partial Evaluation through the Euclidean Algorithm; Issues behind a research paper
Olivier Danvy, Basic Research In Computer Science(BRICS), University of Aarhus, Denmark [ slides ]
1999-11-18An Extensional Characterization of Lambda-Lifting and Lambda-Dropping; Formalizing Implementation Strategies for First-Class Continuations
Olivier Danvy, Basic Research In Computer Science(BRICS), University of Aarhus, Denmark [ slides / slides ]
1999-11-03DSP Compiler Mission Improving ILP By Software Pipelining
Gang-Ryung Uh, Lucent Technologies, U.S.A.
1999-11-01A framework for set-based analyses for Java
Byeong-Mo Chang, Dept. of Computer Science, Sookmyung Women's University
1999-10-25Entropy and Sorting
Jeong Han Kim, Microsoft Research, U.S.A.
1999-10-21Seminars on Program Logicx and Applications
Nikolay Shilov, Institute of Informatics System, Russian Academy of Science, Russia
1999-08-26Theory of Domain Design in Abstract Interpretation
Roberto Giacobazzi, Universita di Verona, Italy
1999-08-23Dependency Analysis for Assembly Languages
Wolfram Amme, Fredrick-Schiller University Jena, Germany
1999-06-22Static Analysis in Optimizing Compilers for DSP Chips
Luddy Harrison, Connected Components Corporation, U.S.A.
1999-04-06Seminars on Dependent Types in Practical Programming
Hongwei Xi, Oregon Graduate Institute, U.S.A
1999-02-09Four talks on abstract interpretation of (constraint) logic programs
Harald Sondergaard, The University of Melbourne, Australia
1999-01-26Workshop on LEGO (or calculus of constructions)
Mino Bai, Dongduk Women's University [ Randy Pollacks's Lecture Notes ]
1998-12-07Word Problems, Pseudorecursive Varieties, And Multisorted Logic
Dr. Dejan Delic, Department of Pure Mathematics, University of Waterloo, Canada
1998-06-25Type-Directed Specialization of Polymorphism; A Typed Context Calculus
Atsushi Ohori, Research Institute for Mathematical Sciences, Kyoto University, Japan [ web pages ]
1997-11-10KAIST Abstract Interpretation Workshop
Patrick Cousot, ENS, France [ web page / Cousot's papers ]
1995-12-29Our PL2401 meetings
ROPAS Members [ web page ]