Software Model Construction for Finite-state Verification

Overview

picture here

Talks

• A high-level summary of the project as of Oct, 1998.
• Dave Schmidt's presentation at the Nov, 1998 DARPA Formal Methods PI Meeting.

Abstraction-based Program Specialization

overview

Papers

• Staging Static Analyses Using Abstraction-based Program Specialization , John Hatcliff, Matthew B. Dwyer, Shawn Laubach, and David Schmidt. This paper is published as KSU CIS TR 98-5 and a more compact version appeared in LNCS 1490 (Principles of Declarative Programming: 10th International Symposium, PLILP'98), 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 will appear in ACM Computing Surveys. An abstract of this paper is also available.
• Specializing Configurable Systems for Finite-state Verification , John Hatcliff, Matthew B. Dwyer, Shawn Laubach, and Nanda Muhammad. This paper is published as KSU CIS TR 98-4 and has been submitted for publication. An abstract of this paper is also available.

Software

Program Slicing

overview

Papers

• Slicing Software for Model Construction , Matthew B. Dwyer and John Hatcliff, This paper is published as KSU CIS TR 98-14 and has been submitted for publication. An abstract of this paper is also available.

Software

Source Language Processing

overview

Papers

Software

Specification Patterns

overview

The Specification Patterns Web-Site

Papers

• Property Specification Patterns for Finite-state Verification, Matthew B. Dwyer, George S. Avrunin and James C. Corbett in the 2nd Workshop on Formal Methods in Software Practice, March, 1998. An abstract of this paper is also available.
• Patterns in Property Specifications for Finite-state Verification , Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. This paper is published as KSU CIS TR 98-9 and has been submitted for publication. An abstract of this paper is also available.

Software

Filter-based Analysis

overview

Papers

• Limiting State Explosion with Filter-Based Refinement, Matthew B. Dwyer and David A. Schmidt. in Proceedings of the ILPS'97 Workshop on Verification, Model Checking and Abstract Interpretation, October, 1997. An abstract of this paper is also available.
• Modular Flow Analysis for Concurrent Software, Matthew B. Dwyer. in Proceedings of the 12th International Conference on Automated Software Engineering, November, 1997. An abstract of this paper is also available.
• 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 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. An abstract of this paper is also available.

Talks

• FSE'98 slides

Raw Materials for Case Studies

• Replicated Workers Framework
• Generic Container Implementations

Software

Transition System Generation

overview

Papers

• Jay TSE 96
• Translating Ada Programs for Model Checking : A Tutorial, Matthew B. Dwyer, James C. Corbett and Corina S. Pasareanu. This paper is published as KSU CIS TR 98-12. An online version of this paper (with additional resources linked) is available here.

Software

Evaluation

overview

Papers

Software

Alias Analysis

overview

Papers

• Jay

Software

People

• George Avrunin
• James Corbett
• Matt Dwyer
• John Hatcliff
• Shaun Laubach
• Corina Pasareanu
• Dave Schmidt
• Hongjun Zheng

Related Projects

• sable

Support

• NASA project NAG-02-1209
• NSF-EIA Experimental Software Systems (ESS) project 9708184
• NSF-CCR CAREER project 9703094.
• NSF-CCR CAREER project JOHN?.
• NSF-CCR/DARPA Evolutionary Design of Complex Systems (EDCS) project 9633388. subprojects