Abstract
We present a method to discharge proof obligations from Atelier B using multiple SMT solvers. It is based on a faithful modeling of B's set theory into polymorphic first-order logic. We report on two case studies demonstrating a significant improvement in the ratio of obligations that are automatically discharged. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Mentré, D., Marché, C., Filliâtre, J. C., & Asuka, M. (2012). Discharging proof obligations from Atelier B using multiple automated provers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7316 LNCS, pp. 238–251). https://doi.org/10.1007/978-3-642-30885-7_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
