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", }