Publications

• A Convenient Category for Higher-Order Probability Theory,

Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang

LICS 2017, June 2017. ©IEEE

• Design and Implementation of Probabilistic Programming Language Anglican,

David Tolpin, Jan-Willem van de Meent, Hongseok Yang, and Frank Wood

Postconference Proceedings of IFL 2016, February 2017. ©ACM

The full version is available here.

• Automatically Generating Features for Learning Program Analysis Heuristics,

Kwonsoo Chae, Hakjoo Oh, Kihong Heo, and Hongseok Yang

November 2016. (Draft)

• Exchangeable Random Processes and Data Abstraction,

Sam Staton, Hongseok Yang, Nathanael Ackerman, Cameron Freer, and Daniel M. Roy

PPS Workshop 2017, Janary 2017.

• Efficient Exact Inference in Discrete Anglican Programs,

Robert Cornish, Frank Wood, and Hongseok Yang

PPS Workshop 2017, Janary 2017.

• On the Pitfalls of Nested Monte Carlo,

Tom Rainforth, Robert Cornish, Hongseok Yang, and Frank Wood

NIPS workshop on Advances in Approximate Bayesian Inference 2016, December 2016.

• Learning a Variable-Clustering Strategy for Octagon from Labeled Data Generated by a Static Analysis,

Kihong Heo, Hakjoo Oh, and Hongseok Yang

SAS 2016, September 2016. ©Springer-Verlag

• Specification and Complexity of Collaborative Text Editing,

Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang,

and Marek Zawirski

PODC 2016, July 2016. ©ACM

The full version is available here.

• Semantics for Probabilistic Programming: Higher-order Functions, Continuous Distributions, and Soft Constraints,

Sam Staton, Hongseok Yang, Chris Heunen, Ohad Kammar, and Frank Wood

LICS 2016, July 2016. ©IEEE

• 'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems,

Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh,

and Marc Shapiro

POPL 2016, January 2016. ©ACM

The full version is available here.

• Abstraction Refinement Guided by a Learnt Probabilistic Model,

Radu Grigore and Hongseok Yang

POPL 2016, January 2016. ©ACM

The full version is available here.

• Selective X-Sensitive Analysis Guided by Impact Pre-Analysis,

Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi

TOPLAS 2015, December 2015. ©ACM

This is a full version of our PLDI'14 paper.

• Learning a Strategy for Adapting a Program Analysis via Bayesian Optimisation,

Hakjoo Oh, Hongseok Yang, and Kwangkeun Yi

OOPSLA 2015, October 2015. ©ACM

• Transaction Chopping for Parallel Snapshot Isolation,

Andrea Cerone, Alexey Gotsman, and Hongseok Yang

DISC 2015, October 2015. ©Springer-Verlag

The full version is available here.

• Modularity in Lattices: A Case Study on the Correspondence between Top-Down and Bottom-Up Analysis,

Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, and Hongseok Yang

SAS 2015, September 2015. ©Springer-Verlag

• Particle Gibbs with Ancestor Sampling for Probabilistic Programs,

Jan-Willem van de Meent, Hongseok Yang, Vikash Mansinghka, and Frank Wood

AISTATS 2015, May 2015.

• Composite Replicated Data Types,

Alexey Gotsman and Hongseok Yang

ESOP 2015, April 2015. ©Springer-Verlag

The full version is available here.

• Symbolic Automata for Representing Big Code,

Hila Peleg, Sharon Shoham, Eran Yahav, and Hongseok Yang

Acta Informatica, 2015.

This is a full version of our SAS'13 paper.

• Parameterised Linearizability,

Andrea Cerone, Alexey Gotsman, and Hongseok Yang

ICALP 2014, July 2014. ©Springer-Verlag

The full version is available here.

• On Abstraction Refinement for Program Analyses in Datalog,

(Distinguished paper award)

Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang

PLDI 2014, June 2014. ©ACM

