Lunedì 15-3, h14:30

Claudio Castellini and Jacopo Mantovani AI-Lab, DIST, University of Genova

Title
Software Model Checking: towards every programmer's dream

Abstract
introduced in the late 80s by Clarke, Model Checking is rapidly becoming of common use for hardware verification, that is, mathematically ensuring that a Boolean circuit respects a property. In this talk, we will be outlining the new frontier in Model Checking: applying this technique to software. This requires pushing MC to infinite-state systems, given that, unlike circuits, programs usually have infinite-domain data-structures such as integer and real numbers, lists, arrays.

The grand goal of Software Model Checking is then to answer the question:

given a piece of code and a requirement,
  say whether the requirement is respected, or
  produce a counter-example.

This is tantamount to realizing every programmer's dream: to automatically debug one's own programs.

@LIRA-Home