Plagge, Daniel and Leuschel, Michael and Lopatkin, Ilya and Iliasov, Alexei and Romanovsky, Alexander (2009) SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook. In: AFM09 (Automated Formal Methods), 27 June 2009, Grenoble, France. (In Press)
![[img]](../style/images/fileicons/application_pdf.png)
| PDF - Accepted Version 261Kb |
Abstract
PROB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using alternative techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether PROB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Subjects: | Tool developments > Model checking Tool developments > Rodin plug-ins |
| ID Code: | 133 |
| Deposited By: | Mr Ilya Lopatkin |
| Deposited On: | 13 Jul 2009 12:09 |
| Last Modified: | 19 Apr 2010 16:05 |
Repository Staff Only: item control page
