Modular Verification of Interrupt-driven software
Since there has been relatively lack of verification
methods for interrupt-driven programs even the behavior of interrupts is similar with that of threads, we introduced a more accurate verification
method for interrupt-driven programs by leveraging a thread-modular
analysis for concurrent programs. By modeling interrupt behavior such
as priority information and preemption information with Z3 SMT solver,
I combined this information with a thread-modular abstract interpretation
analysis. Therefore, I could remove infeasible interference for interrupt-driven programs and could achieve a more accurate analysis without losing
I compared our analysis to state-of-the-art techniques one of which is a thread-modular analysis for concurrent programs, and another is a model checking based interrupt-driven analysis tool, with about 35 C-base interrupt-driven programs. Finally, my tool showed its higher accuracy than other two tools with getting a little overhead.
Project link: https://github.com/chunghasung/intabs
Extension of a Scope query optimization tool
During the internship at MSR, I extended a scope query optimization tool. The tool consists of two parts: one part is parser and another part is template generation. Basically, it parses a query file and then prints a C-style code template, and the template is fed into a programming synthesis tool to optimize it. Then, the optimized C-style program is translated into an optimized query. However, the tool only supported a small set of queries because many queries use many combinations of columns and uninterpreted functions. So, I have changed both parser and template generation parts. To achieve this, I got used to F#, C# and Scope query.
Optimization of testing web applications
Project link: https://github.com/chunghasung/jsdep
Project link: https://righthelp.github.io/tutorial/overview
Development of Boot loader sequence
When I was at AhnLab, I worked on prototyping new boot loader for an appliance that should be compatible with x86/MIPS architecture and Linux-based operating systems and simplified customer support and troubleshooting, ensuring that the boot loader would provide multi-level booting, securing the system to protect not only back side information, but customers’ information as well.