Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method

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, especially for potentially undiscovered, pathological cases. To find such cases and assess their performance impacts within a single tool, we leverage the performance fuzzing algorithm BanditFuzz for the constraint solving backends of the ProB model checker. BanditFuzz utilises two multi-armed bandits to generate and mutate benchmark inputs for the ProB backends in a targeted manner. We describe how we adapted BanditFuzz for the B method, which differences exist to the original implementation for the SMT-LIB standard, and how we ensure well-definedness of the randomly generated benchmarks. Our experiments successfully uncovered performance issues in specific backends and even external tooling, providing valuable insights into areas which required improvement.