Abstract This paper introduces several techniques that improve the scalability of the deductive verification of data-level parallel programs working on arrays and matrices. First of all, we introduce a technique to rewrite expressions with (nested) quantifiers, so suitable triggers can be generated for these expressions. We have proven this rewrite technique correct using a theorem prover. Second, we make reasoning about potentially overlapping arrays easier, by providing specification constructs to indicate and verify that two arrays are not aliases, or that they are immutable, so they can be modelled as mathematical sequences. All our techniques are implemented in the VerCors program verifier. We illustrate how the combination of our techniques improves scalability via a large number of experiments. Using our techniques on a set of typical GPU kernels, we achieve a reduction of verification time by, on average, a factor of 9, with outliers being up to 150 times faster. Additionally, applying these techniques to earlier experiments and an earlier case study of a radio telescope pipeline permitted to obtain verification results that were previously either unobtainable or only in a significantly longer verification time.

In 2009, the Simple Language of Communicating Objects ( Slco ) Domain-Specific Language was designed. Since then, a range of tools have been developed around this language to conduct research on a wide range of topics, all related to the construction of complex, component-based software, with formal verification being applied in every development step. This addresses our vision that formal verification should be seamlessly integrated into Model-Driven Software Engineering, to effectively develop correct software. In this article, we present this range of topics, and draw connections between the various, at first glance disparate, research results. We discuss the current status of the Slco framework, i.e., the language in combination with the tools, related work w.r.t. each of the topics, and plans for future work.

Abstract GPUexplore $$^{\textsc {prob}}$$ P R O B is an extension of GPUexplore that constructs state spaces of Markov Chains and performs probabilistic model checking entirely on a GPU. It can construct the state space of a Discrete-Time Markov Chain and verify that it satisfies a given Probabilistic Computation-Tree Logic formula. We present the tool, and experimentally compare with Storm, demonstrating its effectiveness.

This special collection arose from the 18th International Conference on integrated Formal Methods (iFM 2023), which was held in Leiden, The Netherlands from 13 to 15 November 2023.

Abstract GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. Such optimizations can introduce errors. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone. This paper presents an approach to automatically apply optimizations to GPU programs while preserving provability by defining annotation-aware transformations . It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. The approach has been implemented in the Alpinist tool and we evaluate Alpinist in combination with the VerCors program verifier, to automatically apply optimizations to a collection of verified programs and reverify them.

Abstract The HaliVer tool integrates deductive verification into the popular scheduling language Halide, used for image processing pipelines and array computations. HaliVer uses VerCors, a separation logic-based verifier, to verify the correctness of (1) the Halide algorithms and (2) the optimised parallel code produced by Halide when an optimisation schedule is applied to an algorithm. This allows proving complex, optimised code correct while reducing the effort to provide the required verification annotations. For both approaches, the same specification is used. We evaluated the tool on several optimised programs generated from characteristic Halide algorithms, using all but one of the essential scheduling directives available in Halide. Without annotation effort, HaliVer proves memory safety in almost all programs. With annotations HaliVer, additionally, proves functional correctness properties. We show that the approach is viable and reduces the manual annotation effort by an order of magnitude.

Abstract The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. In this paper, we propose a new algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae [45] that is aimed at running on such devices. We prove its correctness and termination guarantee, and experimentally compare a GPU implementation with state-of-the-art LTL model checkers. Our new GPU LTL-checking algorithm is up to 150 $$\times $$ × faster on proving the correctness of a system than LTSmin running on a 32-core high-end CPU, and is more economic in using the available memory.

Abstract Since 2013, the leading SAT solvers in SAT competitions all use inprocessing, which, unlike preprocessing, interleaves search with simplifications. However, inprocessing is typically a performance bottleneck, in particular for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As one of the main challenges in GPU programming is memory locality, we present new compact data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improve memory locality. Our new parallel variable elimination algorithm is roughly twice as fast as previous work. Moreover, we augment the variable elimination with the first parallel algorithm for functional dependency extraction in an attempt to find more logical gates to eliminate that cannot be found with syntactic approaches. We present a novel algorithm to generate clausal proofs in parallel to validate all simplifications running on the GPU besides the CDCL search, giving high credibility to our solver and its use in critical applications such as model checkers. In experiments, our new solver ParaFROST solves numerous benchmarks faster on the GPU than its sequential counterparts. With functional dependency extraction, inprocessing in ParaFROST was more effective in reducing the solving time. Last but not least, all proofs generated by ParaFROST were successfully verified.

