Egy olyan szervezetnek, ami vadászrepülőket meg önvezető autókat tervez kritikus fontosságú a vasakat működtető szoftverek megbízhatósága, melyre legjobb garanciát a formális, matematikai bizonyítás adhat. A baj az, hogy a programokt hagyományosan modellező gráfok elméletében…