The full version is available here.

• Hybrid Top-Down and Bottom-Up Interprocedural Analysis,

Xin Zhang, Ravi Mangal, Mayur Naik, and Hongseok Yang

PLDI 2014, June 2014. ©ACM

The full version is available here.

• Selective Context-Sensitivity Guided by Impact Pre-Analysis,

Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi

PLDI 2014, June 2014. ©ACM

The full version is available here.

• A Correspondence between Two Approaches to Interprocedural Analyses in the Presence of Join, (Best award paper nominee)

Ravi Mangal, Mayur Naik, and Hongseok Yang

ESOP 2014, April 2014. ©Springer-Verlag

The full version is available here.

• Replicated Data Types: Specification, Verification, Optimality,

Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski

POPL 2014, January 2014. ©ACM

The full version is available here.

The preliminary version with some additional material can be found here.

• Modular Verification of Preemptive OS Kernels,

Alexey Gotsman and Hongseok Yang

Journal of Functional Programming, Volume 23, Number 4, 2013.

This is a full version of our ICFP'11 paper.

• Linearizability with Ownership Transfer,

Alexey Gotsman and Hongseok Yang

Logical Methods in Computer Science, 9(3:12), 2013.

This is a full version of our CONCUR'12 paper.

• Symbolic Automata for Static Specification Mining,

Hila Peleg, Sharon Shoham, Eran Yahav, and Hongseok Yang

SAS 2013, June 2013. ©Springer-Verlag

The full version is available here.

• Finding Optimum Abstractions in Parametric Dataflow Analysis,

Xin Zhang, Mayur Naik, and Hongseok Yang

PLDI 2013, June 2013. ©ACM

The full version is available here.

• Verifying Concurrent Memory Reclamation Algorithms with Grace,

(EASST & EATCS best paper runner-up)

Alexey Gotsman, Noam Rinetzky, and Hongseok Yang

ESOP 2013, March 2013. ©Springer-Verlag

The full version is available here.

• A Step-Indexed Kripke Model of Hidden State,

Jan Schwinghammer, Lars Birkedal, Francois Pottier, Bernhard Reus,

Kristian Stovring, and Hongseok Yang

Mathematical Structures in Computer Science, Volume 23, Number 1, February 2013.

• Views: Compositional Reasoning for Concurrent Programs,

Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner,

Matthew Parkinson, and Hongseok Yang

POPL 2013, January 2013. ©ACM

• Two for the Price of One: Lifting Separation Logic Assertions,

Jacob Thamsborg, Lars Birkedal, and Hongseok Yang

Logical Methods in Computer Science, 8(3:22), 2012.

• Automated Concolic Testing of Smartphone Apps,

Saswat Anand, Mayur Naik, Hongseok Yang, and Mary Jean Harrold

FSE 2012, November 2012. ©ACM

The full version is available here.

• Show No Weakness: Sequentially Consistent Specifications of TSO Libraries,

Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang

DISC 2012, October 2012. ©Springer-Verlag

The full version is available here.

• Linearizability with Ownership Transfer, (Best paper award)

Alexey Gotsman, and Hongseok Yang

CONCUR 2012, September 2012. ©Springer-Verlag

The full version is available here.

• Concurrent Library Correctness on the TSO Memory Model,

Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang

ESOP 2012, March 2012. ©Springer-Verlag

The full version with proofs is available here.

• Abstractions From Tests,

Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv

POPL 2012, January 2012. ©ACM

The full version is available here.

• A Divide-and-Concur Approach for Analysing Overlaid Data Structures,

Oukseh Lee, Hongseok Yang, and Rasmus Petersen

Formal Methods in System Design, Volume 41, Number 1, 2012. ©Springer-Verlag

This is a journal version of our CAV’11 paper.

It contains in-depth discussions on the pre-analysis.

• Compositional Shape Analysis by means of Bi-abduction,

Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang

