2nd International Workshop on INvariant Generation, York, UK

<pre>Program verification has a long research tradition, but so far<br>its impact on development of safety critical software has been<br>relatively limited&#046; A key impediment has been the overhead<br>associated with providing and debugging auxiliary invariant<br>annotations&#046; As the design and implementation of reliable<br>software remains an important issue, any progress in this area<br>will be of utmost importance for future developments in IT&#046;<br>The logically deep parts of the code are characterized by<br>(nested) loops or recursions&#046; For these parts, formal program<br>verification is an appropriate tool&#046; One of its biggest<br>challenges is automated discovery of inductive assertions,<br>leading to verification of safety and security properties of<br>programs&#046;<br>The increasing power of automated theorem proving and computer<br>algebra has opened new perspectives for computer aided program<br>verification; in particular for the automatic generation of<br>inductive assertions in order to reason about loops and<br>recursion&#046; Especially promising breakthroughs are invariant<br>generation techniques by Groebner bases, quantifier<br>elimination, and algorithmic combinatorics, which can be used<br>in conjunction with model checking, theorem proving, static<br>analysis and abstract interpretation&#046;</pre>