NPEDetector: Null dereference verification for Java programs
NPEDetector is a tool for sound, demand-driven, scalable null-dereference analysis for Java programs. The tool uses a backwards abstract-interpretation-based weakest-preconditions analysis. The underlying approach, as well empirical results obtained by applying the tool on real Java programs, are described in this publication.
The tool is available for download as a VirtualBox VM image.
Ross: Verifying safety of Java programs using points-to analysis
Ross is a tool that uses refinement-based points-to analysis to conservatively verify safety of Java programs from low-level errors. Specifically, the tool identifies all potentially unsafe downcast sites in a given program, and identifies all allocation sites that allocate immutable objects only. The underlying approach, as well empirical results obtained by applying the approach on real Java programs, are described in this publication.
The tool is available for download as a Java application.
DFAS: Static analysis of asynchronous systems
Asynchronous message-passing systems are employed frequently to implement distributed mechanisms, protocols, and processes. This work addresses the problem of precise data flow analysis for such systems. To obtain good precision, data flow analysis of message-passing systems needs to somehow skip execution paths that read more messages than the number of messages sent so far in the path, as such paths are infeasible at run time. Current data flow analysis techniques for such systems either compromise on precision by traversing infeasible paths in addition to feasible paths, or traverse only feasible paths but admit only finite abstract analysis domains. Our approach elides a large class of infeasible paths, and generalizes upon the state of art by admitting infinite abstract analysis domains (such as constant propagation). An application of data flow analysis, namely, verification of assertions, is also supported by our implementation.Our software tool is available for download here.
Matching service descriptions with existing code
The objective of this project is to develop tools to match a service in a domain model with fragments of code in a given existing application that potentially implement this service. The applications of this work include (a) identifying portions of code in the application that satisfy a business requirement, (b) transforming an existing monolithic application into a service-oriented architecture (SOA), and (c) migrating custom business logic from a custom application to a standard package.We describe an initial semi-automated technique for this problem in this publication.
A subsequent automated technique for this problem is described in this publication. We provide here data from two case studies that we performed using our technique, in which we matched two real Java applications with two real domain models.
A third, more precise automated technique for this problem is described in this publication. We provide here data from two similar case studies that we performed using this technique.