Abstract Various techniques have been proposed to accelerate explicit-state model checking with GPUs, but none address the compact storage of states, or if they do, at the cost of losing completeness of the checking procedure. We investigate how to implement a tree database to store states as binary trees in GPU memory. We present fine-grained parallel algorithms to find and store trees, experiment with a number of GPU-specific configurations, and propose a novel hashing technique, called Cleary-Cuckoo hashing, which enables the use of Cleary compression on GPUs. We are the first to assess the effectiveness of using a tree database, and Cleary compression, on GPUs. Experiments show processing speeds of up to 131 million states per second.

This article presents a way to implement many-sorted term rewriting on a GPU. This is done by letting the GPU repeatedly perform a massively parallel evaluation of all subterms. Innermost many-sorted term rewriting is experimentally compared with a relaxed form of innermost many-sorted term rewriting, and two different garbage collection mechanisms, to remove terms that are no longer needed, are discussed and experimentally compared. It is concluded that when the many-sorted term rewrite systems exhibit sufficient internal parallelism, GPU rewriting substantially outperforms the CPU. Both relaxed innermost many-sorted rewriting and garbage collection further improve this performance. Since the implementation can probably be even further optimised, and because in any case GPUs will become much more powerful in the future, this suggests that GPUs are an interesting platform for (many-sorted) term rewriting. As term rewriting can be viewed as a universal programming language, this also opens a route towards programming GPUs by term rewriting, especially for irregular computations.

Abstract We present the first parallel algorithms that decide strong and branching bisimilarity in linear time. More precisely, if a transition system has n states, m transitions and $$\vert Act \vert $$ | A c t | action labels, we introduce an algorithm that decides strong bisimilarity in $$\mathcal {O}(n+\vert Act \vert )$$ O ( n + | A c t | ) time on $$\max (n,m)$$ max ( n , m ) processors and an algorithm that decides branching bisimilarity in $$\mathcal {O}(n+\vert Act \vert )$$ O ( n + | A c t | ) time using up to $$\max (n^2,m,\vert Act \vert n)$$ max ( n 2 , m , | A c t | n ) processors.

Abstract GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone. This paper introduces Alpinist, an annotation-aware GPU program optimizer. It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. We evaluate Alpinist, in combination with the VerCors program verifier, to automatically optimize a collection of verified programs and reverify them.

Abstract The effective parallelisation of Bounded Model Checking is challenging, due to SAT and SMT solving being hard to parallelise. We present ParaFROST, which is the first tool to employ a graphics processor to accelerate BMC, in particular the simplification of SAT formulas before and repeatedly during the solving, known as pre- and inprocessing. The solving itself is performed by a single CPU thread. We explain the design of the tool, the data structures, and the memory management, the latter having been particularly designed to handle SAT formulas typically generated for BMC, i.e., that are large, with many redundant variables. Furthermore, the solver can make multiple decisions simultaneously. We discuss experimental results, having applied ParaFROST on programs from the Core C99 package of Amazon Web Services.

Abstract Since 2013, the leading SAT solvers in the SAT competition all use inprocessing, which unlike preprocessing, interleaves search with simplifications. However, applying inprocessing frequently can still be a bottle neck, i.e., for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As memory is a scarce resource in GPUs, we present new space-efficient data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improves memory access locality. Our new parallel variable elimination algorithm is twice as fast as previous work. In experiments our new solver ParaFROST solves many benchmarks faster on the GPU than its sequential counterparts.

Techniques are required that support developers to produce GPU software that is both functionally correct and high-performing. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years.

Most modern and successful SAT solvers are based on the Conflict-Driven Clause-Learning (CDCL) algorithm. The CDCL approach is to try to learn from previous assignments, and based on this, prune the search space to make better decisions in the future. In the current paper, we propose the introduction of a multiple decision maker (MDM) into CDCL. Adhering to a number of rules, MDM constructs sets of decisions to be made at once. Experiments show MDM has a considerably positive impact on CDCL, for many different SAT application problems. Overall, about 50% of the benchmarks we considered were solved faster when MDM was enabled, and the total processing time of all benchmarks was reduced by 6%. Moreover, MDM allowed 31 extra problems to be solved. We introduce MDM, analyse its impact, and try to understand the cause of that impact.

