SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Formal Specification and Verification for Critical Systems: Tools, Achievements, and Prospects
 by Dr. John Rushby.

Abstract

Formal specification and verification use mathematical techniques to help document, specify, design, analyze, or certify computer software and hardware. Mathematically-based notation can provide specifications that are precise and unambiguous and that can be checked mechanically for certain types of error. Formal verification uses theorem proving techniques to establish consistency between one level of formal specification and another.

This paper describes some of the issues in the design and use of formal specification languages and verification systems, outlines some examples of the application of formal methods to critical systems, and identifies the benefits that may be obtained from this technology.

Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy