Marc Pantel, Associate Professor in Computer Science

 

This session illustrates the proof of simple imperative programs using Hoare logic both with the Coq proof assistant and the Why3 toolset.

 
 
hoarecoqwhy3.txt · Last modified: 2017/01/20 12:05 by pantel
Recent changes RSS feed Creative Commons License Valid XHTML 1.0 Valid CSS Driven by DokuWiki
Drupal Garland Theme for Dokuwiki