Verification of semantic commutativity conditions and inverse operations on linked data structures. - Deokhwan Kim; Martin C. Rinard (PLDI, 2011)

Proving acceptability properties of relaxed nondeterministic approximate programs. - Michael Carbin; Deokhwan Kim; Sasa Misailovic; Martin C. Rinard (PLDI, 2012)

Verified integrity properties for safe approximate program transformations. - Michael Carbin; Deokhwan Kim; Sasa Misailovic; Martin C. Rinard (PEPM, 2013)

Parallelizing Sequential Programs with Statistical Accuracy Tests. - Sasa Misailovic; Deokhwan Kim; Martin C. Rinard (ACM Trans. Embed. Comput. Syst., 2013)

Sound input filter generation for integer overflow errors. - Fan Long; Stelios Sidiroglou-Douskos; Deokhwan Kim; Martin C. Rinard (POPL, 2014)

Targeted Automatic Integer Overflow Discovery Using Goal-Directed Conditional Branch Enforcement. - Stelios Sidiroglou-Douskos; Eric Lahtinen; Nathan Rittenhouse; Paolo Piselli; Fan Long; Deokhwan Kim; Martin C. Rinard (ASPLOS, 2015)

Information Flow Analysis of Android Applications in DroidSafe. - Michael I. Gordon; Deokhwan Kim; Jeff H. Perkins; Limei Gilham; Nguyen Nguyen 002; Martin C. Rinard (NDSS, 2015)

Gyro Drift Correction for An Indirect Kalman Filter Based Sensor Fusion Driver. - Chan-Gun Lee; Nhu-Ngoc Dao; Seonmin Jang; Deokhwan Kim; Yonghun Kim 003; Sungrae Cho (Sensors, 2016)

Synthesizing replacement classes. - Malavika Samak; Deokhwan Kim; Martin C. Rinard (Proc. ACM Program. Lang., 2020)