Hongseok Yang : Publications

Journal papers

• [1]

  Two for the Price of One: Lifting Separation Logic Assertions

  Jacob Thamsborg‚ Lars Birkedal and Hongseok Yang

  2011.

  (Submitted)

  Details about Two for the Price of One: Lifting Separation Logic Assertions | BibTeX data for Two for the Price of One: Lifting Separation Logic Assertions

• [2]

  A Step−Indexed Kripke Model of Hidden State

  Jan Schwinghammer‚ Lars Birkedal‚ Francois Pottier‚ Bernhard Reus‚ Kristian Stovring and Hongseok Yang

  2011.

  (Submitted)

  Details about A Step−Indexed Kripke Model of Hidden State | BibTeX data for A Step−Indexed Kripke Model of Hidden State | Download  (pdf) of A Step−Indexed Kripke Model of Hidden State

• [3]

  Nested Hoare Triples and Frame Rule for Higher−order Store

  Jan Schwinghammer‚ Lars Birkedal‚ Bernhard Reus and Hongseok Yang

  In Logical Methods in Computer Science. Vol. 7(3:21). 2011.

  Details about Nested Hoare Triples and Frame Rule for Higher−order Store | BibTeX data for Nested Hoare Triples and Frame Rule for Higher−order Store | Download  (pdf) of Nested Hoare Triples and Frame Rule for Higher−order Store

• [4]

  Compositional Shape Analysis by means of Bi−abduction

  Cristiano Calcagno‚ Dino Distefano‚ Peter W. O’Hearn and Hongseok Yang

  In Journal of the ACM. 2011.

  (To appear)

  Details about Compositional Shape Analysis by means of Bi−abduction | BibTeX data for Compositional Shape Analysis by means of Bi−abduction | Download  (pdf) of Compositional Shape Analysis by means of Bi−abduction

• [5]

  Abstraction for Concurrent Objects

  Ivana Filipovic‚ Peter W. O’Hearn‚ Noam Rinetzky and Hongseok Yang

  In Theoretical Computer Science. Vol. 411. No. 51−52. Pages 4379–4398. 2010.

  Details about Abstraction for Concurrent Objects | BibTeX data for Abstraction for Concurrent Objects

• [6]

  Blaiming the Client: On Data Refinement in the Presence of Pointers

  Ivana Filipovic‚ Peter W. O’Hearn‚ Noah Torp−Smith and Hongseok Yang

  In Formal Aspects of Computing. Vol. 22. No. 5. Pages 547–583. 2010.

  Details about Blaiming the Client: On Data Refinement in the Presence of Pointers | BibTeX data for Blaiming the Client: On Data Refinement in the Presence of Pointers

• [7]

  Separation and Information Hiding

  Peter W. O’Hearn‚ Hongseok Yang and John Reynolds

  In ACM Transactions on Programming Languages and Systems. Vol. 31. No. 3. February, 2009.

  Details about Separation and Information Hiding | BibTeX data for Separation and Information Hiding

• [8]

  Relational Parametricity and Separation Logic

  Lars Birkedal and Hongseok Yang

  In Logical Methods in Computer Science. Vol. 4. No. 2. May, 2008.

  Details about Relational Parametricity and Separation Logic | BibTeX data for Relational Parametricity and Separation Logic

• [9]

  Goal−directed Weakening of Abstract Interpretation Results

  Sunae Seo‚ Hongseok Yang‚ Kwangkeun Yi and Taisook Han

  In ACM Transactions on Programming Languages and Systems. Vol. 29. No. 6. October, 2007.

  Details about Goal−directed Weakening of Abstract Interpretation Results | BibTeX data for Goal−directed Weakening of Abstract Interpretation Results

• [10]

  Relational Separation Logic

  Hongseok Yang

  In Theoretical Computer Science. Vol. 375. No. 1−3. Pages 308–334. May, 2007.

  Details about Relational Separation Logic | BibTeX data for Relational Separation Logic

• [11]

  Semantics of Separation−logic Typing and Higher−order Frame Rules for Algol−like Languages

  Lars Birkedal‚ Noah Torp−Smith and Hongseok Yang

  In Logical Methods in Computer Science. Vol. 2. No. 5. Pages 1. October, 2006.

  Details about Semantics of Separation−logic Typing and Higher−order Frame Rules for Algol−like Languages | BibTeX data for Semantics of Separation−logic Typing and Higher−order Frame Rules for Algol−like Languages

