recentpopularlog in

MaxBarraclough : formalmethods   11

Tokeneer - AdaCore case study
Links to full PDF. Discussion of the faults they found at around p46. Interesting 'Analysis' section at p59.

See also https://blog.adacore.com/tokeneer-fully-verified-with-spark-2014 , https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove/tests/tokeneer

They used Z Notation for formal modelling.
formalMethods  papers  Ada  SPARK  Znotation 
7 weeks ago by MaxBarraclough

Copy this bookmark:





to read