Model Checking of Real-Time Properties of Resource-Bound Process Algebra. - Junkil Park; Jungjae Lee; Jin-Young Choi; Insup Lee 001 (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2009)

Formal specifications for software-defined networking. - Miyoung Kang; Ki-Hyuk Nam; Junkil Park; Myung-Ki Shin; Jeehoon Shin; Jin-Young Choi (CFI, 2012)

Process Algebraic Specification of Software Defined Networks. - Miyoung Kang; Junkil Park; Jin-Young Choi; Ki-Hyuk Nam; Myung-Ki Shin (CICSyN, 2012)

Demo abstract: ROSLab - A modular programming environment for robotic applications. - Nicola Bezzo; Junkil Park; Andrew L. King; Peter Gebhard; Radoslav Ivanov; Insup Lee 001 (ICCPS, 2014)

A Safety Argument Strategy for PCA Closed-Loop Systems: A Preliminary Proposal. - Lu Feng 001; Andrew L. King; Sanjian Chen; Anaheed Ayoub; Junkil Park; Nicola Bezzo; Oleg Sokolsky; Insup Lee 001 (MCPS, 2014)

Automatic verification of linear controller software. - Miroslav Pajic; Junkil Park; Insup Lee 001; George J. Pappas; Oleg Sokolsky (EMSOFT, 2015)

Sensor attack detection in the presence of transient faults. - Junkil Park; Radoslav Ivanov; James Weimer; Miroslav Pajic; Insup Lee 001 (ICCPS, 2015)

Verified ROS-Based Deployment of Platform-Independent Control Systems. - Wenrui Meng; Junkil Park; Oleg Sokolsky; Stephanie Weirich; Insup Lee 001 (NFM, 2015)

Adaptive Transient Fault Model for Sensor Attack Detection. - Minsu Jo; Junkil Park; Youngmi Baek; Radoslav Ivanov; James Weimer; Sang Hyuk Son; Insup Lee 001 (CPSNA, 2016)

Toward a Hybrid Sensor Fusion Using Probabilistic and Abstract Sensor Models. - Minsu Jo; Junkil Park; Youngmi Baek; Radoslav Ivanov; James Weimer; Sang Hyuk Son; Insup Lee 001 (RTCSA, 2016)

Scalable Verification of Linear Controller Software. - Junkil Park; Miroslav Pajic; Insup Lee 001; Oleg Sokolsky (TACAS, 2016)

Automatic Verification of Finite Precision Implementations of Linear Controllers. - Junkil Park; Miroslav Pajic; Oleg Sokolsky; Insup Lee 001 (TACAS (1), 2017)

A process algebraic approach to the schedulability analysis and workload abstraction of hierarchical real-time systems. - Junkil Park; Insup Lee 001; Oleg Sokolsky; Dae-Yon Hwang; So Jin Ahn; Jin-Young Choi; Inhye Kang (J. Log. Algebraic Methods Program., 2017)

Security of Cyber-Physical Systems in the Presence of Transient Sensor Faults. - Junkil Park; Radoslav Ivanov; James Weimer; Miroslav Pajic; Sang Hyuk Son; Insup Lee 001 (ACM Trans. Cyber Phys. Syst., 2017)

LCV: A Verification Tool for Linear Controller Software. - Junkil Park; Miroslav Pajic; Oleg Sokolsky; Insup Lee 001 (TACAS (1), 2019)

The Move Prover. - Jingyi Emma Zhong; Kevin Cheang; Shaz Qadeer; Wolfgang Grieskamp; Sam Blackshear; Junkil Park; Yoni Zohar; Clark W. Barrett; David L. Dill (CAV (1), 2020)

Reasoning About Vectors Using an SMT Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (IJCAR, 2022)

Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. - David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Meng Xu; Jingyi Emma Zhong (TACAS (1), 2022)

Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. - Ying Sheng 007; Andres Nötzli; Andrew Reynolds 001; Yoni Zohar; David L. Dill; Wolfgang Grieskamp; Junkil Park; Shaz Qadeer; Clark W. Barrett; Cesare Tinelli (J. Autom. Reason., 2023)

Securing Aptos Framework with Formal Verification. - Junkil Park; Teng Zhang; Wolfgang Grieskamp; Meng Xu; Gerardo Di Giacomo; Kundu Chen; Yi Lu; Robert Chen (FMBC@CAV, 2024)