Developed a neuro-symbolic framework for C program termination and non-termination analysis, integrating LLVM-based loop extraction, LLM-guided witness synthesis, and SMT-based validation with iterative refinement.
Developed a sound framework for termination and non-termination analysis of C programs, incorporating bit-precise reasoning, bounded semantics, and support for complex language constructs.
Developed a tool-agnostic preprocessing framework for C/C++ termination and nontermination analysis, using loop-based program slicing and input-driven concretization to simplify analysis for existing verification tools.
Developed a hybrid termination and non-termination analysis framework for C/C++ programs, combining dynamic loop-entry reachability analysis with static precondition synthesis and refinement.
Developed a hybrid rule-based and machine-learning framework for automatically detecting and classifying physical-unit inconsistencies in ROS/C++ robotic software.
Extended an LLVM-IR-to-transition-system translator with support for arrays, structures, and bit-level operations, enabling automated analysis of complex program constructs.
Developed a constraint-based test generation framework for automatically synthesizing domain-specific test inputs from program path constraints.
Developed a Roslyn-based static analysis tool for detecting violations of naming conventions, method-structure guidelines, and code-complexity rules in C# programs.
Developed a software modularization and architecture recovery tool using class-level dependency analysis to identify structural relationships and module boundaries.
Designed and tested an object-oriented C# application using interface-based design, test stubs, and NUnit-based unit testing.
Developed and evaluated an early-fusion semantic segmentation framework integrating RGB, depth, and edge information for thin-obstacle detection in UAV navigation using the DDOS dataset.
Developed a spatial trajectory analysis pipeline using data preprocessing and DBSCAN clustering to identify geographic patterns in large-scale taxi data.
Developed a warehouse management system integrating a PostgreSQL database, SQL stored procedures and functions, and a C#Windows Forms application.
Implemented a WCF-based client-server application to compare synchronous and asynchronous communication using C# Windows Forms clients.
Analyzed and modeled hospital workflows to identify process inefficiencies and propose improved future-state operational processes.