Abstract Branching bisimilarity is a behavioural equivalence relation on labelled transition systems (LTSs) that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than ones for other weak behavioural equivalences, especially weak bisimilarity. With m the number of transitions and n the number of states, the classic $${O\left( {m n}\right) }$$ algorithm was recently replaced by an $$O({m (\log \left| { Act }\right| + \log n)})$$ algorithm [9], which is unfortunately rather complex. This paper combines its ideas with the ideas from Valmari [20], resulting in a simpler $$O({m \log n})$$ algorithm. Benchmarks show that in practice this algorithm is also faster and often far more memory efficient than its predecessors, making it the best option for branching bisimulation minimisation and preprocessing for calculating other weak equivalences on LTSs.

Reasoning about the correctness of parallel and distributed systems requires automated tools. By now, the mCRL2 toolset and language have been developed over a course of more than fifteen years. In this paper, we report on the progress and advancements over the past six years. Firstly, the mCRL2 language has been extended to support the modelling of probabilistic behaviour. Furthermore, the usability has been improved with the addition of refinement checking, counterexample generation and a user-friendly GUI. Finally, several performance improvements have been made in the treatment of behavioural equivalences. Besides the changes to the toolset itself, we cover recent applications of mCRL2 in software product line engineering and the use of domain specific languages (DSLs).

The growing scale of applications encoded to Boolean Satisfiability (SAT) problems imposes the need for accelerating SAT simplifications or preprocessing. Parallel SAT preprocessing has been an open challenge for many years. Therefore, we propose novel parallel algorithms for variable and subsumption elimination targeting Graphics Processing Units (GPUs). Benchmarks show that the algorithms achieve an acceleration of 66 $$\times $$ over a state-of-the-art SAT simplifier (SatELite). Regarding SAT solving, we have conducted a thorough evaluation, combining both our GPU algorithms and SatELite with MiniSat to solve the simplified problems. In addition, we have studied the impact of the algorithms on the solvability of problems with Lingeling. We conclude that our algorithms have a considerable impact on the solvability of SAT problems.

Abstract In Model Driven Software Engineering, models and model transformations are the primary artifacts when developing a software system. In such a workflow, model transformations are used to incrementally transform initial abstract models into concrete models containing all relevant system details. Over the years, various formal methods have been proposed and further developed to determine the functional correctness of models of concurrent systems. However, the formal verification of model transformations has so far not received as much attention. In this article, we propose a formal verification technique to determine that formalisations of such transformations in the form of rule systems are guaranteed to preserve functional properties, regardless of the models they are applied on. This work extends our earlier work in various ways. Compared to our earlier approaches, the current technique involves only up to n individual checks, with n the number of rules in the rule system, whereas previously, up to 2 n − 1 checks were required. Furthermore, a full correctness proof for the technique is presented, based on a formal proof conducted with the Coq proof assistant. Finally, we report on two sets of conducted experiments. In the first set, we compared traditional model checking with transformation verification, and in the second set, we compared the verification technique presented in this article with the previous version.

Model checking (Baier and Katoen in Principles of model checking, MIT Press, Cambridge, 2008; Clarke et al. in Model checking, MIT Press, Cambridge, 2001) is an automatic technique to formally verify that a given specification of a concurrent system meets given functional properties. Its use has been demonstrated many times over the years. Key characteristics that make the method so appealing are its level of automaticity, its ability to determine the absence of errors in the system (contrary to testing techniques) and the fact that it produces counter-examples when errors are detected, that clearly demonstrate not only that an error is present, but also how the error can be produced. The main drawback of model checking is its limited scalability, and for this reason, research on reducing the computational effort has received much attention over the last decades. Besides the verification of qualitative functional properties, the model checking technique can also be applied for other types of analyses, such as planning and the verification of quantitative properties. We briefly discuss several contributions in the model checking field that address both its scalability and its applicability to perform planning and quantitative analysis. In particular, we introduce six papers selected from the 23rd International SPIN Symposium on Model Checking Software (SPIN 2016).

We provide a new algorithm to determine stuttering equivalence with time complexity O ( m log n ), where n is the number of states and m is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimulation in O ( m (log | Act | + log n )) time, where Act is the set of actions in a labeled transition system. Theoretically, our algorithm substantially improves upon existing algorithms, which all have time complexity of the form O ( mn ) at best. Moreover, it has better or equal space complexity. Practical results confirm these findings: they show that our algorithm can outperform existing algorithms by several orders of magnitude, especially when the Kripke structures are large. The importance of our algorithm stretches far beyond stuttering equivalence and branching bisimulation. The known O ( mn ) algorithms were already far more efficient (both in space and time) than most other algorithms to determine behavioral equivalences (including weak bisimulation), and therefore they were often used as an essential preprocessing step. This new algorithm makes this use of stuttering equivalence and branching bisimulation even more attractive.

