Tuning the Alt-Ergo SMT Solver for B Proof Obligations

Abstract : In this paper, we present recent developments on the Alt-Ergo SMT-solver to efficiently discharge proof obligations (PO) 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. Benchmarks realized on more than 10,000 PO generated from industrial B projects show significant improvements.
Document type :
Conference papers
Complete list of metadatas

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/hal-01093000
Contributor : Sylvain Conchon <>
Submitted on : Tuesday, December 9, 2014 - 10:02:19 PM
Last modification on : Friday, October 4, 2019 - 1:47:31 AM
Long-term archiving on : Tuesday, March 10, 2015 - 12:30:12 PM

File

alt-ergo.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01093000, version 1

Collections

Citation

Sylvain Conchon, Mohamed Iguernelala. Tuning the Alt-Ergo SMT Solver for B Proof Obligations. ABZ, Jun 2014, Toulouse, France. ⟨hal-01093000⟩

Share

Metrics

Record views

263

Files downloads

285