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.
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.
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.