Journal of the ACM, Volume 58, Number 6, December 2011.

This is a journal version of our POPL’09 paper.

• Modular Verification of Preemptive OS Kernels,

Alexey Gotsman, and Hongseok Yang

ICFP 2011, September 2011. ©ACM

The full version with proofs is available here.

• Nested Hoare Triples and Frame Rule for Higher-order Store,

Jan Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang

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

This is a journal version of our CSL’09 paper.

It contains more examples, proofs, and counterexamples.

• Liveness-preserving Atomicity Abstraction,

Alexey Gotsman, and Hongseok Yang

ICALP 2011, July 2011. ©Springer-Verlag

The full version with proofs is available here.

• Program Analysis for Overlaid Data Structures,

Oukseh Lee, Hongseok Yang, and Rasmus Petersen

CAV 2011, July 2011. ©Springer-Verlag

• Step-Indexed Kripke Models over Recursive Worlds,

Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Stovring,

Jacob Thamsborg, and Hongseok Yang

POPL 2011, January 2011. ©ACM

• Metric Spaces and Termination Analysis,

Aziem Chawdhary, and Hongseok Yang

APLAS 2010, November 2010. ©Springer-Verlag

The full version with proofs is available here.

• Abstraction for Concurrent Objects,

Ivana Filipovic, Peter O’Hearn, Noam Rinetzky and Hongseok Yang

Theoretical Computer Science 411(51-52), 2010. ©Elsevier

This is a journal version of our ESOP’09 paper, and it contains proofs, examples

and more in-depth discussions on our results.

• A Semantic Foundation for Hidden State,

Jan Schwinghammer, Hongseok Yang, Lars Birkedal, Francois Pottier,

and Bernhard Reus

FOSSACS 2010, April 2010. ©Springer-Verlag

The full version with proofs is available here.

• Blamining the Client: On Data Refinement in the Presence of Pointers,

Ivana Filipovic, Peter O’Hearn, Noah Torp-Smith and Hongseok Yang

Formal Aspects of Computing 22(5), 2010. ©Springer-Verlag

• Nested Hoare Triples and Frame Rule for Higher-order Store,

Jan Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang

CSL 2009, August 2009. ©Springer-Verlag

The full version with proofs is available here.

• Abstraction for Concurrent Objects,

Ivana Filipovic, Peter O’Hearn, Noam Rinetzky and Hongseok Yang

ESOP 2009, April 2009. ©Springer-Verlag

The full version with proofs is available here.

• Separation and Information Hiding,

Peter O’Hearn, Hongseok Yang and John Reynolds

ACM Transactions on Programming Languages and Systems 31(3), 2009. ©ACM

• Compositional Shape Analysis by means of Bi-abduction,

Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang

POPL 2009, January 2009. ©ACM

• Scalable Shape Analysis for Systems Code,

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook,

Dino Distefano and Peter O’Hearn,

CAV 2008, July 2008. ©Springer-Verlag

• A Simple Model of Separation Logic for Higher-order Store,

Lars Birkedal, Bernhard Reus, Jan Schwinghammer and Hongseok Yang

ICALP 2008, July 2008. ©Springer-Verlag

• Ranking Abstractions,

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

ESOP 2008, April 2008. ©Springer-Verlag

The full version with proofs is available here.

• Relational Parametricity and Separation Logic,

Lars Birkedal and Hongseok Yang,

Logical Methods in Computer Science, 4(2:6), 2008.

Journal version of my FOSSACS’07 paper.

It contains proofs, examples and a description on general framework.

• On Scalable Shape Analysis,

Hongseok Yang, Oukseh Lee, Cristiano Calcagno, Dino Distefano and

Peter O’Hearn,

Queen Mary Tech Report RR-07-10, November 2007.

• Goal-directed Weakening of Abstract Interpretation Results,

