Hongseok Yang

Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang: A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science 23(1): 1-54 (2013)

Alexey Gotsman, Noam Rinetzky, Hongseok Yang: Verifying Concurrent Memory Reclamation Algorithms with Grace. ESOP 2013: 249-269

Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang: Views: compositional reasoning for concurrent programs. POPL 2013: 287-300

Jacob Thamsborg, Lars Birkedal, Hongseok Yang: Two for the Price of One: Lifting Separation Logic Assertions. Logical Methods in Computer Science 8(3) (2012)

Oukseh Lee, Hongseok Yang, Rasmus Petersen: A divide-and-conquer approach for analysing overlaid data structures. Formal Methods in System Design 41(1): 4-24 (2012)

Alexey Gotsman, Hongseok Yang: Linearizability with Ownership Transfer. CONCUR 2012: 256-271

Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang: Concurrent Library Correctness on the TSO Memory Model. ESOP 2012: 87-107

Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv: Abstractions from tests. POPL 2012: 373-386

Saswat Anand, Mayur Naik, Mary Jean Harrold, Hongseok Yang: Automated concolic testing of smartphone apps. SIGSOFT FSE 2012: 59

Alexey Gotsman, Madanlal Musuvathi, Hongseok Yang: Show No Weakness: Sequentially Consistent Specifications of TSO Libraries. DISC 2012: 31-45

Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang: Nested Hoare Triples and Frame Rules for Higher-order Store. Logical Methods in Computer Science 7(3) (2011)

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Compositional Shape Analysis by Means of Bi-Abduction. J. ACM 58(6): 26 (2011)

Oukseh Lee, Hongseok Yang, Rasmus Petersen: Program Analysis for Overlaid Data Structures. CAV 2011: 592-608

Alexey Gotsman, Hongseok Yang: Liveness-Preserving Atomicity Abstraction. ICALP (2) 2011: 453-465

Alexey Gotsman, Hongseok Yang: Modular verification of preemptive OS kernels. ICFP 2011: 404-417

Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, Hongseok Yang: Step-indexed kripke models over recursive worlds. POPL 2011: 119-132

Hongseok Yang (Ed.): Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings. Lecture Notes in Computer Science 7078, Springer 2011, isbn 978-3-642-25317-1

Ivana Filipovic, Peter W. O'Hearn, Noah Torp-Smith, Hongseok Yang: Blaming the client: on data refinement in the presence of pointers. Formal Asp. Comput. 22(5): 547-583 (2010)

Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51-52): 4379-4398 (2010)

Aziem Chawdhary, Hongseok Yang: Metric Spaces and Termination Analyses. APLAS 2010: 156-171

Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus: A Semantic Foundation for Hidden State. FOSSACS 2010: 2-17

Peter W. O'Hearn, Hongseok Yang, John C. Reynolds: Separation and information hiding. ACM Trans. Program. Lang. Syst. 31(3) (2009)

Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang: Nested Hoare Triples and Frame Rules for Higher-Order Store. CSL 2009: 440-454

Hongseok Yang: Automatic Verification of Heap-Manipulating Programs Using Separation Logic. CSR 2009: 25

Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang: Abstraction for Concurrent Objects. ESOP 2009: 252-266

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Compositional shape analysis by means of bi-abduction. POPL 2009: 289-300

Lars Birkedal, Hongseok Yang: Relational Parametricity and Separation Logic. Logical Methods in Computer Science 4(2) (2008)

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn: Scalable Shape Analysis for Systems Code. CAV 2008: 385-398

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang: Ranking Abstractions. ESOP 2008: 148-162

Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang: A Simple Model of Separation Logic for Higher-Order Store. ICALP (2) 2008: 348-360

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Space Invading Systems Code. LOPSTR 2008: 1-3

Lars Birkedal, Hongseok Yang: Relational Parametricity and Separation Logic. CoRR abs/0805.0783 (2008)

