The proof is in the testing...
The proof is in the testing: The Swiss breakthrough that will make software more reliable
The size and complexity of today's software programs can make it difficult to check their likely reliability.
Testing only goes so far: often after applications are released, it's a wait-and-see strategy, with developers sending out patches for products if and when major problems become evident.
Two computer scientists at the Swiss Federal Institute of Technology (École Polytechnique Fédérale de Lausanne or EPFL) hope to change that - using automated reasoning tools to replace validating software through testing with more accurate formal mathematical proofs.
While verification tools have developed significantly over the years, one stumbling block has been support for proofs that use mathematical induction.