• [12]

  Static Insertion of Safe and Effective Memory Reuse Commands into ML−like Programs

  Oukseh Lee‚ Hongseok Yang and Kwangkeun Yi

  In Science of Computer Programming. Vol. 58. No. 1−2. Pages 141–178. October, 2005.

  Details about Static Insertion of Safe and Effective Memory Reuse Commands into ML−like Programs | BibTeX data for Static Insertion of Safe and Effective Memory Reuse Commands into ML−like Programs

• [13]

  Possible Worlds and Resources: The Semantics of BI

  David Pym‚ Peter W. O'Hearn and Hongseok Yang

  In Theoretical Computer Science. Vol. 315. No. 1. Pages 257–305. May, 2004.

  Details about Possible Worlds and Resources: The Semantics of BI | BibTeX data for Possible Worlds and Resources: The Semantics of BI

• [14]

  Correctness of Data Representations involving Heap Data Structures

  Uday S. Reddy and Hongseok Yang

  In Science of Computer Programming. Vol. 50. No. 1−3. Pages 129–160. March, 2004.

  Details about Correctness of Data Representations involving Heap Data Structures | BibTeX data for Correctness of Data Representations involving Heap Data Structures

Conference papers

• [1]

  The Importance of Being Linearizable

  Alexey Gotsman and Hongseok Yang

  2011.

  (Submitted)

  Details about The Importance of Being Linearizable | BibTeX data for The Importance of Being Linearizable | Download  (pdf) of The Importance of Being Linearizable