Hongseok Yang: Relational separation logic. Theor. Comput. Sci. 375(1-3): 308-334 (2007)

Sunae Seo, Hongseok Yang, Kwangkeun Yi, Taisook Han: Goal-directed weakening of abstract interpretation results. ACM Trans. Program. Lang. Syst. 29(6) (2007)

Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang: Shape Analysis for Composite Data Structures. CAV 2007: 178-192

Lars Birkedal, Hongseok Yang: Relational Parametricity and Separation Logic. FoSSaCS 2007: 93-107

Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang: Local Action and Abstract Separation Logic. LICS 2007: 366-378

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Footprint Analysis: A Shape Analysis That Discovers Preconditions. SAS 2007: 402-418

Hongseok Yang: Towards Shape Analysis for Device Drivers. VMCAI 2007: 267

Richard Bornat, Cristiano Calcagno, Hongseok Yang: Variables as Resource in Separation Logic. Electr. Notes Theor. Comput. Sci. 155: 247-276 (2006)

Lars Birkedal, Noah Torp-Smith, Hongseok Yang: Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages. Logical Methods in Computer Science 2(5) (2006)

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. SAS 2006: 182-203

Hongseok Yang: Shape Analysis for Low-Level Code. SAS 2006: 280

Dino Distefano, Peter W. O'Hearn, Hongseok Yang: A Local Shape Analysis Based on Separation Logic. TACAS 2006: 287-302

Lars Birkedal, Noah Torp-Smith, Hongseok Yang: Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages. CoRR abs/cs/0610081 (2006)

Oukseh Lee, Hongseok Yang, Kwangkeun Yi: Static insertion of safe and effective memory reuse commands into ML-like programs. Sci. Comput. Program. 58(1-2): 141-178 (2005)

Ivana Mijajlovic, Hongseok Yang: Data Refinement with Low-Level Pointer Operations. APLAS 2005: 19-36

Oukseh Lee, Hongseok Yang, Kwangkeun Yi: Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis. ESOP 2005: 124-140

Lars Birkedal, Noah Torp-Smith, Hongseok Yang: Semantics of Separation-Logic Typing and Higher-Order Frame Rules. LICS 2005: 260-269

Uday S. Reddy, Hongseok Yang: Correctness of data representations involving heap data structures. Sci. Comput. Program. 50(1-3): 129-160 (2004)

David J. Pym, Peter W. O'Hearn, Hongseok Yang: Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. 315(1): 257-305 (2004)

Peter W. O'Hearn, Hongseok Yang, John C. Reynolds: Separation and information hiding. POPL 2004: 268-280

Sunae Seo, Hongseok Yang, Kwangkeun Yi: Automatic Construction of Hoare Proofs from Abstract Interpretation Results. APLAS 2003: 230-245

Uday S. Reddy, Hongseok Yang: Correctness of Data Representations Involving Heap Data Structures. ESOP 2003: 223-237

Oukseh Lee, Hongseok Yang, Kwangkeun Yi: Inserting Safe Memory Reuse Commands into ML-Like Programs. SAS 2003: 171-188

Oukseh Lee, Hongseok Yang, Kwangkeun Yi: Inserting Safe Memory Re-use Commands into ML-like Programs. APLAS 2002: 317-333

Hongseok Yang, Peter W. O'Hearn: A Semantic Basis for Local Reasoning. FoSSaCS 2002: 402-416

Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. APLAS 2001: 289-300

Peter W. O'Hearn, John C. Reynolds, Hongseok Yang: Local Reasoning about Programs that Alter Data Structures. CSL 2001: 1-19

Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. FSTTCS 2001: 108-119

Hongseok Yang, Uday S. Reddy: On the Semantics of Refinement Calculi. FoSSaCS 2000: 359-374

Hongseok Yang, Howard Huang: Type Reconstruction for Syntactic Control of Interference, Part 2. ICCL 1998: 164-173