Abstract Context With artificial intelligence (AI) being well established within the daily lives of research communities, we turn our gaze toward formal methods (FM). FM aim to provide sound and verifiable reasoning about problems in computer science. Objective We conduct a systematic mapping study to overview the current landscape of research publications that apply AI to FM. We aim to identify how FM can benefit from AI techniques and highlight areas for further research. Our focus lies on the previous five years (2019–2023) of research. Method Following the proposed guidelines for systematic mapping studies, we searched for relevant publications in four major databases, defined inclusion and exclusion criteria, and applied extensive snowballing to uncover potential additional sources. Results This investigation results in 189 entries which we explored to find current trends and highlight research gaps. We find a strong focus on AI in the area of theorem proving while other subfields of FM are less represented. Conclusions The mapping study provides a quantitative overview of the modern state of AI application in FM. The current trend of the field is yet to mature. Many primary studies focus on practical application, yet we identify a lack of theoretical groundwork, standard benchmarks, or case studies. Further, we identify issues regarding shared training data sets and standard benchmarks.

The B method is a formal method supported by a variety of tools. Those tools, like any complex piece of software, may suffer from performance issues and vulnerabilities. In this work, we leverage performance fuzzing to generate inputs that uncover potential performance issues in the ProB model checker and its employed constraint solving backends. These backends include a mix of constraint solvers that are directly implemented in ProB or are bindings to third-party solvers such as Z3. During constraint solving, any such backend can be selected to solve a given constraint. As performance fuzzing algorithm, we utilise BanditFuzz. BanditFuzz utilises two multi-armed bandit agents to control a fuzz generator and mutator. This way, the algorithm can generate targeted input benchmarks that are well-formed inputs to ProB yet exhibit significant performance differences between the employed constraint solvers. We describe how we adapted BanditFuzz for the B method, what differences exist to the original implementation for the SMT-LIB standard, and how we ensure well-definedness of the randomly generated benchmarks. Further, we consider two opposed approaches to integrate BanditFuzz with ProB : as an external tool that considers ProB as a black box, and as an internal tool that has direct dependency onto ProB ’s source code and can capitalise on available, internal functionalities. Our experiments successfully uncovered performance issues in specific backends and even external tooling, providing valuable insights into areas that required improvement. Ultimately, we conclude that BanditFuzz is a valuable tool for development and advocate for the external architecture, as its benefits outweigh the drawbacks.

Abstract In this article, we present an approach to the ABZ 2020 case study that differs from those usually presented at ABZ: Rather than using a (correct-by-construction) approach following a formal method, we use C for a low-level implementation instead. We strictly adhere to test-driven development for validation, and only afterwards apply model checking using CBMC for verification. While the approach has several benefits compared to the more rigorous approaches, it also provides less mathematical clarity and overall less thorough verification. In consequence, our realization of the ABZ case study serves as a baseline reference for comparison, allowing to assess the benefit provided by the various formal modeling languages, methods and tools.

Abstract The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present a Java API to the ProB animator and model checker. We describe several case studies that use this API as enabling technology to interact with a formal specification at runtime.