Sunae Seo, Hongseok Yang, Kwangkeun Yi and Taisook Han.

ACM Transactions on Programming Languages and Systems, 29(6), 2007. ©ACM

• Footprint Analysis: A Shape Analysis that Discovers Preconditions,

Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang,

Queen Mary Tech Report RR-07-02.

• Shape Analysis for Composite Data Structures,

Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn,

Thomas Wies and Hongseok Yang,

Microsoft Research Tech Report TR-2007-13.

• Local Action and Abstract Separation Logic,

Cristiano Calcagno, Peter O’Hearn and Hongseok Yang,

The full version with proofs is available here.

• Relational Separation Logic,

Hongseok Yang,

• Relational Parametricity and Separation Logic,

Lars Birkedal and Hongseok Yang,

• Semantics of Separation-logic Typing and Higher-order Frame Rules for Algol-like Languages,

Lars Birkedal, Noah Torp-Smith and Hongseok Yang,

Logical Methods in Computer Science, 2(5:1), 2006.

Journal version of my LICS’05 paper.

It contains proofs, examples and new results on the conjunction rule.

• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic,

Cristiano Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang,

The full version with proofs is available here.

• A local shape analysis based on separation logic,

Dino Distefano, Peter O'Hearn and Hongseok Yang,

The full version with proofs is available here.

• Data Refinement with Low-level Pointer Operations,

Ivana Mijajlovic and Hongseok Yang,

The full version with proofs is available here.

• Static Insertion of Safe and Effective Memory Reuse Commands into ML-like Programs,

Oukseh Lee, Hongseok Yang and Kwangkeun Yi,

• Semantics of Separation-logic Typing and Higher-order Frame Rules,

Lars Birkedal, Noah Torp-Smith and Hongseok Yang,

• Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis,

Oukseh Lee, Hongseok Yang and Kwangkeun Yi,

A technical report has more explanations, and it is available here.

• Abstract-value Slicing,

Sunae Seo, Hongseok Yang and Kwangkeun Yi,

Electronic Manuscript. September 2004.

A longer version with proofs is available here.

• Possible Worlds and Resources: The Semantics of BI,

David J. Pym, Peter W. O'Hearn and Hongseok Yang,

• Correctness of Data Representations involving Heap Data Structures,

Uday S. Reddy and Hongseok Yang,

Journal version of my ESOP paper.

It contains a better semantic model than the one in the conference paper.

• Separation and Information Hiding,

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

• Automatic Construction of Hoare Proofs from Abstract Interpretation Results,

Sunae Seo, Hongseok Yang and Kwangkeun Yi,

• Inserting Safe Memory Re-use Commands into ML-like Programs,

Oukseh Lee, Hongseok Yang and Kwangkeun Yi,

• Correctness of Data Representations involving Heap Data Structures,

Uday S. Reddy and Hongseok Yang,

• A Semantic Basis for Local Reasoning,

Hongseok Yang and Peter W. O'Hearn,

• Local Reasoning about Programs that Alter Data Structures,

Peter W. O'Hearn, John Reynolds and Hongseok Yang,

• Local Reasoning for Stateful Programs,

Hongseok Yang,

Ph.D. thesis, July, 2001

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

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

• An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm,

Hongseok Yang,

• Parametric Sheaves for modelling Store Locality,

Hongseok Yang and Uday S. Reddy,

Electronic Manuscript, December 2000.

• On the Semantics of Refinement Calculi,

Hongseok Yang and Uday S. Reddy,

• Petri Net Semantics of Bunched Implication,

Peter W. O'Hearn and Hongseok Yang,

Electric Manuscript, October 1999.

• Type Reconstruction for Syntactic Control of Interference, Part 2,

Hongseok Yang and Howard Huang,

ICCL 1998, May 1998.

• Imperative Lambda Calculus Revisited,

Hongseok Yang and Uday S. Reddy,

Electronic Manuscript, August 1997.