• [2]

  Modular verification of preemptive OS kernels

  Alexey Gotsman and Hongseok Yang

  In Manuel M. T. Chakravarty‚ Zhenjiang Hu and Olivier Danvy, editors, Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. Pages 404−417. Tokyo‚ Japan. 2011. ACM.

  Details about Modular verification of preemptive OS kernels | BibTeX data for Modular verification of preemptive OS kernels | Download  (pdf) of Modular verification of preemptive OS kernels | DOI (http://doi.acm.org/10.1145/2034773.2034827)

• [3]

  Liveness−preserving Atomicity Abstraction

  Alexey Gotsman and Hongseok Yang

  In Proceedings of the 38th International Colloquium on Automata‚ Languages and Programming. Vol. 6461 of Lecture Notes in Computer Science. Pages 453–465. Zurich‚ Switzerland. July, 2011. Springer−Verlag.

  Details about Liveness−preserving Atomicity Abstraction | BibTeX data for Liveness−preserving Atomicity Abstraction | Download  (pdf) of Liveness−preserving Atomicity Abstraction

• [4]

  Program Analysis for Overlaid Data Structures

  Oukseh Lee‚ Hongseok Yang and Rasmus Petersen

  In Proceedings of the 23rd International Conference on Computer Aided Verification. Vol. 6806 of Lecture Notes in Computer Science. Pages 592–608. Utah‚ USA. July, 2011. Springer−Verlag.

  Details about Program Analysis for Overlaid Data Structures | BibTeX data for Program Analysis for Overlaid Data Structures | Download  (pdf) of Program Analysis for Overlaid Data Structures

• [5]

  Step−Indexed Kripke Models over Recursive Worlds

  Lars Birkedal‚ Bernhard Reus‚ Jan Schwinghammer‚ Kristian Stovring‚ Jacob Thamsborg and Hongseok Yang

  In Proceedings of the 38th ACM Symposium on Principles of Programming Languages. Pages 119–132. Austin‚ USA. January, 2011. ACM.

  Details about Step−Indexed Kripke Models over Recursive Worlds | BibTeX data for Step−Indexed Kripke Models over Recursive Worlds | Download  (pdf) of Step−Indexed Kripke Models over Recursive Worlds

• [6]

  Metric Spaces and Termination Analyses

  Aziem Chawdhary and Hongseok Yang

  In Proceedings of the 8th Asian Symposium on Programming Languages and Systems. Vol. 6461 of Lecture Notes in Computer Science. Pages 156–171. Shanghai‚ China. November, 2010. Springer−Verlag.

  Details about Metric Spaces and Termination Analyses | BibTeX data for Metric Spaces and Termination Analyses

• [7]

  A Semantic Foundation for Hidden State

  Jan Schwinghammer‚ Hongseok Yang‚ Lars Birkedal‚ François Pottier and Bernhard Reus

  In Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures. Vol. 6014 of Lecture Notes in Computer Science. Pages 2–17. Paphos‚ Cyprus. March, 2010. Springer−Verlag.

  Details about A Semantic Foundation for Hidden State | BibTeX data for A Semantic Foundation for Hidden State

• [8]

  Nested Hoare Triples and Frame Rule for Higher−order Store

  Jan Schwinghammer‚ Lars Birkedal‚ Bernhard Reus and Hongseok Yang

  In Proceedings of the 18th EACSL Annual Conference on Computer Science Logic. Vol. 5771 of Lecture Notes in Computer Science. Pages 440–454. Coimbra‚ Portugal. September, 2009. Springer−Verlag.

  Details about Nested Hoare Triples and Frame Rule for Higher−order Store | BibTeX data for Nested Hoare Triples and Frame Rule for Higher−order Store

• [9]

  Abstraction for Concurrent Objects

  Ivana Filipovic‚ Peter W. O’Hearn‚ Noam Rinetzky and Hongseok Yang

  In Proceedings of the 18th European Symposium on Programming. Vol. 5502 of Lecture Notes in Computer Science. Pages 252–266. York‚ UK. March, 2009. Springer−Verlag.

  Details about Abstraction for Concurrent Objects | BibTeX data for Abstraction for Concurrent Objects

• [10]

  Compositional Shape Analysis by means of Bi−abduction

  Cristiano Calcagno‚ Dino Distefano‚ Peter W. O’Hearn and Hongseok Yang

  In Proceedings of the 36th ACM Symposium on Principles of Programming Languages. Pages 289–300. Savannah‚ USA. January, 2009. ACM.

  Details about Compositional Shape Analysis by means of Bi−abduction | BibTeX data for Compositional Shape Analysis by means of Bi−abduction

• [11]

  A Simple Model of Separation Logic for Higher−Order Store

  Lars Birkedal‚ Bernhard Reus‚ Jan Schwinghammer and Hongseok Yang

  In Proceedings of the 35th International Colloquium on Automata‚ Languages and Programming. Vol. 5126 of Lecture Notes in Computer Science. Pages 348–360. Reykjavik‚ Iceland. July, 2008. Springer−Verlag.

  Details about A Simple Model of Separation Logic for Higher−Order Store | BibTeX data for A Simple Model of Separation Logic for Higher−Order Store

• [12]

  Ranking Abstractions

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

  In Proceedings of the 17th European Symposium on Programming. Vol. 4960 of Lecture Notes in Computer Science. Pages 148–162. Budapest‚ Hangary. April, 2008. Springer−Verlag.

  Details about Ranking Abstractions | BibTeX data for Ranking Abstractions

• [13]

  Scalable Shape Analysis for Systems Code

  Hongseok Yang‚ Oukseh Lee‚ Josh Berdine‚ Cristiano Calcagno‚ Byron Cook‚ Dino Distefano and Peter W. O'Hearn

  In Proceedings of the 20th International Conference on Computer Aided Verification. Vol. 5123 of Lecture Notes in Computer Science. Pages 385–398. Princeton‚ NJ‚ USA. July, 2008. Springer−Verlag.

  Details about Scalable Shape Analysis for Systems Code | BibTeX data for Scalable Shape Analysis for Systems Code

• [14]

  Footprint Analysis: A Shape Analysis that Discovers Preconditions

  Cristiano Calcagno‚ Dino Distefano‚ Peter W. O'Hearn and Hongseok Yang

  In Proceedings of the 14th International Static Analysis Symposium. Vol. 4634 of Lecture Notes in Computer Science. Pages 402–418. Springer−Verlag. August, 2007.

  Details about Footprint Analysis: A Shape Analysis that Discovers Preconditions | BibTeX data for Footprint Analysis: A Shape Analysis that Discovers Preconditions

• [15]

  Shape Analysis for Composite Data Structures

  Josh Berdine‚ Cristiano Calcagno‚ Byron Cook‚ Dino Distefano‚ Peter W. O'Hearn‚ Thomas Wies and Hongseok Yang

  In Proceedings of the 19th International Conference on Computer Aided Verification. Vol. 4590 of Lecture Notes in Computer Science. Pages 178–192. Berlin‚ Germany. July, 2007. Springer−Verlag.

  Details about Shape Analysis for Composite Data Structures | BibTeX data for Shape Analysis for Composite Data Structures

• [16]

  Local Action and Abstract Separation Logic

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

  In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science. Pages 366–378. Wroclaw‚ Poland. July, 2007. IEEE.

  Details about Local Action and Abstract Separation Logic | BibTeX data for Local Action and Abstract Separation Logic

• [17]

  Relational Parametricity and Separation Logic

  Lars Birkedal and Hongseok Yang

  In Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures. Vol. 4423 of Lecture Notes in Computer Science. Pages 93–107. Braga‚ Portugal. March, 2007. Springer−Verlag.

  Details about Relational Parametricity and Separation Logic | BibTeX data for Relational Parametricity and Separation Logic

• [18]

  Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

  Cristiano Calcagno‚ Dino Distefano‚ Hongseok Yang and Peter W. O'Hearn

  In Proceedings of the 13th International Static Analysis Symposium. Vol. 4134 of Lecture Notes in Computer Science. Pages 182–203. Seoul‚ Korea. August, 2006. Springer−Verlag.

  Details about Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic | BibTeX data for Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

• [19]

  Variables as Resource in Separation Logic

  Richard Bornat‚ Cristiano Calcagno and Hongseok Yang

  In Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics. Vol. 155 of Electronic Notes in Theoretical Computer Science. Pages 247–276. Elsevier. May, 2006.

  Details about Variables as Resource in Separation Logic | BibTeX data for Variables as Resource in Separation Logic

• [20]

  A local shape analysis based on separation logic

  Dino Distefano‚ Peter W. O'Hearn and Hongseok Yang

  In Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Vol. 3920 of Lecture Notes in Computer Science. Pages 287–302. Vienna. April, 2006. Springer−Verlag.

  Details about A local shape analysis based on separation logic | BibTeX data for A local shape analysis based on separation logic

• [21]

  Data Refinement with Low−level Pointer Operations

  Ivana Mijajlovic and Hongseok Yang

  In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems. Vol. 3780 of Lecture Notes in Computer Science. Pages 19–36. Tsukuba. November, 2005. Springer−Verlag.

  Details about Data Refinement with Low−level Pointer Operations | BibTeX data for Data Refinement with Low−level Pointer Operations

• [22]

  Semantics of Separation−logic Typing and Higher−order Frame Rules

  Lars Birkedal‚ Noah Torp−Smith and Hongseok Yang

  In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science. Pages 260–269. Chicago. June, 2005. IEEE.

  Details about Semantics of Separation−logic Typing and Higher−order Frame Rules | BibTeX data for Semantics of Separation−logic Typing and Higher−order Frame Rules

• [23]

  Automatic Verification of Pointer Programs Using Grammar−Based Shape Analysis

  Oukseh Lee‚ Hongseok Yang and Kwangkeun Yi

  In Proceedings of the 14th European Symposium on Programming. Vol. 3444 of Lecture Notes in Computer Science. Pages 124–140. Edinburgh. April, 2005. Springer−Verlag.

  Details about Automatic Verification of Pointer Programs Using Grammar−Based Shape Analysis | BibTeX data for Automatic Verification of Pointer Programs Using Grammar−Based Shape Analysis

• [24]

  Separation and Information Hiding

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

  In Proceedings of the 31st ACM Symposium on Principles of Programming Languages. Pages 268–280. Venice. January, 2004. ACM.

  Details about Separation and Information Hiding | BibTeX data for Separation and Information Hiding

• [25]

  Automatic Construction of Hoare Proofs from Abstract Interpretation Results

  Sunae Seo‚ Hongseok Yang and Kwangkeun Yi

  In Proceedings of the 1st Asian Symposium on Programming Languages and Systems. Vol. 2895 of Lecture Notes in Computer Science. Pages 230–245. Beijing. November, 2003. Springer−Verlag.

  Details about Automatic Construction of Hoare Proofs from Abstract Interpretation Results | BibTeX data for Automatic Construction of Hoare Proofs from Abstract Interpretation Results | Link to Automatic Construction of Hoare Proofs from Abstract Interpretation Results

• [26]

  Inserting Safe Memory Reuse Commands into ML−like Programs

  Oukseh Lee‚ Hongseok Yang and Kwangkeun Yi

  In Proceedings of the 10th Annual International Static Analysis Symposium. Vol. 2694 of Lecture Notes in Computer Science. Pages 171–188. San Diego‚ California. June, 2003. Springer−Verlag.

  Details about Inserting Safe Memory Reuse Commands into ML−like Programs | BibTeX data for Inserting Safe Memory Reuse Commands into ML−like Programs | Link to Inserting Safe Memory Reuse Commands into ML−like Programs

• [27]

  Correctness of Data Representations involving Heap Data Structures

  Uday S. Reddy and Hongseok Yang

  In Proceedings of the 12th European Symposium on Programming. Vol. 2618 of Lecture Notes in Computer Science. Pages 223–237. Springer−Verlag. April, 2003.

  Details about Correctness of Data Representations involving Heap Data Structures | BibTeX data for Correctness of Data Representations involving Heap Data Structures | Link to Correctness of Data Representations involving Heap Data Structures

• [28]

  SAW: the spatial assertion workbench

  Cristiano Calcagno‚ Josh Berdine‚ Hongseok Yang and Peter W. O'Hearn

  In Proceedings of the 2nd Workshop on Automated Verification of Critical Systems. Birmingham. April, 2002.

  Details about SAW: the spatial assertion workbench | BibTeX data for SAW: the spatial assertion workbench

• [29]

  A Semantic Basis for Local Reasoning

  Hongseok Yang and Peter W. O'Hearn

  In Proceedings of the 5th Conference on Foundations of Software Science and Computation Structures. Vol. 2303 of Lecture Notes in Computer Science. Pages 402–416. Springer−Verlag. April, 2002.

  Details about A Semantic Basis for Local Reasoning | BibTeX data for A Semantic Basis for Local Reasoning | Link to A Semantic Basis for Local Reasoning

• [30]

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

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

  In Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science. Vol. 2245 of Lecture Notes in Computer Science. Pages 108–119. Springer−Verlag. December, 2001.

  Details about Computability and Complexity Results for a Spatial Assertion Language for Data Structures | BibTeX data for Computability and Complexity Results for a Spatial Assertion Language for Data Structures | Link to Computability and Complexity Results for a Spatial Assertion Language for Data Structures

• [31]

  Local Reasoning about Programs that Alter Data Structures

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

  In L. Fribourg, editor, Proceedings of 15th Annual Conference of the European Association for Computer Science Logic. Vol. 2142 of Lecture Notes in Computer Science. Pages 1–19. Springer−Verlag. September, 2001.

  Details about Local Reasoning about Programs that Alter Data Structures | BibTeX data for Local Reasoning about Programs that Alter Data Structures | Link to Local Reasoning about Programs that Alter Data Structures

• [32]

  An Example of Local Reasoning in BI Pointer Logic: the Schorr−Waite Graph Marking Algorithm

  Hongseok Yang

  In Proceedings of the 1st Workshop on Semantics‚ Program Analysis‚ and Computing Environments for Memory Management. January, 2001.

  Details about An Example of Local Reasoning in BI Pointer Logic: the Schorr−Waite Graph Marking Algorithm | BibTeX data for An Example of Local Reasoning in BI Pointer Logic: the Schorr−Waite Graph Marking Algorithm | Link to An Example of Local Reasoning in BI Pointer Logic: the Schorr−Waite Graph Marking Algorithm

• [33]

  On the Semantics of Refinement Calculi

  Hongseok Yang and Uday S. Reddy

  In Proceedings of the 3rd Conference on Foundations of Software Science and Computation Structures. Vol. 1784 of Lecture Notes in Computer Science. Pages 359–374. Springer−Verlag. April, 2000.

  Details about On the Semantics of Refinement Calculi | BibTeX data for On the Semantics of Refinement Calculi | Link to On the Semantics of Refinement Calculi

• [34]

  Type Reconstruction for Syntactic Control of Interference‚ Part 2

  Howard Huang and Hongseok Yang

  In Proceedings of the 1998 International Confererence on Computer Languages. Pages 164–173. IEEE. May, 1998.

  Details about Type Reconstruction for Syntactic Control of Interference‚ Part 2 | BibTeX data for Type Reconstruction for Syntactic Control of Interference‚ Part 2 | Link to Type Reconstruction for Syntactic Control of Interference‚ Part 2

Theses

• [1]

  Local Reasoning for Stateful Programs

  Hongseok Yang

  PhD Thesis University of Illinois at Urbana−Champaign. 2001.

  (Technical Report UIUCDCS−R−2001−2227)

  Details about Local Reasoning for Stateful Programs | BibTeX data for Local Reasoning for Stateful Programs | Link to Local Reasoning for Stateful Programs