February 18, 2014 · 7:00 PM
At our next monthly meeting we will have a very interesting talk by Adam Streck about Model Checking and Code Analysis:
On July 1996 the rocket Ariane 5 exploded 40 seconds after start due to an overflow in assigning a 64-bit floating point number to a 16-bit integer causing a loss over billion dollars. This and multiple other errors in "safety-critical" systems drive development of tools that can guarantee safety of a program beyond capabilities of classical testing. Probably the most famous member of the family, model checking, is a formal-logic based method for verification of, but not limited to, computer software. The talk will give in a peek into theory behind this method and discuss some of the model-checking tools for C++ developers available today.