TY - GEN
T1 - Discharging proof obligations from Atelier B using multiple automated provers
AU - Mentré, David
AU - Marché, Claude
AU - Filliâtre, Jean Christophe
AU - Asuka, Masashi
PY - 2012/7/23
Y1 - 2012/7/23
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84863917985
U2 - 10.1007/978-3-642-30885-7_17
DO - 10.1007/978-3-642-30885-7_17
M3 - Conference contribution
AN - SCOPUS:84863917985
SN - 9783642308840
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 238
EP - 251
BT - Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings
T2 - 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012
Y2 - 18 June 2012 through 21 June 2012
ER -