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.

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.


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