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