A challenging aspect of model-to-code transformations is to ensure that the semantic behavior of the input model is preserved in the output code. When constructing concurrent systems, this is mainly difficult due to the non-deterministic potential interaction between threads. In this paper, we consider this issue for a framework that implements a transformation chain from models expressed in the state machine based domain specific language SLCO to Java. In particular, we provide a fine-grained generic solution to preserve atomicity of SLCO statements in the Java implementation. We give its generic specification based on separation logic and verify it using the verification tool VeriFast. The solution can be regarded as a reusable module to safely implement atomic operations in concurrent systems.

This article presents parallel algorithms for component decomposition of graph structures on general purpose graphics processing units (GPUs). In particular, we consider the problem of decomposing sparse graphs into strongly connected components, and decomposing graphs induced by stochastic games (such as Markov decision processes) into maximal end components. These problems are key ingredients of many (probabilistic) model-checking algorithms. We explain the main rationales behind our GPU-algorithms, and show a significant speed-up over the sequential (as well as existing parallel) counterparts in several case studies.

Model checking is an automatic method to formally verify the correctness of a system specification. Such model checking specifications can be viewed as implicit descriptions of a large directed graph or state space, which, for most model checking operations, needs to be analysed. However, construction or on-the-fly exploration of the state space is computationally intensive and often can be prohibitive in practical applications. In this work, we present techniques to perform graph generation and exploration using general purpose graphics processors (GPUs). GPUs have been successfully applied in multiple application domains to drastically speed up computations. We explain the limitations involved when trying to achieve efficient state space exploration with GPUs and present solutions how to overcome these. We discuss the possible approaches involving related work and propose an alternative, using a new hash table approach for GPUs. As input, we consider models that can be represented by a fixed number of communicating finite-state Labelled Transition Systems. This means that we assume that all variables used in a model range over finite data domains. Additionally, we show how our exploration technique can be extended to detect deadlocks and check safety properties on-the-fly. Experimental evaluations with our prototype implementations show significant speed-ups compared to the established sequential counterparts.

BACKGROUND: Techniques for reconstruction of biological networks which are based on perturbation experiments often predict direct interactions between nodes that do not exist. Transitive reduction removes such relations if they can be explained by an indirect path of influences. The existing algorithms for transitive reduction are sequential and might suffer from too long run times for large networks. They also exhibit the anomaly that some existing direct interactions are also removed. RESULTS: We develop efficient scalable parallel algorithms for transitive reduction on general purpose graphics processing units for both standard (unweighted) and weighted graphs. Edge weights are regarded as uncertainties of interactions. A direct interaction is removed only if there exists an indirect interaction path between the same nodes which is strictly more certain than the direct one. This is a refinement of the removal condition for the unweighted graphs and avoids to a great extent the erroneous elimination of direct edges. CONCLUSIONS: Parallel implementations of these algorithms can achieve speed-ups of two orders of magnitude compared to their sequential counterparts. Our experiments show that: i) taking into account the edge weights improves the reconstruction quality compared to the unweighted case; ii) it is advantageous not to distinguish between positive and negative interactions since this lowers the complexity of the algorithms from NP-complete to polynomial without loss of quality.

For many systems, timing aspects are essential. Therefore, when modelling these systems, time should somehow be represented. In the past, many timed process algebras have been developed, using untimed process algebras as initial inspiration. In this paper, we take another approach, considering the possibility to model timing aspects with an untimed process algebra. The advantage is that the algebra itself does not need to be extended, and the available tools can be reused. In contrast to other work, where this approach has been looked at, we focus on ease of modelling, and single delay steps of varying sizes. We present the timing mechanism used, our approach, and some examples.

In this paper, we show how scheduling problems can be modelled in untimed process algebra, by using special tick-actions. As a result, we can use efficient, distributed state space generators to solve scheduling problems. Also, we can use more flexible data specifications than timed model checkers usually provide. We propose a variant on breadth-first search, which visits the states per time slice between ticks. We applied our approach to find optimal schedules for test batches of a realistic clinical chemical analyser, which performs several kinds of tests on patient samples.

In this paper the authors first gave short overviews of the modelling languages timed chi( chit) and muCRL. Then a general translation scheme was presented to translate chitspecifications to muCRL specifications. As chittargets performance analysis and muCRL targets functional analysis of systems, this translation scheme provides a way to perform both kinds of analysis on a given chitsystem model. Finally, an example of a chitsystem was given and shown how the translation works on a concrete case study