SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

A Formalization of the B-Method in Coq and PVS
 by Jean Paul Bodeveix, Mamoun Filali & César A. Muñoz.

Abstract
We formalize the generalized substitution mechanism of the B-method in the higher-order logic of Coq and PVS. Thanks to the dependent type feature of Coq and PVS, our encoding is compact and highly integrated with the logic supported by the theorem provers. In addition, we describe a tool that mechanizes, at the user level, most of the effort of the encoding.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy