Home > Static Analysis > FLAVERS
Static Analysis
Finite-State Verification
Property Specification
Fault-Tree Analysis
Failure Mode and Effect Analysis
MPI Verification
Additional Information
All FLAVERS Publications
Licensed Software


Using data flow analysis techniques, FLAVERS can very quickly compute an approximate solution to a verification query. If the results are inconclusive, we have developed an approach for incrementally and selectively improving the precision until the property is proven or a counter example is described. Thus, we have been exploring the hypothesis that with fine grained control over precision and with a highly optimized program model and data flow based reasoning engine, finite state verification can be applied to large, complex distributed systems. The FLAVERS prototype has successfully been used on some industrial demonstration projects and is currently being extended to evaluate Java programs.

FLAVERS is a flexible, powerful system for automatically guaranteeing the absence or detecting the presence of a wide range of user-specified properties or behaviors in both sequential and concurrent systems. FLAVERS complements traditional testing approaches, which only demonstrate the presence or absence of errors for the specific test cases that have been executed. It also complements formal verification methods, which employ more comprehensive analysis, but require extensive expertise on the part of the user.

FLAVERS is built using the FLAVERS toolkit, a flexible architecture and component library that facilitates the development of FLAVERS analyzers.

The toolkit allows FLAVERS to be extended with additional specialized data flow analyzers and to be applied to a wide range of languages and systems. FLAVERS has been applied to the analysis of Ada and C++ and Java is underway. It has also been used for the analysis of network protocols and architecture specifications.


  • User-definable properties and models
  • Comprehensive API supports application to a wide range of domains and languages
  • Visualization tools aid in understanding concurrent system behavior
  • FLAVERS analyses can improve the quality of a system throughout its lifecycle
    • During design to verify:
      • that the architecture meets the requirements
      • that the design is consistent with the architecture
    • During testing to generalize test cases to all executions
    • During debugging to:
      • identify the cause of a fault
      • confirm that the fault has been removed

Selected Publications


Flow Analysis for Verifying Properties of Concurrent Software Systems
Matthew B. Dwyer, Lori A. Clarke, Jamieson M. Cobleigh, Gleb Naumovich, ACM Transactions on Software Engineering and Methodology (TOSEM), Vol. 13, No. 4, pp. 359-430, October 2004. (UM-CS-2004-006)

This is an updated version of UM-CS-1999-052 and UM-CS-2003-030.

[ ACM ] [ PDF ] [ Appendices B and C ]


This site is maintained by the Laboratory for Advanced Software Engineering Research.
© 2006 University of Massachusetts AmherstSite Policies