Theory in practice for system design and verification

Abstract

Methodology and tools for assisting developers in building high-confidence hardware and software at a reasonable cost has been one of the central themes in computer science since its inception. The formal methods research on this problem has focused on two complimentary goals: to provide mathematical abstractions to manage the complexity of the design and to develop analysis tools to check that the implementation works correctly as intended. Achieving these goals has proved to be extremely challenging for two reasons. First, the scale and complexity of systems being designed remains a moving target as computers have transformed from special-purpose and stand-alone number-crunching processors to networked devices interacting with the physical world. Second, once formalized, the computational problem of verifying that a system meets its specification is undecidable in the general case and has intractable complexity even in special cases.