Research projects:
- Scalable Automated Guided Exceution (SAGE)
SAGE is a white-box testing technology geared toward exposing bugs in the target program by systematically executing all of its relevant, input-driven behaviors. SAGE attempts to generate only those tests that exercise unique control paths in the program, thus maximizing the opportunity of finding defects.
The underlying idea of SAGE is to enumerate all the possilbe branches in program wisely thus to identify any possible bugs. This is not easy since programs are running depending on inputs. To figure out which input can lead the exceution to certain branches, SAGE tags all the inputs in a exceution trace and transforms the execution path into a set of constraints. By flipping each conditional branch constraint to its opposite; SAGE is able to compute new input sets intenlligently which can explore the uncovered branches efficiently. Currently SAGE is offered as a filefuzzer. We are working to extend its application domains and keep innovating its capabilities.
SAT solver is a widely used tool to tackle the well-known satisfiablity (SAT) problem. The hybrid SAT solver takes advantage from both systematic search and local search. MIN-ONE SAT solver tries to find the optimum of a given objective function under the constraints of a SAT problem. Similarly MAX-SAT is another SAT optimization problem which tries to find a solution that maximize the satisfiablity of the formula. Both MIN-ONE SAT and MAX-SAT have lots of applications in various domains. I proposed a fast approximation algorithm for MIN-ONE SAT which also benefits MAX-SAT solving. These algorithms are implemented based on existing SAT solvers under Linux.
ATPG (Automatic Test Pattern Generator) is used to generate test patterns to test a TMR (Triple Modular Redundancy) circuit. This program was developed under Linux.
A research platform is built to conduct research on various learning techniques on model checking. The basic programs are invoked through Perl or Shell script, which enables a flexible framework to try the prototype ideas quickly.
A SAT based learning scheme is deployed to help test point insertion to increase the testing coverage. I did this during my internship at NEC research lab and a corresponding pattern has been filed. The programs were written primarily in C/C++ and script languages on both Solaris and Linux. The whole system was integrated into an industry design flow.
Summary: In my PhD research works, I mainly worked in the area of improving decision based search techniques in constraint satisfiability solver to benefit both design testing and formal verification. Most of the works were conducted under Linux with GNU development tools. C/C++, Perl and shell script languages were extensively used. Now I am working on a constraint solver powered software fuzzing tool.
Past Working projects:
Fingerprint USB device and Windows authentication system
Developing a fingerprint USB device and the Windows authentication system based on it. I was responsible for implementing firmware on the hardware platform (TI 5402 DSP + EZUSB), drivers for Windows 2000 and part of the logon authentication. Involved tools and language: TI DSP development kit, C, DDK, Windows Logon GINA Library.
VPN device
Developing a VPN device. This network device supports IPSEC, SNMP V1/V2, and X.509 certificate. The operating system is required as real time. I worked at its prototype validation stage.
Stock trading system
Being a team member to build the stock trading system. The system runs in a comprehensive environment constituted by SCO Unix, Redhat Linux and Windows. Tools: C++ Builder, Corba(Visibroker), SQL server
Summary: During my two years work at China, as a software engineer I was exposed to various projects, from embedded system firmware design to large scale database applications.