Abstract
In this paper, we present recent developments in the Alt-Ergo SMT-solver to efficiently discharge proof obligations (POs) generated by Atelier B. This includes a new plugin architecture to facilitate experiments with different SAT engines, new heuristics to handle quantified formulas, and important modifications in its internal data structures to boost performances of core decision procedures. Experiments realized on more than 10,000 POs generated from industrial B projects show significant improvements. © 2014 Springer-Verlag.
Author supplied keywords
Cite
CITATION STYLE
Conchon, S., & Iguernelala, M. (2014). Tuning the Alt-Ergo SMT solver for B proof obligations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8477 LNCS, pp. 294–297). Springer Verlag. https://doi.org/10.1007/978-3-662-43652-3_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
