A Role for Formal Methodists

  • Fred B. Schneider
Conference paper
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 9)


Proving “correctness” of entire systems is not now feasible, nor is it likely to become feasible in the foreseeable future. Establishing that a large system satisfies a non-trivial specification requires a large proof. Without mechanical support, building or checking such a proof is not practical. Even with mechanical support, designing a large proof is at least as difficult as designing a large program. We are barely up to the task of building large and complex systems that almost work; we are certainly not up to building such systems twice — once in a programming language and once in a logic — without any flaws at all.


Model Checker Formal Method Large System Mechanical Support Foreseeable Future 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • Fred B. Schneider
    • 1
  1. 1.Department of Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations