Publication

  1. Reparameterization Gradient for Non-differentiable Models. Wonyeol Lee, Hangyeol Yu, and Hongseok Yang. NIPS 2018, December 2018. (To appear)
  2. On Nesting Monte Carlo Estimators. Tom Rainforth, Rob Cornish, Hongseok Yang, Andrew Warrington, and Frank Wood. ICML 2018, July 2018.
  3. The Beta-Bernoulli Process and Algebraic Effects. Sam Staton, Dario Stein, Hongseok Yang, Nathanael Ackerman, Cameron Freer, and Daniel M. Roy, ICALP 2018, July 2018. ©Springer-Verlag. The full version is available here.
  4. Denotational Validation of Higher-Order Bayesian Inference. Adam Scibior, Ohad Kammar, Matthijs Vakar, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahrahmani. POPL 2018, January 2018. ©ACM
  5. The Semantic Structure of Quasi-Borel Spaces. Chris Heunen, Ohad Kammar, Sean Moss, Adam Scibior, Sam Staton, Matthijs Vakar, and Hongseok Yang. Workshop on Probabilistic Programming Semantics (PPS 2018), January 2018.
  6. Learning Analysis Strategies for Octagon and Context Sensitivity from Labeled Data Generated by Static Analyses. Kihong Heo, Hakjoo Oh, and Hongseok Yang. Formal Methods in System Design, 2018. ©Springer-Verlag. This is a journal version of our SAS'16 paper.
  7. Adapting Static Analysis via Learning with Bayesian Optimization. Kihong Heo, Hakjoo Oh, Hongseok Yang, and Kwangkeun Yi. ACM Transactions on Programming Languages and Systems, 2018 . ©ACM. This is a journal version of our OOSPLA'15 paper.
  8. Towards a Testable Notion of Generalisation for Generative Adversarial Networks. Robert Cornish, Frank Wood, and Hongseok Yang. NIPS Workshop on Deep Learning: Bridging Theory and Practice, December 2017.
  9. Inference Trees: Adaptive Inference with Exploration. Tom Rainforth, Yuan Zhou, Xiaoyu Lu, Yee Whye Teh, Frank Wood, Hongseok Yang, and Jan-Willem van de Meent. NIPS Workshop on Advances in Approximate Bayesian Inference (AABI 2017), December 2017.
  10. Automatically Generating Features for Learning Program Analysis Heuristics for C-like Languages. Kwonsoo Chae, Hakjoo Oh, Kihong Heo, and Hongseok Yang. OOPSLA 2017, October 2017. ©ACM
  11. Algebraic Laws for Weak Consistency. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. CONCUR 2017, September 2017.
  12. A Convenient Category for Higher-Order Probability Theory. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. LICS 2017, June 2017. ©IEEE
  13. Design and Implementation of Probabilistic Programming Language Anglican. David Tolpin, Jan-Willem van de Meent, Hongseok Yang, and Frank Wood. Post-conference Proceedings of IFL 2016, February 2017. ©ACM. The full version is available here.
  14. Exchangeable Random Processes and Data Abstraction. Sam Staton, Hongseok Yang, Nathanael Ackerman, Cameron Freer, and Daniel M. Roy. Workshop on Probabilistic Programming Semantics (PPS 2017), Janary 2017.
  15. Efficient Exact Inference in Discrete Anglican Programs. Robert Cornish, Frank Wood, and Hongseok Yang. Workshop on Probabilistic Programming Semantics (PPS 2017), Janary 2017.
  16. On the Pitfalls of Nested Monte Carlo. Tom Rainforth, Robert Cornish, Hongseok Yang, and Frank Wood. NIPS workshop on Advances in Approximate Bayesian Inference (AABI 2016), December 2016.
  17. 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
  18. 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.
  19. 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
  20. '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.
  21. Abstraction Refinement Guided by a Learnt Probabilistic Model. Radu Grigore and Hongseok Yang. POPL 2016, January 2016. ©ACM. The full version is available here.
  22. Selective X-Sensitive Analysis Guided by Impact Pre-Analysis. Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. ACM Transactions on Programming Languages and Systems, December 2015. ©ACM. This is a full version of our PLDI'14 paper.
  23. Learning a Strategy for Adapting a Program Analysis via Bayesian Optimisation. Hakjoo Oh, Hongseok Yang, and Kwangkeun Yi. OOPSLA 2015, October 2015. ©ACM
  24. 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.
  25. 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
  26. Particle Gibbs with Ancestor Sampling for Probabilistic Programs. Jan-Willem van de Meent, Hongseok Yang, Vikash Mansinghka, and Frank Wood. AISTATS 2015, May 2015.
  27. Composite Replicated Data Types. Alexey Gotsman and Hongseok Yang. ESOP 2015, April 2015. ©Springer-Verlag. The full version is available here.
  28. 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.
  29. Parameterised Linearizability. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. ICALP 2014, July 2014. ©Springer-Verlag. The full version is available here.
  30. 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.
  31. 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.
  32. 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.
  33. A Correspondence between Two Approaches to Interprocedural Analyses in the Presence of Join. (Best Paper Award Nominee). Ravi Mangal, Mayur Naik, and Hongseok Yang. ESOP 2014, April 2014. ©Springer-Verlag. The full version is available here.
  34. 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.
  35. 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.
  36. 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.
  37. 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.
  38. 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.
  39. 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.
  40. 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.
  41. Views: Compositional Reasoning for Concurrent Programs. Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang. POPL 2013, January 2013. ©ACM
  42. 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.
  43. 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.
  44. 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.
  45. Linearizability with Ownership Transfer. (Best paper award). Alexey Gotsman, and Hongseok Yang. CONCUR 2012, September 2012. ©Springer-Verlag. The full version is available here.
  46. 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.
  47. Abstractions From Tests. Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv. POPL 2012, January 2012. ©ACM. The full version is available here.
  48. 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, and contains in-depth discussions on the pre-analysis.
  49. 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.
  50. Modular Verification of Preemptive OS Kernels. Alexey Gotsman, and Hongseok Yang. ICFP 2011, September 2011. ©ACM. The full version with proofs is available here.
  51. 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.
  52. Liveness-preserving Atomicity Abstraction. Alexey Gotsman, and Hongseok Yang. ICALP 2011, July 2011. ©Springer-Verlag. The full version with proofs is available here.
  53. Program Analysis for Overlaid Data Structures. Oukseh Lee, Hongseok Yang, and Rasmus Petersen. CAV 2011, July 2011. ©Springer-Verlag
  54. 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
  55. Metric Spaces and Termination Analysis. Aziem Chawdhary, and Hongseok Yang. APLAS 2010, November 2010. ©Springer-Verlag. The full version with proofs is available here.
  56. 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.
  57. 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.
  58. 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.
  59. 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.
  60. 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.
  61. Separation and Information Hiding. Peter O’Hearn, Hongseok Yang and John Reynolds. ACM Transactions on Programming Languages and Systems 31(3), 2009. ©ACM
  62. Compositional Shape Analysis by means of Bi-abduction. Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang. POPL 2009, January 2009. ©ACM
  63. 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
  64. 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
  65. 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.
  66. 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.
  67. 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.
  68. 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
  69. Footprint Analysis: A Shape Analysis that Discovers Preconditions. Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang. SAS 2007, August 2007. ©Springer-Verlag. Queen Mary Tech Report RR-07-02.
  70. Shape Analysis for Composite Data Structures. Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn, Thomas Wies and Hongseok Yang. CAV 2007, July 2007. ©Springer-Verlag. Microsoft Research Tech Report TR-2007-13.
  71. Local Action and Abstract Separation Logic. Cristiano Calcagno, Peter O’Hearn and Hongseok Yang. LICS 2007, July 2007. ©IEEE. The full version with proofs is available here.
  72. Relational Separation Logic. Hongseok Yang. Theoretical Computer Science, vol375/1-3, pp 308-334, May 2007. ©Elsevier
  73. Relational Parametricity and Separation Logic. Lars Birkedal and Hongseok Yang. FOSSACS 2007, April 2007. ©Springer-Verlag
  74. 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.
  75. Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. Cristiano Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang,. SAS 2006, August 2006. ©Springer-Verlag. The full version with proofs is available here.
  76. A Local Shape Analysis based on Separation Logic. Dino Distefano, Peter O'Hearn and Hongseok Yang. TACAS 2006, April 2006. ©Springer-Verlag. The full version with proofs is available here.
  77. Data Refinement with Low-level Pointer Operations. Ivana Mijajlovic and Hongseok Yang. APLAS 2005, November 2005. ©Springer-Verlag. The full version with proofs is available here.
  78. Static Insertion of Safe and Effective Memory Reuse Commands into ML-like Programs. Oukseh Lee, Hongseok Yang and Kwangkeun Yi. Science of Computer Programming, vol 58/1-2, pp 141-178, October 2005. ©Elsevier
  79. Semantics of Separation-logic Typing and Higher-order Frame Rules. Lars Birkedal, Noah Torp-Smith and Hongseok Yang. LICS 2005, June 2005. ©IEEE
  80. Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis. Oukseh Lee, Hongseok Yang and Kwangkeun Yi. ESOP 2005, April 2005. ©Springer-Verlag. A technical report has more explanations, and it is available here.
  81. Abstract-value Slicing. Sunae Seo, Hongseok Yang and Kwangkeun Yi. Electronic Manuscript. September 2004. A longer version with proofs is available here.
  82. Possible Worlds and Resources: The Semantics of BI. David J. Pym, Peter W. O'Hearn and Hongseok Yang. Theoretical Computer Science, vol 315/1, pp 257-305, May 2004. ©Elsevier
  83. Correctness of Data Representations involving Heap Data Structures. Uday S. Reddy and Hongseok Yang. Science of Computer Programming, vol. 50/1-3, pp 129-160, March 2004. ©Elsevier. This is a journal version of our ESOP paper. It contains a better semantic model than the one in the conference paper.
  84. Separation and Information Hiding. Peter W. O'Hearn, Hongseok Yang and John C. Reynolds. POPL 2004, January 2004. ©ACM
  85. Automatic Construction of Hoare Proofs from Abstract Interpretation Results. Sunae Seo, Hongseok Yang and Kwangkeun Yi,. APLAS 2003, November 2003. ©Springer-Verlag
  86. Inserting Safe Memory Re-use Commands into ML-like Programs. Oukseh Lee, Hongseok Yang and Kwangkeun Yi. SAS 2003, June 2003. ©Springer-Verlag
  87. Correctness of Data Representations involving Heap Data Structures. Uday S. Reddy and Hongseok Yang. ESOP 2003, April 2003. ©Springer-Verlag
  88. A Semantic Basis for Local Reasoning. Hongseok Yang and Peter W. O'Hearn. FOSSACS 2002, April 2002. ©Springer-Verlag
  89. Local Reasoning about Programs that Alter Data Structures. Peter W. O'Hearn, John Reynolds and Hongseok Yang. CSL 2001, September 2001. ©Springer-Verlag
  90. Local Reasoning for Stateful Programs. Hongseok Yang. Ph.D. thesis, July, 2001
  91. Computability and Complexity Results for a Spatial Assertion Language for Data Structures. Cristiano Calcagno, Hongseok Yang and Peter W. O'Hearn. FSTTCS 2001, December 2001. ©Springer-Verlag
  92. An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. Hongseok Yang. Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE 2001), January 2001.
  93. Parametric Sheaves for modelling Store Locality. Hongseok Yang and Uday S. Reddy. Electronic Manuscript, December 2000.
  94. On the Semantics of Refinement Calculi. Hongseok Yang and Uday S. Reddy. FOSSACS 2000, April 2000. ©Springer-Verlag
  95. Petri Net Semantics of Bunched Implication. Peter W. O'Hearn and Hongseok Yang. Electric Manuscript, October 1999.
  96. Type Reconstruction for Syntactic Control of Interference, Part 2. Hongseok Yang and Howard Huang. ICCL 1998, May 1998.
  97. Imperative Lambda Calculus Revisited. Hongseok Yang and Uday S. Reddy. Electronic Manuscript, August 1997.