Skip to main content
University of Oxford Department of Computer Science
  Contact Us     Search  
  1. Home
  2. About Us
  3. People
  4. Faculty
  5. Hongseok Yang
  6. Publications

Hongseok Yang : Publications

Click here to download all publications in a single bibtex file

@inproceedings{livlinear-icalp11,
  title = "Liveness-preserving Atomicity Abstraction",
  author = "Alexey Gotsman and Hongseok Yang",
  year = "2011",
  address = "Zurich, Switzerland",
  booktitle = "Proceedings of the 38th International Colloquium on Automata, Languages and Programming",
  isbn = "978-3-642-22011-1",
  month = "July",
  pages = "453--465",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "6461",
}
@inproceedings{multiview-cav11,
  title = "Program Analysis for Overlaid Data Structures",
  author = "Oukseh Lee and Hongseok Yang and Rasmus Petersen",
  year = "2011",
  address = "Utah, USA",
  booktitle = "Proceedings of the 23rd International Conference on Computer Aided Verification",
  isbn = "978-3-642-22109-5",
  month = "July",
  pages = "592--608",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "6806",
}
@inproceedings{kripke-popl11,
  title = "Step-Indexed Kripke Models over Recursive Worlds",
  author = "Lars Birkedal and Bernhard Reus and Jan Schwinghammer and Kristian Stovring and Jacob Thamsborg and Hongseok Yang",
  year = "2011",
  address = "Austin, USA",
  booktitle = "Proceedings of the 38th ACM Symposium on Principles of Programming Languages",
  isbn = "978-1-4503-0490-0",
  month = "January",
  pages = "119--132",
  publisher = "ACM",
}
@article{LiftingJournal11,
  title = "Two for the Price of One: Lifting Separation Logic Assertions",
  author = "Jacob Thamsborg and Lars Birkedal and Hongseok Yang",
  year = "2011",
  note = "(Submitted)",
}
@article{AntiframeJournal11,
  title = "A Step-Indexed Kripke Model of Hidden State",
  author = "Jan Schwinghammer and Lars Birkedal and Francois Pottier and Bernhard Reus and Kristian Stovring and Hongseok Yang",
  year = "2011",
  note = "(Submitted)",
}
@article{deepframe-LMCS11,
  title = "Nested Hoare Triples and Frame Rule for Higher-order Store",
  author = "Jan Schwinghammer and Lars Birkedal and Bernhard Reus and Hongseok Yang",
  year = "2011",
  journal = "Logical Methods in Computer Science",
  volume = "7(3:21)",
}
@article{biabduction-jacm11,
  title = "Compositional Shape Analysis by means of Bi-abduction",
  author = "Cristiano Calcagno and Dino Distefano and Peter W. O’Hearn and Hongseok Yang",
  year = "2011",
  journal = "Journal of the ACM",
  note = "(To appear)",
}
@inproceedings{linown11,
  title = "The Importance of Being Linearizable",
  author = "Alexey Gotsman and Hongseok Yang",
  year = "2011",
  note = "(Submitted)",
}
@inproceedings{scheduler-icfp11,
  title = "Modular verification of preemptive OS kernels",
  author = "Alexey Gotsman and Hongseok Yang",
  year = "2011",
  address = "Tokyo, Japan",
  booktitle = "Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming",
  editor = "Manuel M. T. Chakravarty and Zhenjiang Hu and Olivier Danvy",
  isbn = "978-1-4503-0865-6",
  pages = "404-417",
  publisher = "ACM",
  doi = "http://doi.acm.org/10.1145/2034773.2034827",
}
@inproceedings{antiframe-fossacs10,
  title = "A Semantic Foundation for Hidden State",
  author = "Jan Schwinghammer and Hongseok Yang and Lars Birkedal and Fran\c{c}ois Pottier and Bernhard Reus",
  year = "2010",
  address = "Paphos, Cyprus",
  booktitle = "Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures",
  isbn = "978-3-642-12031-2",
  month = "March",
  pages = "2--17",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "6014",
}
@inproceedings{metric-aplas10,
  title = "Metric Spaces and Termination Analyses",
  author = "Aziem Chawdhary and Hongseok Yang",
  year = "2010",
  address = "Shanghai, China",
  booktitle = "Proceedings of the 8th Asian Symposium on Programming Languages and Systems",
  isbn = "978-3-642-17163-5",
  month = "November",
  pages = "156--171",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "6461",
}
@article{linearizability-tcs10,
  title = "Abstraction for Concurrent Objects",
  author = "Ivana Filipovic and Peter W. O’Hearn and Noam Rinetzky and Hongseok Yang",
  year = "2010",
  journal = "Theoretical Computer Science",
  number = "51-52",
  pages = "4379--4398",
  publisher = "Elsevier",
  volume = "411",
}
@article{refinement-fac09,
  title = "Blaiming the Client: On Data Refinement in the Presence of Pointers",
  author = "Ivana Filipovic and Peter W. O’Hearn and Noah Torp-Smith and Hongseok Yang",
  year = "2010",
  journal = "Formal Aspects of Computing",
  number = "5",
  pages = "547--583",
  publisher = "Springer-Verlag",
  volume = "22",
}
@inproceedings{nested-csl09,
  title = "Nested Hoare Triples and Frame Rule for Higher-order Store",
  author = "Jan Schwinghammer and Lars Birkedal and Bernhard Reus and Hongseok Yang",
  year = "2009",
  address = "Coimbra, Portugal",
  booktitle = "Proceedings of the 18th EACSL Annual Conference on Computer Science Logic",
  isbn = "978-3-642-04026-9",
  month = "September",
  pages = "440--454",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "5771",
}
@inproceedings{linearizability-esop09,
  title = "Abstraction for Concurrent Objects",
  author = "Ivana Filipovic and Peter W. O’Hearn and Noam Rinetzky and Hongseok Yang",
  year = "2009",
  address = "York, UK",
  booktitle = "Proceedings of the 18th European Symposium on Programming",
  isbn = "978-3-642-00589-3",
  month = "March",
  pages = "252--266",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "5502",
}
@article{hiding-toplas09,
  title = "Separation and Information Hiding",
  author = "Peter W. O’Hearn and Hongseok Yang and John Reynolds",
  year = "2009",
  journal = "ACM Transactions on Programming Languages and Systems",
  month = "February",
  number = "3",
  publisher = "ACM",
  volume = "31",
}
@inproceedings{biabduction-popl09,
  title = "Compositional Shape Analysis by means of Bi-abduction",
  author = "Cristiano Calcagno and Dino Distefano and Peter W. O’Hearn and Hongseok Yang",
  year = "2009",
  address = "Savannah, USA",
  booktitle = "Proceedings of the 36th ACM Symposium on Principles of Programming Languages",
  isbn = "978-1-60558-379-2",
  month = "January",
  pages = "289--300",
  publisher = "ACM",
}
@inproceedings{hostore-icalp08,
  title = "A Simple Model of Separation Logic for Higher-Order Store",
  author = "Lars Birkedal and Bernhard Reus and Jan Schwinghammer and Hongseok Yang",
  year = "2008",
  address = "Reykjavik, Iceland",
  booktitle = "Proceedings of the 35th International Colloquium on Automata, Languages and Programming",
  isbn = "978-3-540-70582-6",
  month = "July",
  pages = "348--360",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "5126",
}
@inproceedings{scalability-cav08,
  title = "Scalable Shape Analysis for Systems Code",
  author = "Hongseok Yang and Oukseh Lee and Josh Berdine and Cristiano Calcagno and Byron Cook and Dino Distefano and Peter W. O'Hearn",
  year = "2008",
  address = "Princeton, NJ, USA",
  booktitle = "Proceedings of the 20th International Conference on Computer Aided Verification",
  isbn = "978-3-540-70543-7",
  month = "July",
  pages = "385--398",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "5123",
}
@article{BY-lmcs08,
  title = "Relational Parametricity and Separation Logic",
  author = "Lars Birkedal and Hongseok Yang",
  year = "2008",
  journal = "Logical Methods in Computer Science",
  month = "May",
  number = "2",
  volume = "4",
}
@inproceedings{ranking-esop08,
  title = "Ranking Abstractions",
  author = "Aziem Chawdhary and Byron Cook and Sumit Gulwani and Mooly Sagiv and Hongseok Yang",
  year = "2008",
  address = "Budapest, Hangary",
  booktitle = "Proceedings of the 17th European Symposium on Programming",
  isbn = "978-3-540-78738-9",
  month = "April",
  pages = "148--162",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "4960",
}
@inproceedings{CDOY-sas07,
  title = "Footprint Analysis: A Shape Analysis that Discovers Preconditions",
  author = "Cristiano Calcagno and Dino Distefano and Peter W. O'Hearn and Hongseok Yang",
  year = "2007",
  booktitle = "Proceedings of the 14th International Static Analysis Symposium",
  isbn = "978-3-540-74060-5",
  month = "August",
  pages = "402--418",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "4634",
}
@inproceedings{composite-cav07,
  title = "Shape Analysis for Composite Data Structures",
  author = "Josh Berdine and Cristiano Calcagno and Byron Cook and Dino Distefano and Peter W. O'Hearn and Thomas Wies and Hongseok Yang",
  year = "2007",
  address = "Berlin, Germany",
  booktitle = "Proceedings of the 19th International Conference on Computer Aided Verification",
  isbn = "978-3-540-73367-6",
  month = "July",
  pages = "178--192",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "4590",
}
@inproceedings{COY-lics07,
  title = "Local Action and Abstract Separation Logic",
  author = "Cristiano Calcagno and Peter W. O'Hearn and Hongseok Yang",
  year = "2007",
  address = "Wroclaw, Poland",
  booktitle = "Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science",
  month = "July",
  pages = "366--378",
  publisher = "IEEE",
}
@article{Yang-relational-separation-logic,
  title = "Relational Separation Logic",
  author = "Hongseok Yang",
  year = "2007",
  journal = "Theoretical Computer Science",
  month = "May",
  number = "1-3",
  pages = "308--334",
  publisher = "Elsevier",
  volume = "375",
}
@inproceedings{BY-fossocs07,
  title = "Relational Parametricity and Separation Logic",
  author = "Lars Birkedal and Hongseok Yang",
  year = "2007",
  address = "Braga, Portugal",
  booktitle = "Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures",
  isbn = "978-3-540-71388-3",
  month = "March",
  pages = "93--107",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "4423",
}
@article{SeYaYiHa05,
  title = "Goal-directed Weakening of Abstract Interpretation Results",
  author = "Sunae Seo and Hongseok Yang and Kwangkeun Yi and Taisook Han",
  year = "2007",
  journal = "ACM Transactions on Programming Languages and Systems",
  month = "October",
  number = "6",
  publisher = "ACM",
  volume = "29",
}
@inproceedings{CDOY06,
  title = "Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic",
  author = "Cristiano Calcagno and Dino Distefano and Hongseok Yang and Peter W. O'Hearn",
  year = "2006",
  address = "Seoul, Korea",
  booktitle = "Proceedings of the 13th International Static Analysis Symposium",
  isbn = "3-540-37756-5",
  month = "August",
  pages = "182--203",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "4134",
}
@inproceedings{BoCaYa06-ENTCS,
  title = "Variables as Resource in Separation Logic",
  author = "Richard Bornat and Cristiano Calcagno and Hongseok Yang",
  year = "2006",
  booktitle = "Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics",
  month = "May",
  pages = "247--276",
  publisher = "Elsevier",
  series = "Electronic Notes in Theoretical Computer Science",
  volume = "155",
}
@inproceedings{DiOhYa06,
  title = "A local shape analysis based on separation logic",
  author = "Dino Distefano and Peter W. O'Hearn and Hongseok Yang",
  year = "2006",
  address = "Vienna",
  booktitle = "Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
  isbn = "3-540-33056-9",
  month = "April",
  pages = "287--302",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "3920",
}
@article{BiToYa05-LMCS,
  title = "Semantics of Separation-logic Typing and Higher-order Frame Rules for Algol-like Languages",
  author = "Lars Birkedal and Noah Torp-Smith and Hongseok Yang",
  year = "2006",
  journal = "Logical Methods in Computer Science",
  month = "October",
  number = "5",
  pages = "1",
  volume = "2",
}
@inproceedings{BiToYa05,
  title = "Semantics of Separation-logic Typing and Higher-order Frame Rules",
  author = "Lars Birkedal and Noah Torp-Smith and Hongseok Yang",
  year = "2005",
  address = "Chicago",
  booktitle = "Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science",
  month = "June",
  pages = "260--269",
  publisher = "IEEE",
}
@inproceedings{LeYaYi05,
  title = "Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis",
  author = "Oukseh Lee and Hongseok Yang and Kwangkeun Yi",
  year = "2005",
  address = "Edinburgh",
  booktitle = "Proceedings of the 14th European Symposium on Programming",
  isbn = "3-540-25435-8",
  month = "April",
  pages = "124--140",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "3444",
}
@inproceedings{MiYa05,
  title = "Data Refinement with Low-level Pointer Operations",
  author = "Ivana Mijajlovic and Hongseok Yang",
  year = "2005",
  address = "Tsukuba",
  booktitle = "Proceedings of the 3rd Asian Symposium on Programming Languages and Systems",
  isbn = "3-540-29735-9",
  month = "November",
  pages = "19--36",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = "3780",
}
@article{LeYaYi05-scp,
  title = "Static Insertion of Safe and Effective Memory Reuse Commands into ML-like Programs",
  author = "Oukseh Lee and Hongseok Yang and Kwangkeun Yi",
  year = "2005",
  journal = "Science of Computer Programming",
  month = "October",
  number = "1-2",
  pages = "141--178",
  publisher = "Elsevier",
  volume = "58",
}
@article{OhPyYa03,
  title = "Possible Worlds and Resources: The Semantics of {B}{I}",
  author = "David Pym and Peter W. O'Hearn and Hongseok Yang",
  year = "2004",
  journal = "Theoretical Computer Science",
  month = "May",
  number = "1",
  pages = "257--305",
  publisher = "Elsevier",
  volume = "315",
}
@article{ReYa03-scp,
  title = "Correctness of Data Representations involving Heap Data Structures",
  author = "Uday S. Reddy and Hongseok Yang",
  year = "2004",
  journal = "Science of Computer Programming",
  month = "March",
  number = "1-3",
  pages = "129--160",
  publisher = "Elsevier",
  volume = "50",
}
@inproceedings{OhYaRe03,
  title = "Separation and Information Hiding",
  author = "Peter W. O'Hearn and Hongseok Yang and John C. Reynolds",
  year = "2004",
  address = "Venice",
  booktitle = "Proceedings of the 31st ACM Symposium on Principles of Programming Languages",
  isbn = "1-58113-729-X",
  month = "January",
  pages = "268--280",
  publisher = "ACM",
}
@inproceedings{LeYaYi03,
  title = "Inserting Safe Memory Reuse Commands into ML-like Programs",
  author = "Oukseh Lee and Hongseok Yang and Kwangkeun Yi",
  year = "2003",
  address = "San Diego, California",
  booktitle = "Proceedings of the 10th Annual International Static Analysis Symposium",
  isbn = "3-540-40325-6",
  month = "June",
  pages = "171--188",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/safe-memory-reuse-ML.ps",
  volume = "2694",
}
@inproceedings{ReYa03,
  title = "Correctness of Data Representations involving Heap Data Structures",
  author = "Uday S. Reddy and Hongseok Yang",
  year = "2003",
  booktitle = "Proceedings of the 12th European Symposium on Programming",
  isbn = "3-540-00886-1",
  month = "April",
  pages = "223--237",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/heap-parametricity.ps",
  volume = "2618",
}
@inproceedings{SeYaYi03,
  title = "Automatic Construction of Hoare Proofs from Abstract Interpretation Results",
  author = "Sunae Seo and Hongseok Yang and Kwangkeun Yi",
  year = "2003",
  address = "Beijing",
  booktitle = "Proceedings of the 1st Asian Symposium on Programming Languages and Systems",
  isbn = "3-540-20536-5",
  month = "November",
  pages = "230--245",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/ai2HoareProofs.ps",
  volume = "2895",
}
@inproceedings{CBYO-SAW02,
  title = "{S}{A}{W}: the spatial assertion workbench",
  author = "Cristiano Calcagno and Josh Berdine and Hongseok Yang and Peter W. O'Hearn",
  year = "2002",
  address = "Birmingham",
  booktitle = "Proceedings of the 2nd Workshop on Automated Verification of Critical Systems",
  month = "April",
}
@inproceedings{YO02,
  title = "A Semantic Basis for Local Reasoning",
  author = "Hongseok Yang and Peter W. O'Hearn",
  year = "2002",
  booktitle = "Proceedings of the 5th Conference on Foundations of Software Science and Computation Structures",
  isbn = "3-540-43366-X",
  month = "April",
  pages = "402--416",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/basis.ps",
  volume = "2303",
}
@inproceedings{ORY01,
  title = "Local Reasoning about Programs that Alter Data Structures",
  author = "Peter W. O'Hearn and John C. Reynolds and Hongseok Yang",
  year = "2001",
  booktitle = "Proceedings of 15th Annual Conference of the European Association for Computer Science Logic",
  editor = "L. Fribourg",
  isbn = "3-540-42554-3",
  month = "September",
  pages = "1--19",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/localreasoning.ps",
  volume = "2142",
}
@inproceedings{CYO01,
  title = "Computability and Complexity Results for a Spatial Assertion Language for Data Structures",
  author = "Cristiano Calcagno and Hongseok Yang and Peter W. O'Hearn",
  year = "2001",
  booktitle = "Proceedings of the 22nd Conference on Foundations of Software Technology and Theoretical Computer Science",
  isbn = "3-540-43002-4",
  month = "December",
  pages = "108--119",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/decidability.ps",
  volume = "2245",
}
@inproceedings{Yang-SchorrWaite,
  title = "An Example of Local Reasoning in {B}{I} Pointer Logic: the {S}chorr-{W}aite Graph Marking Algorithm",
  author = "Hongseok Yang",
  year = "2001",
  booktitle = "Proceedings of the 1st Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management",
  month = "January",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/SchorrWaite.ps",
}
@phdthesis{Yang-thesis,
  title = "Local Reasoning for Stateful Programs",
  author = "Hongseok Yang",
  year = "2001",
  note = "(Technical Report UIUCDCS-R-2001-2227)",
  school = "University of Illinois at Urbana-Champaign",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/thesis.ps",
}
@inproceedings{Yang-Reddy-refinement,
  title = "On the Semantics of Refinement Calculi",
  author = "Hongseok Yang and Uday S. Reddy",
  year = "2000",
  booktitle = "Proceedings of the 3rd Conference on Foundations of Software Science and Computation Structures",
  isbn = "3-540-67257-5",
  month = "April",
  organization = "Springer-Verlag",
  pages = "359--374",
  series = "Lecture Notes in Computer Science",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/mulrefinement.ps",
  volume = "1784",
}
@inproceedings{Huang-Yang-reconstruction-2,
  title = "Type Reconstruction for Syntactic Control of Interference, Part 2",
  author = "Howard Huang and Hongseok Yang",
  year = "1998",
  booktitle = "Proceedings of the 1998 International Confererence on Computer Languages",
  month = "May",
  organization = "IEEE",
  pages = "164--173",
  url = "http://www.cs.ox.ac.uk/people/hongseok.yang/paper/final.ps",
}

About Us

Back to Top