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-20 | Fortress: A New Programming Language for Scientific Computing Dr. Sukyoung Ryu,
Sun Microsystems Laboratories
[
slides
]
|
---|
2007-03-16 | Substitution Theorem Prof. Makoto Tatsuta,
National Institute of Informatics, Tokyo
[
slides
]
|
---|
2007-01-26 | A 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-07 | Software Protection : Validating Control Flow at Run Time Gyungho Lee,
Department of Electrical and Computer Engineering University,
University of Illinois at Chicago
[
slides
]
|
---|
2006-08-04 | Logical Interpretation of Selective CPS Transformation Hyeonseung Im,
Department of Computer Science and Engineering,
Pohang University of Science and Technology |
---|
2006-08-04 | A Polymorphic Type System for Staged Exceptions Hyunjun Eo,
School of Computer Science and Engineering,
Seoul National University
[
slides
]
|
---|
2006-08-04 | A Logic of Direct Evidence Sungwoo Park,
Department of Computer Science and Engineering,
Pohang University of Science and Technology |
---|
2006-08-04 | Challenge of Computer Mathematics Gyesik Lee,
INRIA,
Ecole Polytechnique |
---|
2006-04-07 | A 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-21 | Row Polymorphism and First-class Matches Matthias Blume, Toyota Technological Institute at Chicago |
---|
2006-01-10 | Toward a Grainless Semantics for Shared-Variable Concurrency John Reynolds, School of Computer
Science, Carnegie-Mellon University |
---|
2006-01-06 | A Next-Generation Platform for Analyzing Executables Junghee Lim, Department of Computer Science, University of Wisconsin-Madison |
---|
2005-07-06 | A programming language for probabilistic computation Sungwoo Park, School of Computer
Science, Carnegie-Mellon University |
---|
2005-03-11 | Proofs about folklore: why model checking = reachability? Nicolay V. Shilov, Division of Computer
Science, KAIST |
---|
2004-12-13 | Markov Chain Monte Carlo Algorithms Eric Vigoda, College of Computing, Georgia Institue of Technology |
---|
2004-09-16 | A Type Theory for Krivine-style Evaluation and Compilation Kwanghoon Choi, School of Information Science, Japan Advanced Institute of Science and Technology |
---|
2004-09-16 | A Logical Approach to Compiler Construction Atsushi Ohori, School of Information
Science, Japan Advanced Institute of Science and
Technology |
---|
2004-06-18 | Resources, Concurrency and Local Reasoning Peter W. O'Hearn, Department of Computer
Science, Queen Mary, University of London |
---|
2004-05-28 | ML-like Inference for Classifiers Cristiano Calcagno, Department of
Computing, Imperial College |
---|
2002-12-09 | The poisson cloning model for random k-SAT Jeong Han Kim,
Microsoft Research
|
---|
2002-11-22 | Complex System: Are Cells Like the Internet? Hawoong Jeong, Dept. of Physics, KAIST
[
slides
]
|
---|
2002-07-11 | Tutorial on Logical Relation and Relational Parametricity Uday S. Reddy, School of Computer Science, University of Birmingham |
---|
2002-06-25 | Tutorial on Separation Logic Peter W. O'Hearn, Department of Computer
Science, Queen Mary, University of London |
---|
2001-06-05 | Rewriting Logic and Maude:An Approach to Formal Methods Peter W.O'Hearn, CS,Stanford University |
---|
2001-05-31 | Oracle-Based Checking of Untrusted Software George Necula, EECS,UCBerkeley |
---|
2001-05-29 | An Introduction to Implicit Computational Complexity Luck Ong, Computing Laboratory,Oxford University
[
slides 1 / slides 2
]
|
---|
2001-05-28 | Game Semantics and Memory Management Luck Ong, Computing Laboratory,Oxford University |
---|
2001-04-30 | Types as Abstract Programes:Ageneric Type System for Concurrent Programs Naoki Kobayashi, Tokyo
Institute of Technology |
---|
2000-12-12 | Deterministic Java Replay Debugger for Jalapeno JVM Jongdeok Choi, IBM T.J.Watson |
---|
2000-12-01 | XML Overview and Research Issues Kyuseok Shim, Division of Computer Science, KAIST |
---|
2000-11-24 | The Functional Guts of the Kleisli Query System Limsoon Wong, Kent Ridge Digital Lab, and National Singapore University |
---|
2000-09-18 | Survey Workshop on Typeful Compilation ROPAS Members, Research On Program Analysis System, KAIST
[
web pages
]
|
---|
2000-07-19 | Parametricity 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-10 | Tutorial 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-21 | Tutorial on Program Logics Nikolay V. Shilov |
---|
2000-06-14 | An Overview of Abstract Interpretation and Program Static Analysis Patrick Cousot, ENS, Paris, France
[
slides
]
|
---|
2000-06-14 | Partial Completeness of Abstract Fixpoint Checking Patrick Cousot, ENS, Paris, France
[
paper
]
|
---|
2000-04-28 | Introduction to Computer Algebra Systems in Education Youngcook Jun, Department
of Computer Education, Sunchon National University,
Korea |
---|
2000-04-25 | Lambda-choice: a calculus for consistent alternatives Matthias
Blume, Research
Institute for Mathematical Sciences, Kyoto University,
Japan
[
paper
]
|
---|
2000-04-06 | Survey Workshop on Resource Bound Checking ROPAS Members, Research On Program Analysis System, KAIST
[
web page
]
|
---|
1999-11-19 | An 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-18 | An 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-03 | DSP Compiler Mission Improving ILP By Software Pipelining Gang-Ryung Uh, Lucent Technologies, U.S.A. |
---|
1999-11-01 | A framework for set-based analyses for Java Byeong-Mo Chang, Dept. of Computer Science, Sookmyung Women's University |
---|
1999-10-25 | Entropy and Sorting Jeong Han Kim, Microsoft Research, U.S.A. |
---|
1999-10-21 | Seminars on Program Logicx and Applications Nikolay Shilov, Institute of Informatics System, Russian Academy of Science, Russia |
---|
1999-08-26 | Theory of Domain Design in Abstract Interpretation Roberto Giacobazzi, Universita di Verona, Italy |
---|
1999-08-23 | Dependency Analysis for Assembly Languages Wolfram Amme, Fredrick-Schiller University Jena, Germany |
---|
1999-06-22 | Static Analysis in Optimizing Compilers for DSP Chips Luddy Harrison, Connected Components Corporation, U.S.A. |
---|
1999-04-06 | Seminars on Dependent Types in Practical Programming Hongwei Xi, Oregon Graduate Institute, U.S.A |
---|
1999-02-09 | Four talks on abstract interpretation of (constraint) logic programs Harald Sondergaard, The University of Melbourne, Australia |
---|
1999-01-26 | Workshop on LEGO (or calculus of constructions) Mino Bai, Dongduk Women's University
[
Randy Pollacks's Lecture Notes
]
|
---|
1998-12-07 | Word Problems, Pseudorecursive Varieties, And Multisorted Logic Dr. Dejan Delic, Department of Pure Mathematics, University of Waterloo, Canada |
---|
1998-06-25 | Type-Directed Specialization of Polymorphism; A Typed Context Calculus Atsushi Ohori, Research
Institute for Mathematical Sciences, Kyoto University,
Japan
[
web pages
]
|
---|
1997-11-10 | KAIST Abstract Interpretation Workshop Patrick Cousot, ENS, France
[
web page / Cousot's papers
]
|
---|
1995-12-29 | Our PL2401 meetings ROPAS Members
[
web page
]
|
---|