Skip to content

Chung-Kil Hur

Publication record assembled from the DBLP archive of ranked conferences.

Papers indexed

27

Venues

11

Active years

2007–2025

Best venue rank

A*

Where they publish

Papers

27 indexed papers, newest first.

YearVenueTitleAuthors
2025CPPCRIS: The Power of Imagination in Specification and Verification (Invited Talk).Chung-Kil Hur
2025ICMLPfeife: Automatic Pipeline Parallelism for PyTorch.Ho Young Jhoo, Chung-Kil Hur, Nuno P. Lopes
2022PLDISequential reasoning for optimizing compilers under weak memory concurrency.Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav
2021CAVAn SMT Encoding of LLVM's Memory Model for Bounded Translation Validation.Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes
2021CONCURFormally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL.Simon Foster, Chung-Kil Hur, Jim Woodcock
2021PLDIModular data-race-freedom guarantees in the promising semantics.Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav
2021PLDIAlive2: bounded translation validation for LLVM.Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr
2020CPPAn equational theory for weak bisimulation via generalized parameterized coinduction.Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
2020PLDIPromising 2.0: global optimizations in relaxed memory concurrency.Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
2019CAVAliveInLean: A Verified LLVM Peephole Optimization Verifier.Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes
2019PLDIPromising-ARM/RISC-V: a simpler and faster operational concurrency model.Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur
2018PLDICrellvm: verified credible compilation for LLVM.Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun Yi
2017PLDIRepairing sequential consistency in C/C++11.Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
2017PLDITaming undefined behavior in LLVM.Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, Nuno P. Lopes
2017POPLA promising semantics for relaxed-memory concurrency.Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
2016POPLLightweight verification of separate compilation.Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
2015ICFPPilsner: a compositionally verified compiler for a higher-order imperative language.Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis
2015PLDIA formal C memory model supporting integer-pointer casts.Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
2014AAAIR2: An Efficient MCMC Sampler for Probabilistic Programs.Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, Selva Samuel
2014PLDISlicing probabilistic programs.Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel
2013POPLThe power of parameterization in coinductive proof.Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis
2012POPLThe marriage of bisimulations and Kripke logical relations.Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis
2011LICSSeparation Logic in the Presence of Garbage Collection.Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
2011POPLA kripke logical relation between ML and assembly.Chung-Kil Hur, Derek Dreyer
2010CSLSecond-Order Equational Logic (Extended Abstract).Marcelo P. Fiore, Chung-Kil Hur
2009ICFPBiorthogonality, step-indexing and compiler correctness.Nick Benton, Chung-Kil Hur
2007ICALPEquational Systems and Free Constructions (Extended Abstract).Marcelo P. Fiore, Chung-Kil Hur