BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Tests and Proofs in Isabelle - Yakoub Nemouchi\, University of Yor
 k
DTSTART:20200310T143000Z
DTEND:20200310T145000Z
UID:TALK140647@talks.cam.ac.uk
CONTACT:Jean Pichon-Pharabod
DESCRIPTION:Formal verification techniques have seen a remarkable boost in
  recent years. In particular\, methods based on deductive code-verificatio
 n\, model-checking\, and code-generation techniques can\, within the bound
 aries of certain foundational assumptions\,\nprovide an absolute guarantee
  in a sense for the correctness of the components of computer based system
 s towards a specification. \nHowever\, the assumptions underlying the mode
 l\, which involves assumptions on the correctness of the compiler\, \nhard
 ware correctness\, etc.\, can cause a significant gap between the specifie
 d behavior and the behavior of the code in its execution context. \nThus\,
  the verification of the underlying foundational assumptions\, ie.\, the t
 rusted computing base (TCB) is necessary. \nThis can be achieved via prove
 r based testing\, where tests\nare generated from the verified model and e
 xecuted on the verified code. During my talk\, I will introduce a set of a
 pplications for this approach\, namely\, where two formal methods\, ie.\, 
 tests and proofs\, are combined together on a top of the interactive theor
 em proving environment Isabelle.
LOCATION:Computer Lab\, SS03
END:VEVENT
END:VCALENDAR