Static Analysis Research

We're interested in efficient static analyses that support program verification and validation activities. Our work fits into three broad areas:

applying flow analysis to verifying specifications of real software systems
incorporating semantically well-founded abstractions into model-checking of software systems
using partial evaluation to enable static analysis of configurations of dynamic software systems
developing software systems that support the efficient implementation of complex flow analysis computations

Flow Analysis for Verifying Specifications (FLAVERS)

FLAVERS (FLow Analysis for VERifying Specifications) is a static analysis technique that enables cost-effective verification of finite-state specifications of the intended behavior of sequential or concurrent software.

Papers

We've written some about FLAVERS

Flow Analysis for Verifying Specifications of Concurrent and Distributed Software, Matthew B. Dwyer and Lori A. Clarke. Submitted for journal publication.
Modular Flow Analysis for Concurrent Software, Matthew B. Dwyer. This paper is published as KSU CIS TR 96-6 and will appear in the 12th International Conference on Automated Software Engineering, November, 1997. An abstract of this paper is also available.
Verification of Concurrent Software with FLAVERS (Formal Demonstration), Gleb Naumovich, Lori A. Clarke, Leon J. Osterweil, and Matthew B. Dwyer, Proceedings of the 19th International Conference on Software Engineering, May, 1997.
Data Flow Analysis for Verifying Correctness Properties of Concurrent Programs, Matthew B. Dwyer, Phd Dissertation, University of Massachusetts, Amherst, MA, September 1995.
Data Flow Analysis for Verifying Properties of Concurrent Programs, Matthew B. Dwyer and Lori A. Clarke, Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, New Orleans, LA, December 1994, pp. 62-75. An abstract of this paper is also available.

This work is funded by NSF under CCR-9703094 and CCR-9708184.

Model Checking with Abstractions

We are working to take the concept of abstraction that is fundamental to flow analysis and abstract interpretation and use it as the basis for efficient model checking of software. We're pursuing this in both theoretical and applied directions. The applied direction is looking at abstractions for domain-specific model checking. We've written some tutorial notes on the use of a toolset that converts Ada source code to the input languages of the popular model checkers SPIN and SMV. This toolset is used in some of the experiments described in the papers below.

Papers

We've written some about MCA

Model Checking Generic Container Implementations, Matthew B. Dwyer and Corina S. Pasareanu, This paper is published as KSU CIS TR 98-10 and has been submitted for publication.
Filter-based Model Checking of Partial Systems, Matthew B. Dwyer and Corina S. Pasareanu. This paper is published as KSU CIS TR 98-3 and will appear in the ACM SIGSOFT Symposium on the Foundation of Software Engineering, November, 1998.
Model Checking Graphical User Interfaces Using Abstractions, Matthew B. Dwyer, Vicki Carr and Laura Hines. This paper is published as KSU CIS TR 97-1 and will appear in the Joint meeting of the 6th European Software Engineering Conference togther with 5th ACM SIGSOFT Symposium on the Foundation of Software Engineering, September, 1997. An abstract of this paper is also available.
Limiting State Explosion with Filter-Based Refinement, Matthew B. Dwyer and David A. Schmidt. This paper is published as KSU CIS TR 97-9 and will appear at the ILPS'97 Workshop on Verification, Model Checking and Abstract Interpretation, October, 1997. An abstract of this paper is also available.

This work is funded by NSF and DARPA under CCR-9633388 and CCR-9703094.

Partial Evaluation to Enable Static Concurrency Analysis

John Hatcliff and I have been working on applying partial evaluation as a front-end technology for "compiling" abstract finite-state transition for automated verification. It's amazing how many analysis techniques that are used in concurrency analysis tools turn out to be special cases of partial evaluation techniques.

Papers

Staging Static Analyses Using Abstraction-based Program Specialization , John Hatcliff, Matthew B. Dwyer and Shawn Laubach. This paper is published as KSU CIS TR 98-5 and a smaller version of this paper will appear in the Joint International Symposiums on Programming Languages, Implementations, Logics, and Programs (PLILP) and Algebraic and Logic Programming (ALP), September, 1998.
Using Partial Evaluation to Enable Verification of Concurrent Software, Matthew B. Dwyer, John Hatcliff, and Muhammad Nanda This paper is published as KSU CIS TR 97-15 and has been submitted for publication. An abstract of this paper is also available.

This work is funded by NSF and DARPA under CCR-9633388.

Supporting Program Flow Analysis

We are engaged in a collection of projects aimed at providing support for the development of efficient precise solutions to demanding static program analysis problems. Topics we are investigating include

Reusable Frameworks for building flow analyzers
Combined and qualified flow analyses
Parallel solution of monotone, bounded flow analysis problems
Multi-source flow analysis frameworks

Papers

We've written some about these things

A Flexible Architecture for Building Data Flow Analyzers, Matthew B. Dwyer and Lori A. Clarke, Proceedings of the Eighteenth International Conference on Software Engineering, Berlin, Germany, March 1996. An abstract of this paper is also available.
Data Flow Analysis Frameworks for Concurrent Programs, Matthew B. Dwyer. This paper is published as KSU CIS TR 95-8. An abstract of this paper is also available. An alternate version of this work is described in an extended abstract.

Matt Dwyer (dwyer@cis.ksu.edu) Last updated 8 June 1997.