Abstract ESBMC, a bounded model checking (BMC) verifier based on SMT solving, has demonstrated its effectiveness in bug detection in recent software verification competitions. We extend its capabilities to enable branch coverage analysis and test suite generation. Our contributions are twofold: (1) we define a branch coverage property and instrument the control flow graph (CFG) to compute branch coverage using SMT solving, and (2) we propose an incremental multi-property reasoning algorithm for efficient and sound test case generation. ESBMC is ranked 7th in the category of Test-Comp 2025.

Abstract ESBMC implements many state-of-the-art techniques that combine abstract interpretation and model checking. Here, we report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC now employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, and forward-backward contractors. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.

Abstract Combining different verification and testing techniques together could, at least in theory, achieve better results than each individual one on its own. The challenge in doing so is how to take advantage of the strengths of each technique while compensating for their weaknesses. EBF 4.2 addresses this challenge for concurrency vulnerabilities by creating Ensembles of Bounded model checkers and gray-box Fuzzers. In contrast with portfolios, which simply run all possible techniques in parallel, EBF strives to obtain closer cooperation between them. This goal is achieved in a black-box fashion. On the one hand, the model checkers are forced to provide seeds to the fuzzers by injecting additional vulnerabilities in the program under test. On the other hand, off-the-shelf fuzzers are forced to explore different interleavings by adding lightweight instrumentation and systematically re-seeding them.

This paper presents ESBMC-CHERI -- the first bounded model checker capable of formally verifying C programs for CHERI-enabled platforms. CHERI provides run-time protection for the memory-unsafe programming languages such as C/C++ at the hardware level. At the same time, it introduces new semantics to C programs, making some safe C programs cause hardware exceptions on CHERI-extended platforms. Hence, it is crucial to detect memory safety violations and compatibility issues ahead of compilation. However, there are no current verification tools for reasoning over CHERI-C programs. We demonstrate the work undertaken towards implementing support for CHERI-C in our state-of-the-art bounded model checker ESBMC and the plans for future work and extensive evaluation of ESBMC-CHERI. The ESBMC-CHERI demonstration and the source code are available at https://github.com/esbmc/esbmc/tree/cheri-clang.

Despite increased understanding about psoriasis pathophysiology, currently there is a lack of predictive computational models. We developed a personalisable ordinary differential equations model of human epidermis and psoriasis that incorporates immune cells and cytokine stimuli to regulate the transition between two stable steady states of clinically healthy (non-lesional) and disease (lesional psoriasis, plaque) skin. In line with experimental data, an immune stimulus initiated transition from healthy skin to psoriasis and apoptosis of immune and epidermal cells induced by UVB phototherapy returned the epidermis back to the healthy state. Notably, our model was able to distinguish disease flares. The flexibility of our model permitted the development of a patient-specific "UVB sensitivity" parameter that reflected subject-specific sensitivity to apoptosis and enabled simulation of individual patients' clinical response trajectory. In a prospective clinical study of 94 patients, serial individual UVB doses and clinical response (Psoriasis Area Severity Index) values collected over the first three weeks of UVB therapy informed estimation of the "UVB sensitivity" parameter and the prediction of individual patient outcome at the end of phototherapy. An important advance of our model is its potential for direct clinical application through early assessment of response to UVB therapy, and for individualised optimisation of phototherapy regimes to improve clinical outcome. Additionally by incorporating the complex interaction of immune cells and epidermal keratinocytes, our model provides a basis to study and predict outcomes to biologic therapies in psoriasis.

Cyber-physical system models often feature stochastic behaviour that itself depends on uncertain parameters (e.g., transition rates). For these systems, verifying reachability amounts to computing a range of probabilities depending on how uncertainty is resolved. In general, this is a hard problem for which rigorous solutions suffer from the well-known curse of dimensionality. In this paper we focus on hybrid systems with random parameters whose distribution is subject to nondeterministic uncertainty. We show that for these systems the reachability probability is a smooth function of the nondeterministic parameters, and thus Gaussian processes can be used to approximate the reachability probability function itself very efficiently over its entire domain. Furthermore, we introduce a novel approach that exploits rigorous probability enclosures for training Gaussian processes. We apply our approaches to non-trivial hybrid systems case studies, and we empirically demonstrate their advantages with respect to standard statistical model checking.

We present ProbReach, a tool for verifying probabilistic reachability for stochastic hybrid systems, i.e., computing the probability that the system reaches an unsafe region of the state space. In particular, ProbReach will compute an arbitrarily small interval which is guaranteed to contain the required probability. Standard (non-probabilistic) reachability is undecidable even for linear hybrid systems. In ProbReach we adopt the weaker notion of delta-reachability, in which the unsafe region is overapproximated by a user-defined parameter (delta). This choice leads to false alarms, but also makes the reachability problem decidable for virtually any hybrid system. In ProbReach we have implemented a probabilistic version of delta-reachability that is suited for hybrid systems whose stochastic behaviour is given in terms of random initial conditions. In this paper we introduce the capabilities of ProbReach, give an overview of the parallel implementation, and present results for several benchmarks involving highly non-linear hybrid systems.