Publications

• Two for the Price of One: Lifting Separation Logic Assertions,

Jacob Thamsborg, Lars Birkedal, and Hongseok Yang

January 2010. (Submitted)

• A Semantic Foundation for Hidden State,

Jab Schwinghammer, Hongseok Yang, Lars Birkedal, Francois Pottier,

and Bernhard Reus

FOSSACS 2010, April 2010. ©Springer-Verlag

The full version with proofs is available here.

• Nested Hoare Triples and Frame Rule for Higher-order Store,

Jab Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang

CSL 2009, August 2009. ©Springer-Verlag

The full version with proofs is available here.

• Blamining the Client: On Data Refinement in the Presence of Pointers,

Ivana Filipovic, Peter O’Hearn, Noah Torp-Smith and Hongseok Yang

Formal Aspects of Computing,

2009. ©Springer-Verlag (To appear)

• Abstraction for Concurrent Objects,

Ivana Filipovic, Peter O’Hearn, Noam Rinetzky and Hongseok Yang

ESOP 2009, April 2009. ©Springer-Verlag

The full version with proofs is available here.

• Separation and Information Hiding,

Peter O’Hearn, Hongseok Yang and John Reynolds

ACM Transactions on Programming Languages and Systems 31(3),

2009. ©ACM

• Compositional Shape Analysis,

Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang

POPL 2009, January 2009. ©ACM

• Scalable Shape Analysis for Systems Code,

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook,

Dino Distefano and Peter O’Hearn,

CAV 2008, July 2008. ©Springer-Verlag

• A Simple Model of Separation Logic for Higher-order Store,

Lars Birkedal, Bernhard Reus, Jan Schwinghammer and Hongseok Yang

ICALP 2008, July 2008. ©Springer-Verlag

• Ranking Abstractions,

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv and Hongseok Yang,

ESOP 2008, April 2008. ©Springer-Verlag

The full version with proofs is available here.

• Relational Parametricity and Separation Logic,

Lars Birkedal and Hongseok Yang,

Logical Methods in Computer Science, 4(2:6), 2008.

Journal version of my FOSSACS paper.

It contains proofs, examples and a description on general framework.

• On Scalable Shape Analysis,

Hongseok Yang, Oukseh Lee, Cristiano Calcagno, Dino Distefano and

Peter O’Hearn,

Queen Mary Tech Report RR-07-10, November 2007.

• Goal-directed Weakening of Abstract Interpretation Results,

Sunae Seo, Hongseok Yang, Kwangkeun Yi and Taisook Han.

ACM Transactions on Programming Languages and Systems, 29(6), 2007. ©ACM

• Footprint Analysis: A Shape Analysis that Discovers Preconditions,

Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang,

SAS 2007, August 2007. ©Springer-Verlag

Queen Mary Tech Report RR-07-02.

• Shape Analysis for Composite Data Structures,

Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn,

Thomas Wies and Hongseok Yang,

CAV 2007, July 2007. ©Springer-Verlag

Microsoft Research Tech Report TR-2007-13.

• Local Action and Abstract Separation Logic,

Cristiano Calcagno, Peter O’Hearn and Hongseok Yang,

LICS 2007, July 2007. ©IEEE

The full version with proofs is available here.

• Relational Separation Logic,

Hongseok Yang,

Theoretical Computer Science, vol375/1-3, pp 308-334, May 2007. ©Elsevier

• Relational Parametricity and Separation Logic,

Lars Birkedal and Hongseok Yang,

FOSSACS 2007, April 2007. ©Springer-Verlag

• Semantics of Separation-logic Typing and Higher-order Frame Rules for Algol-like Languages,

Lars Birkedal, Noah Torp-Smith and Hongseok Yang,

vol 2, issue 5, paper 1, Logical Methods in Computer Science, 2006.

Journal version of my LICS paper.

It contains proofs, examples and new results on the conjunction rule.

• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic,

Cristiano Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang,

SAS 2006, August 2006. ©Springer-Verlag

The full version with proofs is available here.

• A local shape analysis based on separation logic,

Dino Distefano, Peter O'Hearn and Hongseok Yang,

TACAS 2006, April 2006. ©Springer-Verlag

The full version with proofs is available here.

• Data Refinement with Low-level Pointer Operations,

Ivana Mijajlovic and Hongseok Yang,

APLAS 2005, November 2005. ©Springer-Verlag

The full version with proofs is available here.

• Static Insertion of Safe and Effective Memory Reuse Commands into ML-like Programs,

Oukseh Lee, Hongseok Yang and Kwangkeun Yi,

Science of Computer Programming, vol 58/1-2, pp 141-178, October 2005. ©Elsevier

• Semantics of Separation-logic Typing and Higher-order Frame Rules,

Lars Birkedal, Noah Torp-Smith and Hongseok Yang,

LICS 2005, June 2005. ©IEEE

• Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis,

Oukseh Lee, Hongseok Yang and Kwangkeun Yi,

ESOP 2005, April 2005. ©Springer-Verlag

A technical report has more explanations, and it is available here.

• Abstract-value Slicing,

Sunae Seo, Hongseok Yang and Kwangkeun Yi,

Electronic Manuscript. September 2004.

A longer version with proofs is available here.

• Possible Worlds and Resources: The Semantics of BI,

David J. Pym, Peter W. O'Hearn and Hongseok Yang,

Theoretical Computer Science, vol 315/1, pp 257-305, May 2004. ©Elsevier

• Correctness of Data Representations involving Heap Data Structures,

Uday S. Reddy and Hongseok Yang,

Journal version of my ESOP paper.

It contains a better semantic model than the one in the conference paper.

• Separation and Information Hiding,

Peter W. O'Hearn, Hongseok Yang and John C. Reynolds,

• Automatic Construction of Hoare Proofs from Abstract Interpretation Results,

Sunae Seo, Hongseok Yang and Kwangkeun Yi,

• Inserting Safe Memory Re-use Commands into ML-like Programs,

Oukseh Lee, Hongseok Yang and Kwangkeun Yi,

• Correctness of Data Representations involving Heap Data Structures,

Uday S. Reddy and Hongseok Yang,

• A Semantic Basis for Local Reasoning,

Hongseok Yang and Peter W. O'Hearn,

• Local Reasoning about Programs that Alter Data Structures,

Peter W. O'Hearn, John Reynolds and Hongseok Yang,

• Local Reasoning for Stateful Programs,

Hongseok Yang,

Ph.D. thesis, July, 2001

• Computability and Complexity Results for a Spatial Assertion Language for Data Structures,

Cristiano Calcagno, Hongseok Yang and Peter W. O'Hearn,

• An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm,

Hongseok Yang,

SPACE 2001 workshop, London, January 2001.

• Parametric Sheaves for modelling Store Locality,

Hongseok Yang and Uday S. Reddy,

Electronic Manuscript, December 2000.

• On the Semantics of Refinement Calculi,

Hongseok Yang and Uday S. Reddy,

• Petri Net Semantics of Bunched Implication,

Peter W. O'Hearn and Hongseok Yang,

Electric Manuscript, October 1999.

• Type Reconstruction for Syntactic Control of Interference, Part 2,

Hongseok Yang and Howard Huang,

ICCL 1998, May 1998.

• Imperative Lambda Calculus Revisited,

Hongseok Yang and Uday S. Reddy,

Electronic Manuscript, August 1997.