My main research interests are in software engineering,
especially in program analysis and automated testing.
For example, how can we reduce the high number of false bug warnings
produced by automated bug-finding tools?
A related question I am also working on is how to automatically infer
specifications of object-oriented programs from existing test suites.
This paper discusses the implementation of our dynamic symbolic data structure repair tool, DSDSR. We provide initial empirical results of applying DSDSR on different formulations of the same correctness condition and compare DSDSR with a state-of-the-art tool, Juzi.
Dynamic symbolic data structure repair (Proc. 32nd ACM/IEEE International Conference on Software Engineering (ICSE), Volume 2, Emerging Results Track, 2010)
We motivate how dynamic symbolic techniques enable generic repair to support a wider range of correctness conditions and present DSDSR, a novel repair algorithm based on dynamic symbolic execution. We implement the algorithm for Java and report initial empirical results to demonstrate the promise of our approach for generic repair.
DySy uses the concolic execution system Pex to detect invariants in arbitrary .Net programs. DySy can derive much better targeted invariants than previous, template-based approaches, such as Daikon.
We propose a two-pass algorithm to support interfaces and method overriding in dynamic invariant detection. The first pass associates a method call with the method executed and all methods it overrides up to and including the static receiver to derive the methods' preconditions. The second pass associates a method call with every supertype whose precondition is met to derive non-conflicting postconditions.
Dsc+Mock is a dynamic symbolic test case generator that can reason about type constraints and can generate mock classes that satisfy such constraints. Our prototype implementation achieved higher code coverage than related test case generators that do not generate mock classes, such as Pex.
This is a superset of our earlier ASE 2007 paper, expanding the treatment of test data generation. Object-Role Modeling (ORM) is a popular language for specifying database schemas. It supports many constraints and is undecidable in general. We pick a restricted subset of ORM that is decidable in polynomial time and implement a fast automated solver. We found that our ORM subset covers the vast majority of constraints used in our sample of over 160 ORM diagrams from industrial practice. Our earlier 2007 paper received the Best Paper Award at ASE 2007.
An existing static program analysis that over-approximates the execution paths of the analyzed program can be made more precise for automatic testing in an object-oriented programming language, by combining the over-approximating analysis with usage-observing and under-approximating analyses. This summarizes the DSD-Crasher, Check 'n' Crash, and JCrasher work. Unpublished material includes a critical review of the performed evaluation, lessons learnt, and how to generalize the approach.
This is a superset of our earlier ISSTA 2006 paper on DSD-Crasher, adding a high-level overview, experiments with subjects from the software-artifact infrastructure repository (SIR), more related work, and a discussion on increasing code coverage by reasoning about implicit control flow branches.
Object-Role Modeling (ORM) is a popular language for specifying database schemas. It supports many constraints and is undecidable in general. We pick a restricted subset of ORM that is decidable in polynomial time and implement a fast automated solver. We found that our ORM subset covers the vast majority of constraints used in our sample of over 160 ORM diagrams from industrial practice. Received the Best Paper Award.
This is an invited paper that reviews our bug finding tools: Check 'n' Crash addresses the language-level unsoundness of static bug finding tools whereas DSD-Crasher also addresses their user-level unsoundness. We use a small case study to compare JCrasher, ESC/Java, Check 'n' Crash, and DSD-Crasher.
DSD-Crasher first uses Daikon to capture the subject's intended execution behavior, then statically analyzes this restricted domain with ESC/Java, and finally lets Check 'n' Crash generate and execute concrete test-cases to verify the results of ESC/Java. Received an ACM SIGSOFT Distinguished Paper Award.
Check 'n' Crash uses ESC/Java to statically search for problems like null dereference, illegal type cast, or illegal array manipulation. Check 'n' Crash compiles ESC's results to JUnit test cases and executes them to filter out ESC's false positives.
JCrasher generates random test cases by chaining object constructors. It filters test case execution and presents only those that expose a bug or lack of robustness. It also enables JUnit to efficiently undo the changes a test case has done to testee class fields.
