History for Technical Background

added:


added:

  1. Analysis: Expressing and deriving properties of the software 
such as the ranges and types of values assigned to variables, relationships between 
variables, datatype invariants, execution time, and space usage. 


changed:
-can also be used for test case generation and plan synthesis.
can also be used for test case generation, extended static checking, translation validation, predicate abstraction, and plan synthesis.

changed:
-automated theorem proving frameworks.  The  
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
automated theorem proving frameworks that employ induction, case analysis, simplification, rewriting, and quantifier instantiation 
to establish deeper properties of software that may not be amenable 
to automated approaches such as model checking and static analysis.  
Deductive approaches have been applied to such critical system properties such as cache coherence, fault tolerance, and distributed
algorithms.  

It is important to note that all of the approaches to automated verification can be applied at all levels of abstraction from 
high-level specification to hardware designs.  They can also be 
used for verifying properties of the software as well as for relating
different levels of abstraction through refinement.