Hardware and software systems will inevitably grow in
scale and functionality. Because of this increase in complexity, the
likelihood of subtle errors is much greater. Moreover, some of these
errors may cause catastrophic loss of money, time, or even human life.
A major goal of software engineering is to enable developers to
construct systems that operate reliably despite this complexity. One
way of achieving this goal is by using <#57#>formal methods<#57#>, which
are mathematically-based languages, techniques, and tools for
specifying and verifying such systems. Use of formal methods does not
<#58#>a priori<#58#> guarantee correctness. However, they can greatly
increase our understanding of a system by revealing inconsistencies,
ambiguities, and incompletenesses that might otherwise go undetected.
The first part of this report assesses the state of the art in <#59#>
specification<#59#> and <#60#>verification<#60#>. For verification, we
highlight advances in <#61#>model checking<#61#> and <#62#>theorem proving<#62#>.
In the three sections on specification, model checking, and theorem
proving, we explain what we mean by the general technique and briefly
describe some successful case studies and well-known tools. The second part of
this report outlines future directions in fundamental concepts, new
methods and tools, integration of methods, and education and
technology transfer. We close with summary remarks and pointers to
resources for more information.