New Applications and Techniques for Constraint Programming in B

The safety of software systems is gaining importance due to the almost indispensable integration of software in modern everyday life. Formal methods are a fundamental approach for the design and verification of software and hardware systems, one of which is the B-Method. This thesis is a selection of my co-authored manuscripts on the B-Method and the ProB tool.

In the first part, a translation of a popular formal specification language called Alloy to classical B is presented, which is automated by ProB. A difference between both languages is that Alloy’s syntax is flexible and resembles object-oriented programming languages while B’s syntax is strictly typed and rooted in set theory, mathematics, and logic. In contrast to Alloy, B also allows defining infinite and arbitrarily nested sets and relations. Further, B has operational semantics, which eases the definition of state-based systems. Empirical results have shown benefits for performance and soundness of B and ProB compared to Alloy when solving integer constraints, and benefits for performance of the Alloy Analyzer compared to ProB when solving relational constraints. This work contributed to an ongoing discussion in the Alloy community to integrate state-based concepts in the core language of Alloy and Satisfiability Modulo Theories (SMT) in the Alloy Analyzer. Besides that, this work improved the communication between the Alloy and B communities.

The second part of this thesis deals with constraint solving, which is one of the most important features of any formal verification tool. ProB’s constraint solver has proven to be powerful for many problems. Yet, its use of plain saturation-based techniques often prevents finding contradictions, especially when considering infinite domains. We present additional constraint solving backends for ProB using techniques of SMT, which enable to learn from conflicts and leverage the power of Boolean satisfiability solving. In particular, we present an extended translation from B to SMT-LIB and integration of Z3 in ProB as well as a custom implementation of SMT in ProB. Empirical results have shown benefits of clause learning and abstractions to Boolean satisfiability solving compared to ProB’s native constraint solver, especially when it comes to finding contradictions. For instance, it can be possible to identify a contradiction in a formula’s Boolean abstraction without interpreting any theory constraint for which the satisfiability might be undecidable. Z3’s theory solvers have further shown benefits in solving constraints involving infinite domains and integer arithmetic. The overall results, however, have shown that no constraint solver is the best for solving all kinds of constraints. For the verification of formal systems, it is thus beneficial to have a large portfolio of different constraint solving backends, as is the case for the ProB tool.

Joshua Schmidt. (2023). "New Applications and Techniques for Constraint Programming in B" Dissertation. Universitäts- und Landesbibliothek Düsseldorf. https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=64042