Embedded software is playing an important role in economy, government, and military. Since such software is often deployed in safety critical applications, correctness and reliability have become issues of utmost importance. Techniques for verification and validation traditionally fall into two main categories. One is formal verification, i.e., model checking and proof methodology. The other is abstract interpretation and static analysis. The goal of formal Verification is to prove that designs meet their specifications. Model Checking an automatic approach to verification, mainly useful when dealing with finite-state systems. Abstract Interpretation is a method for designing and comparing semantics of programs. It has been successfully used to infer run-time program properties that are instrumental for program optimization purposes. There are no clear dividing lines in between these different methodologies. In fact, they can be combined. An example is the exciting new research direction that combines abstraction (of infinite-state programs into finite-state ones) with model checking (of the finite-state system), that had produced formal and automatic verification of many complex systems. There is a growing conviction in the research community that hybrid methodologies are imperative for the process of formally verifying analyzing full-fledged reactive systems.
