Travelled to:1 × Austria
1 × Cyprus
1 × Estonia
1 × Hungary
1 × Iceland
1 × Japan
1 × Korea
1 × Spain
1 × Switzerland
12 × USA
2 × Denmark
2 × Germany
2 × Poland
2 × Portugal
3 × Italy
4 × United Kingdom
5 × France
Collaborated with:P.W.O'Hearn A.Gotsman L.Birkedal M.Naik C.Calcagno D.Distefano K.Yi O.Lee ∅ U.S.Reddy B.Reus J.Schwinghammer H.Oh N.Rinetzky R.Mangal X.Zhang R.Grigore J.C.Reynolds M.Sagiv S.Burckhardt B.Cook G.Castelnuovo K.Heo A.Cerone R.Petersen N.Torp-Smith J.Berdine M.Zawirski H.Peleg S.Shoham E.Yahav M.Musuvathi S.Anand M.J.Harrold I.Filipovic Kwonsoo Chae Wonyeol Lee 0001 Hangyeol Yu X.Rival W.Lee T.Dinsdale-Young P.Gardner M.J.Parkinson F.Pottier A.Chawdhary S.Gulwani Carla Ferreira 0001 Mahsa Najafzadeh Marc Shapiro 0001 K.Støvring J.Thamsborg T.Wies A.Scibior O.Kammar M.Vákár S.Staton Y.Cai K.Ostermann Sean K. Moss C.Heunen Z.Ghahramani
Talks about:analysi (17) abstract (9) program (9) shape (9) data (7) separ (6) logic (5) structur (4) composit (4) concurr (4)
Person: Hongseok Yang
DBLP: Yang:Hongseok
Facilitated 1 volumes:
EdContributed to:
2015
2015
20152014
2014
2014
201420132013201320132012
20122012
20112011
20112011
2010
200920092009200820082008
200820072007
20072007
20072006
2006200520052004200320032002200120002017201620182020Wrote 49 papers:
- ESOP-2015-GotsmanY #data type
- Composite Replicated Data Types (AG, HY), pp. 585–609.
- OOPSLA-2015-OhYY #adaptation #learning #optimisation #program analysis
- Learning a strategy for adapting a program analysis via bayesian optimisation (HO, HY, KY), pp. 572–588.
- SAS-2015-CastelnuovoNRSY #analysis #bottom-up #case study #composition #top-down
- Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis (GC, MN, NR, MS, HY), pp. 252–274.
- ESOP-2014-MangalNY #analysis #interprocedural
- A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join (RM, MN, HY), pp. 513–533.
- ICALP-v2-2014-CeroneGY
- Parameterised Linearisability (AC, AG, HY), pp. 98–109.
- PLDI-2014-OhLHYY #context-sensitive grammar
- Selective context-sensitivity guided by impact pre-analysis (HO, WL, KH, HY, KY), p. 49.
- PLDI-2014-ZhangMGNY #abstraction #analysis #datalog #on the #refinement
- On abstraction refinement for program analyses in Datalog (XZ, RM, RG, MN, HY), p. 27.
- PLDI-2014-ZhangMNY #analysis #bottom-up #hybrid #interprocedural #top-down
- Hybrid top-down and bottom-up interprocedural analysis (XZ, RM, MN, HY), p. 28.
- POPL-2014-BurckhardtGYZ #data type #specification #verification
- Replicated data types: specification, verification, optimality (SB, AG, HY, MZ), pp. 271–284.
- ESOP-2013-GotsmanRY #algorithm #concurrent #memory management #verification
- Verifying Concurrent Memory Reclamation Algorithms with Grace (AG, NR, HY), pp. 249–269.
- PLDI-2013-ZhangNY #abstraction #analysis #data flow #parametricity
- Finding optimum abstractions in parametric dataflow analysis (XZ, MN, HY), pp. 365–376.
- POPL-2013-Dinsdale-YoungBGPY #composition #concurrent #named #reasoning #source code
- Views: compositional reasoning for concurrent programs (TDY, LB, PG, MJP, HY), pp. 287–300.
- SAS-2013-PelegSYY #automaton #mining #specification
- Symbolic Automata for Static Specification Mining (HP, SS, EY, HY), pp. 63–83.
- ESOP-2012-BurckhardtGMY #concurrent #correctness #library #memory management
- Concurrent Library Correctness on the TSO Memory Model (SB, AG, MM, HY), pp. 87–107.
- FSE-2012-AnandNHY #automation #smarttech #testing
- Automated concolic testing of smartphone apps (SA, MN, MJH, HY), p. 59.
- POPL-2012-NaikYCS #abstraction #testing
- Abstractions from tests (MN, HY, GC, MS), pp. 373–386.
- CAV-2011-LeeYP #data type #program analysis
- Program Analysis for Overlaid Data Structures (OL, HY, RP), pp. 592–608.
- ICALP-v2-2011-GotsmanY #abstraction
- Liveness-Preserving Atomicity Abstraction (AG, HY), pp. 453–465.
- ICFP-2011-GotsmanY #composition #kernel #verification
- Modular verification of preemptive OS kernels (AG, HY), pp. 404–417.
- POPL-2011-BirkedalRSSTY #modelling #recursion
- Step-indexed kripke models over recursive worlds (LB, BR, JS, KS, JT, HY), pp. 119–132.
- FoSSaCS-2010-SchwinghammerYBPR #semantics
- A Semantic Foundation for Hidden State (JS, HY, LB, FP, BR), pp. 2–17.
- CSL-2009-SchwinghammerBRY #higher-order #hoare
- Nested Hoare Triples and Frame Rules for Higher-Order Store (JS, LB, BR, HY), pp. 440–454.
- ESOP-2009-FilipovicORY #abstraction #concurrent
- Abstraction for Concurrent Objects (IF, PWO, NR, HY), pp. 252–266.
- POPL-2009-CalcagnoDOY #analysis #composition
- Compositional shape analysis by means of bi-abduction (CC, DD, PWO, HY), pp. 289–300.
- CAV-2008-YangLBCCDO #analysis #scalability
- Scalable Shape Analysis for Systems Code (HY, OL, JB, CC, BC, DD, PWO), pp. 385–398.
- ESOP-2008-ChawdharyCGSY #abstraction #ranking
- Ranking Abstractions (AC, BC, SG, MS, HY), pp. 148–162.
- ICALP-B-2008-BirkedalRSY #higher-order #logic
- A Simple Model of Separation Logic for Higher-Order Store (LB, BR, JS, HY), pp. 348–360.
- LOPSTR-2008-CalcagnoDOY
- Space Invading Systems Code (CC, DD, PWO, HY), pp. 1–3.
- CAV-2007-BerdineCCDOWY #analysis #data type
- Shape Analysis for Composite Data Structures (JB, CC, BC, DD, PWO, TW, HY), pp. 178–192.
- FoSSaCS-2007-BirkedalY #logic #parametricity #relational
- Relational Parametricity and Separation Logic (LB, HY), pp. 93–107.
- LICS-2007-CalcagnoOY #logic
- Local Action and Abstract Separation Logic (CC, PWO, HY), pp. 366–378.
- SAS-2007-CalcagnoDOY #analysis
- Footprint Analysis: A Shape Analysis That Discovers Preconditions (CC, DD, PWO, HY), pp. 402–418.
- VMCAI-2007-Yang #analysis #towards
- Towards Shape Analysis for Device Drivers (HY), p. 267.
- SAS-2006-CalcagnoDOY #abstraction #pointer #reachability
- Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic (CC, DD, PWO, HY), pp. 182–203.
- SAS-2006-Yang #analysis #low level
- Shape Analysis for Low-Level Code (HY), p. 280.
- TACAS-2006-DistefanoOY #analysis #logic
- A Local Shape Analysis Based on Separation Logic (DD, PWO, HY), pp. 287–302.
- ESOP-2005-LeeYY #analysis #automation #grammarware #pointer #source code #using #verification
- Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis (OL, HY, KY), pp. 124–140.
- LICS-2005-BirkedalTY #higher-order #semantics #type system
- Semantics of Separation-Logic Typing and Higher-Order Frame Rules (LB, NTS, HY), pp. 260–269.
- POPL-2004-OHearnYR #information management
- Separation and information hiding (PWO, HY, JCR), pp. 268–280.
- ESOP-2003-ReddyY #correctness #data transformation #data type
- Correctness of Data Representations Involving Heap Data Structures (USR, HY), pp. 223–237.
- SAS-2003-LeeYY #memory management #reuse #source code
- Inserting Safe Memory Reuse Commands into ML-Like Programs (OL, HY, KY), pp. 171–188.
- FoSSaCS-2002-YangO #reasoning #semantics
- A Semantic Basis for Local Reasoning (HY, PWO), pp. 402–416.
- CSL-2001-OHearnRY #data type #reasoning #source code
- Local Reasoning about Programs that Alter Data Structures (PWO, JCR, HY), pp. 1–19.
- FoSSaCS-2000-YangR #calculus #on the #refinement #semantics
- On the Semantics of Refinement Calculi (HY, USR), pp. 359–374.
- OOPSLA-2017-ChaeOHY #automation #generative #heuristic #learning #program analysis
- Automatically generating features for learning program analysis heuristics for C-like languages (KC, HO, KH, HY), p. 25.
- POPL-2016-GotsmanYFNS #consistency #distributed #reasoning
- 'Cause I'm strong enough: reasoning about consistency choices in distributed systems (AG, HY, CF0, MN, MS0), pp. 371–384.
- POPL-2016-GrigoreY #abstraction #probability #refinement
- Abstraction refinement guided by a learnt probabilistic model (RG, HY), pp. 485–498.
- POPL-2018-ScibiorKVSYCOMH #higher-order #validation
- Denotational validation of higher-order Bayesian inference (AS, OK, MV, SS, HY, YC, KO, SKM, CH, ZG), p. 29.
- POPL-2020-LeeYRY #probability #source code #towards
- Towards verified stochastic variational inference for probabilistic programs (WL0, HY, XR, HY), p. 33.