@inproceedings{d955bbe10f254421a41423d59b2a0d29,
title = "Discharging proof obligations from Atelier B using multiple automated provers",
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.",
author = "David Mentr{\'e} and Claude March{\'e} and Filli{\^a}tre, \{Jean Christophe\} and Masashi Asuka",
year = "2012",
month = jul,
day = "23",
doi = "10.1007/978-3-642-30885-7\_17",
language = "English",
isbn = "9783642308840",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "238--251",
booktitle = "Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Proceedings",
note = "3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ 2012 ; Conference date: 18-06-2012 Through 21-06-2012",
}