1. Introduction
In addition to the traditional testing techniques that have been in use for decades, model checking [
1] is one promising approach for increasing the reliability of software and hardware systems. By checking the entire reachable state spaces of the systems, model checking can systematically verify that finite-state systems satisfy some desired properties. The state space explosion, on the other hand, is well-known to be the most difficult problem in model checking due to the fact that the number of states in a system under the verification’s reachable state space often increases exponentially. Although numerous techniques have been suggested to improve the situation, the issue still needs to be resolved. These include abstraction [
2,
3,
4] and partial order reduction [
5]. Aside from that, there is a running performance issue for model checking because a lot of time is often spent performing model checking experiments when the reachable state space is huge. One of the main approaches to cope with the running performance issue is to parallelize model checking to take advantage of multicore architectures.
Our research team devised a divide-and-conquer approach to model checking some specific properties such as conditional stable properties [
6], leads-to properties [
7], eventual properties [
8], and until stable properties [
9] in order to cope with the state space explosion problem in model checking. We can formalize those properties in linear temporal logic (LTL); however, we need to handle each property separately because it is challenging to find a single technique in order to cope with four different properties at once to reduce the problem. The core principle of our approach is to split the original model checking problem for each property into multiple smaller model checking problems and work on each smaller one. Suppose that the sub-state space’s size for each smaller problem is substantially smaller compared to the reachable state space’s size for the original model checking problem. In this situation, our approach can somewhat reduce the state space explosion problem for each property to a certain extent. Then, for each of the conditional stable properties [
10], leads-to properties [
11], and eventual properties [
12], our research team constructed a sequential tool. Due to the nature of the divide-and-conquer approach, each smaller model checking problem can essentially be tackled independently. Therefore, our research team has proposed parallel techniques/tools for conditional stable properties [
10] and leads-to properties [
13]. In this present paper, we concentrate on parallelizing model checking for eventual properties to benefit from multicore architecture in order to enhance the running performance for model checking eventual properties, in addition to easing the state space explosion as demonstrated in [
12].
Informally, eventual properties indicate that something will eventually occur. This paper only copes with the eventual properties expressed in LTL as
, where
is restricted to a state proposition. The properties can be used to define a number of significant software needs, including termination or halting, which is an essential software requirement that numerous systems should meet. We devised a divide-and-conquer approach to eventual model checking (referred to as DCA2EMC from now on) [
8] that intends to reduce the state space explosion and constructed a sequential tool [
12] in support of the approach. Some experiments have been carried out that show that our approach is a promising solution to reduce the state space explosion problem for eventual model checking. Due to the nature of the divide-and-conquer approach of DCA2EMC, we would like to leverage parallelization to address the ongoing performance issue in model checking for eventual properties. This paper is an extended version of our conference paper [
12], where we propose a technique to parallelize model checking for eventual properties and construct a support tool. The effectiveness of our proposed technique/tool is demonstrated by carrying out some experiments.
The sequential tool [
12] has been developed in Maude [
14], as has the parallel tool. Maude is a high-performance specification/programming language relying on rewriting logic [
15]. Many parallel applications have been developed using Maude, including parallel tools for model checking conditional stable properties [
10] and leads-to properties [
13] based on a divide-and-conquer approach, and the parallelization of Maude-NPA for analyzing cryptographic protocols [
16]. SPIN [
17] is a well-known model checker widely used in academia and industry. From the perspective of running performance and memory usage, Maude and SPIN are comparable [
18]. Therefore, it is worth considering Maude in this work. Moreover, Maude supports reflective programming (or meta-programming), making it easier to extend Maude facilities and use Maude as a handy software component in our implementation. Therefore, we employ Maude to develop the parallel tool rather than another programming language. The case studies and the parallel tool utilized in our experiments are both found at
https://github.com/yatiphyo/DCA2MC (accessed on 29 May 2023).
The remainder of the present paper is organized as follows.
Section 2 mentions some preliminaries.
Section 3 describes the algorithm for DCA2EMC.
Section 4 describes the parallelization of DCA2EMC.
Section 5 reports our experimental results.
Section 6 mentions some existing work. Finally,
Section 7 concludes the paper with some avenues for future work.
2. Preliminaries
A Kripke structure is a tuple of five elements as follows: (1) a set of states denoted by , (2) a set of initial states denoted by such that , (3) a left-total binary relation over states denoted by , (4) a set of atomic propositions denoted by , and (5) a labeling function from to denoted by . denotes a set of atomic propositions that are true in s for each . Each may be thought of as a state transition, which may be expressed as either or if is clear from the context. is called an infinite sequence of states or a path (referred to as ) if is a state transition for each . The following notations for paths are used:
,
,
,
where is a postfix of from the ith state in ; is a prefix of , where the ith state of is repeated forever in the prefix; and is the ith state in , where denotes the first state (or the 0th state) in . If , we refer to a path as a computation. and are used to represent sets of all paths and computations, respectively. By definition, we have . The collection of distinct paths that begin with is denoted by . Given a natural number b, is the collection of paths such that . We employ to indicate .
Assuming that
p is an atomic proposition, we define the syntax of an LTL formula
in the following manner:
The set of all LTL formulas is denoted by
. Inductively, we can define
as follows for
and
:
;
iff ;
iff ;
iff and/or ;
if and only if ;
if and only if there exists a natural number i such that and for all natural numbers , .
Here, the LTL formulas and are used. Then, we have iff for all computations of . The next temporal connective and the until temporal connective are defined as ◯ and , respectively.
We use some other logical and temporal connectives defined as follows:
□ is the always temporal connective, while ⋄ is the eventual temporal connective. State propositions do not include any temporal connectives as propositional formulas in propositional logic, and then the first state can determine whether a path satisfies a state proposition. In this present paper, the properties in the form of are called eventual properties, where is restricted to a state proposition.
In this present paper, if a collection’s non-empty constructor is both associative and commutative (AC), it is referred to as a soup. An observable component is a pair of names and values (e.g.,
indicating that process
p is resided at
or the waiting section). States are characterized by using some observable components. Formally, a state is specified as a braced soup of observable components. For example, if three observable components
are used to characterize a state for a particular purpose,
is the formalization of a state, where the juxtaposition operator (or the empty syntax) is utilized as the non-empty constructor of soups. Because the order does not matter in AC collections,
is equivalent to other permutations of
, such as
. Rewrite rules can be used to describe state transitions. In particular, we formalize systems and protocols as Kripke structures in Maude [
14] and then we use a built-in LTL model checker in Maude for conducting model checking experiments.
3. A Divide-and-Conquer Approach to Eventual Model Checking
Given a Kripke structure
and an eventual property, DCA2EMC divides the original reachable state space that starts from each
into
layers as shown in
Figure 1 for model checking the eventual property in a layered way. We call intermediate layers those from 0 to
L, while we call the final layer
. Let
be a positive natural number to indicate the depth of each layer
l for
,
be 0, and
be
∞. A sequence
is referred to as a layer configuration used for DCA2EMC. Let
be
indicating the true depth of layer
l from each initial state in
for
,
be 0, and
be
∞. States residing at depth
or the bottom of layer
l are utilized as the beginning states (or initial states) of layer
in DCA2EMC. If there are
states residing at the bottom of layer
l, then layer
has
sub-state spaces for each
. Note that for each state, its sub-state space is the reachable state space that starts from the state with a bounded depth, and an unbounded depth is used for the final layer. In this manner, we split the reachable state space from
into multiple smaller sub-state spaces. We carry out model checking experiments with a Kripke structure
for sub-state spaces residing in each intermediate layer
l.
is constructed from
by removing all state transitions that come out from the states residing at the bottom of layer
l and adding a self-transition to each state. Because the final layer’s depth is
∞, we simply carry out model checking experiments with
for sub-state spaces residing in the final layer.
We can check , where is restricted to state propositions in a layered way, as presented in Algorithm 1. For each intermediate layer , DCA2EMC needs to collect all counterexample (or cx for short) states that do not satisfy . Let and be two sets of states used to collect all cx states at each intermediate layer. Our procedure is as follows:
, is initially in the code snippet at line 1, consisting of all initial states, and is regarded as cx states in our initialization.
For each , we first check if is empty in the code snippet at lines 3–5. If so, is returned; otherwise, we keep going as follows. is then set to an empty set in the code snippet at line 6. Model checking an eventual property for the sub-state space that starts from each state in with is conducted. If a cx is found, we add the last state of the cx, which must have a self-transition because of , to in the code snippet at lines 7–13. In the end, all cx states for layer l are stored in and assigned to in the code snippet at line 14.
Note that all states in or are called cx states in this paper.
For the final layer , DCA2EMC needs to be carried out as follows:
Model checking an eventual property for the sub-state space that starts from each state in with is conducted. If a cx is found, it returns in the code snippet at lines 16–22. In other words, a cx of the original model checking problem is found.
If no cx was found in the end, is returned in the code snippet at line 23.
To guarantee the correctness of the algorithm for DCA2EMC, we have proved a theorem in [
8]. As shown in Algorithm 1, it just returns
Failure when
, but with a small modification as described in [
8], we can construct and return a cx. Both the sequential version of DCA2EMC in [
12] and the parallelization of DCA2EMC in this present paper are capable of showing a
cx when
. For a comprehensive understanding of how DCA2EMC operates using a simple example, readers can check Sect. IV in [
8] for more detailed information.
Algorithm 1: A divide-and-conquer approach to eventual model checking in a layered way. |
|
4. A Parallel Version of DCA2EMC
As shown in Algorithm 1, finding counterexample states in each sub-state space at each intermediate layer of DCA2EMC can essentially be conducted independently; however, the overhead to parallelize this part may be higher than the benefit that can be obtained from parallelization, as demonstrated in [
19]. Meanwhile, the model checking problem for each sub-state space residing in the final layer of DCA2EMC can be essentially conducted independently. Therefore, this section describes how to build a parallelization of DCA2EMC relying on a master–worker pattern, where we only conduct the model checking experiments at the final layer in parallel, while collecting all counterexample states residing at the bottom of each intermediate layer up to layer
L, which proceeds in a serial way. Object-oriented systems, in which objects communicate with one another through Maude Sockets, are supported by Maude. Hence, we use these facilities in Maude to develop the parallel tool.
The parallel tool is constructed using a master–worker pattern, where one master and many workers participate. The master is responsible for constructing jobs, distributing jobs to workers, and terminating the parallel tool whenever either a
cx is found by a worker at the final layer or workers have performed all jobs. The master and the workers communicate using three different types of messages:
,
, and
. A
message is constructed from a state
residing at the bottom of layer
L and a log list of the state, which is a list
of pairs of states and natural numbers. The log list is used to track the path that starts from the initial state to the current state to build the
cx of the original model checking problem if applicable. Only the master is the person sending a
message to a worker.
and
messages are literal strings sent from workers to the master. Each worker is responsible for carrying out a model checking experiment with the eventual property concerned from the state encapsulated in each job that the master assigns to the worker. If no
cx is found, the worker asks the master for a new job by sending a
message. Otherwise, the worker finds a
cx and then it sends a
message for terminating the parallel tool and constructs a full
cx for the original model checking problem based on the log list encapsulated in the job and the
cx found in the model checking experiment at the final layer. The reader can refer to [
12] on how to construct the full
cx for more details.
Algorithm 2 presents the pseudocode for assigning jobs carried out by the master. The master maintains two queues: one for jobs (referred to as
) and the other for worker identifiers (referred to as
) to allocate jobs to workers in an equitable manner. Initially, the master is responsible for generating all
cx states residing at the bottom of each intermediate layer up to layer
L using the
function in the code snippet at line 1 with the initial state
and the layer configuration
as its parameters. Because this step is conducted in a serial way, we build the function based on how we generate
cx states for each intermediate layer implemented in the sequential tool [
12]. Recall that each job in
is constructed from a state residing at the bottom of layer
L and a log list of the state. The master then carries out the above-described duties. In the code snippet at lines 3–11, the master checks if there is any message from the workers. If that is the case, the master checks whether the message is either a
message or a
message. If it is the former, the worker identifier is added to the
queue; otherwise, the master disconnects all workers and returns
. In the code snippet at lines 12–16, the master checks if neither
nor
is empty. If so, the master delivers a job to a worker. In the code snippet at lines 17–20, the master verifies whether workers have completed all jobs in
. If so, the master disconnects all workers and returns
.
Algorithm 3 shows the pseudocode for handling jobs operated by each worker. On the first line of the code snippet, the workers send a very first
message to the master to ask for a job. The code snippet at lines 2–11 shows what the worker is supposed to do as described above. When the worker is open, it needs to do as follows. The worker receives a
message in the form of a state and its log list from the master in the code snippet at line 3. The worker then carries out its above-described duties in the code snippet at lines 4–10. If a
cx is found, a full
cx is constructed and returned; otherwise, the worker asks the master for a new job by sending a
message. The worker is not open only when the master disconnects all workers. If so, the worker is subsequently terminated.
Algorithm 2: The master delivers jobs to workers |
|
Algorithm 3:Workers process jobs |
|
6. Related Work
SAT/SMT-based bounded model checking (or SAT/SMT-BMC for short) [
25] is an extremely successful method for dealing with the state space explosion in model checking. It can find a counterexample at the position close to an initial state, but proving that a system has the desired properties is impossible. To address this limitation,
k-induction [
26,
27], an extension of SAT/SMT-BMC, has been proposed in which the technique uses a combination of mathematical induction and SAT/SMT-BMC in order to show the satisfaction of a system with its required properties. An SAT/SMT solver is used to verify the desired properties up to a certain depth (or a bounded depth) from an arbitrary initial state, and this step is regarded as the base case. For each state sequence up to the bounded depth, all successor states from the last state of the state sequence are verified with the desired properties using an SAT/SMT solver, and this step is regarded as the induction step. Our technique [
6] shares the basic idea with SAT/SMT-BMC when we conduct bounded model checking experiments for sub-state spaces residing at each intermediate layer. DCA2EMC can also be regarded as an extension of BMC because we conduct unbounded model checking for sub-state spaces residing in the final layer in order to prove the desired properties, but no SAT/SMT solvers are used.
Barnat et al. [
28] have surveyed recent developments in parallel algorithms for LTL model checking. To optimize the use of multi-core architectures, we are required to modify graph search algorithms. DiVinE 3.0 [
29] and a multi-core extension of SPIN [
30] are two parallel model checkers that use these algorithms. In contrast, we can employ any existing LTL model checker to implement a parallelization of DCA2EMC, without the need to modify graph search algorithms. This is a key distinction from any parallel LTL model checker currently available.
Inverso et al. [
31] expanded the use of SAT/SMT-based BMC to verify concurrent programs. They used an unwinding (or unfolding) bound, denoted by
u, and a round-robin schedule, denoted by
r. The first step is to transform a concurrent program
P into an intermediate program
, where they unfold all loops and inline function calls with
u as a bound, while those used for creating threads are disregarded. The second step is to convert
into a sequential program
by enumerating all behaviors of
in
r round-robin schedules. The third step is to encode
into a propositional formula, which can be checked with a SAT/SMT solver. To parallelize the analysis of such a propositional formula, it can be split into multiple sub-formulas, assigned to multiple instances running a SAT/SMT solver, and handled in parallel [
32]. It seems that their approach can only cope with safety properties, while our approach can cope with eventual properties, which is a category of liveness properties.
A distributed-memory version of SPIN has been presented by Lerda and Sisto [
33]. Their proposed approach is similar to ours as it addresses the problem of formal specifications for systems under verification becoming too large to fit into a computer’s physical memory. This leads to a significant decrease in performance and in the worst case it is even impossible to conduct model checking experiments. To solve this issue, for a large-state system, they split the whole reachable state space into smaller sub-state spaces and assign them to multiple nodes or computers connected through the network. The advantage of their approach is the ability to integrate some existing optimization techniques from SPIN, such as bit state hashing and partial order reduction, into their approach. Some case studies have been conducted, showing the efficiency of their proposed approach. However, the distributed-memory version of SPIN can only cope with safety properties, while our parallelization of DCA2EMC can cope with eventual properties, which is a category of liveness properties.
When verifying huge systems, using an exhaustive search with SPIN is impossible. It then provides a bit-state verification mode, which conducts a non-exhaustive search on the whole reachable state space to tackle such huge systems. However, the likelihood that the SPIN bit-state verification mode will miss system defects increases with the size of the system under verification. To address this limitation, Swarm Verification [
34] has been introduced. In this technique, parallelism and the diversity of search strategies are two main principles. One instance of bit-state verification is carried out for each search strategy. These instances can be run simultaneously and are essentially independent. By using various search strategies, we may explore different regions of the reachable state space, increasing the likelihood of flaw detection, as well as improving coverage. Grapple [
35], a GPU-based Swarm Verification implementation, has also been proposed since then. In our approach, the reachable state space from each initial state is split into multiple layers, generating multiple sub-state spaces, and each sub-state space is checked exhaustively with the Maude LTL model checker. It would be beneficial to employ the Swarm Verification idea in conjunction with our technique so that it can use the Swarm Verification for each sub-state space rather than an exhaustive search to potentially uncover flaws in huge systems more quickly.
Author Contributions
Conceptualization, K.O.; methodology, Y.P. and C.M.D.; software, Y.P. and C.M.D.; validation, Y.P. and M.N.A.; formal analysis, Y.P. and M.N.A.; investigation, Y.P. and M.N.A.; resources, Y.P. and M.N.A.; data curation, Y.P. and C.M.D.; writing—original draft preparation, Y.P.; writing—review and editing, Y.P., M.N.A., C.M.D. and K.O.; visualization, Y.P. and M.N.A.; supervision, K.O.; project administration, K.O.; funding acquisition, K.O. All authors have read and agreed to the published version of the manuscript.
Funding
This work was partially supported by JSPS KAKENHI, Grant Number JP19H04082.
Data Availability Statement
Conflicts of Interest
The authors declare no conflict of interest.
References
- Clarke, E.M.; Henzinger, T.A.; Veith, H.; Bloem, R. (Eds.) Handbook of Model Checking; Springer: Berlin/Heidelberg, Germany, 2018. [Google Scholar] [CrossRef]
- Clarke, E.M.; Grumberg, O.; Long, D.E. Model Checking and Abstraction. ACM Trans. Program. Lang. Syst. 1994, 16, 1512–1542. [Google Scholar] [CrossRef]
- Clarke, E.M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 2003, 50, 752–794. [Google Scholar] [CrossRef] [Green Version]
- Meseguer, J.; Palomino, M.; Martí-Oliet, N. Equational abstractions. Theor. Comput. Sci. 2008, 403, 239–264. [Google Scholar] [CrossRef] [Green Version]
- Clarke, E.M.; Grumberg, O.; Minea, M.; Peled, D.A. State Space Reduction Using Partial Order Techniques. Int. J. Softw. Tools Technol. Transf. 1999, 2, 279–287. [Google Scholar] [CrossRef] [Green Version]
- Phyo, Y.; Do, C.M.; Ogata, K. A Divide & Conquer Approach to Conditional Stable Model Checking. In Proceedings of the Theoretical Aspects of Computing–ICTAC 2021: 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, 8–10 September 2021; Proceedings 18; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 2021; Volume 12819, pp. 105–111. [Google Scholar] [CrossRef]
- Phyo, Y.; Do, C.M.; Ogata, K. A Divide & Conquer Approach to Leads-to Model Checking. Comput. J. 2021, 65, 1353–1364. [Google Scholar] [CrossRef]
- Aung, M.N.; Phyo, Y.; Do, C.M.; Ogata, K. A Divide and Conquer Approach to Eventual Model Checking. Mathematics 2021, 9, 368. [Google Scholar] [CrossRef]
- Do, C.M.; Phyo, Y.; Ogata, K. A Divide & Conquer Approach to Until and Until Stable Model Checking. In Proceedings of the 34th International Conference on Software Engineering & Knowledge Engineering, SEKE 2022, Pittsburgh, PA, USA, 1–10 July 2022. [Google Scholar] [CrossRef]
- Do, C.M.; Phyo, Y.; Ogata, K. Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way. IEEE Access 2022, 10, 133749–133765. [Google Scholar] [CrossRef]
- Phyo, Y.; Do, C.M.; Ogata, K. A support tool for the L + 1-layer divide & conquer approach to leads-to model checking. In Proceedings of the COMPSAC, Munich, Germany, 18–22 July 2011; pp. 854–863. [Google Scholar] [CrossRef]
- Aung, M.N.; Phyo, Y.; Do, C.M.; Ogata, K. A Tool for Model Checking Eventual Model Checking in a Stratified Way. In Proceedings of the 2022 9th International Conference on Dependable Systems and Their Applications (DSA), Wulumuqi, China, 4–5 August 2022; pp. 270–279. [Google Scholar] [CrossRef]
- Do, C.M.; Phyo, Y.; Riesco, A.; Ogata, K. A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties. In Proceedings of the 2021 7th International Symposium on System and Software Reliability (ISSSR), Chongqing, China, 23–24 September 2021; pp. 155–166. [Google Scholar] [CrossRef]
- Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C.L. (Eds.) All About Maude—A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 2007; Volume 4350. [Google Scholar] [CrossRef]
- Meseguer, J. Twenty years of rewriting logic. J. Log. Algebr. Methods Program. 2012, 81, 721–781. [Google Scholar] [CrossRef] [Green Version]
- Minh Do, C.; Riesco, A.; Escobar, S.; Ogata, K. Parallel Maude-NPA for Cryptographic Protocol Analysis. In Proceedings of the Rewriting Logic and Its Applications—14th International Workshop, Munich, Germany, 2–3 April 2022; pp. 253–273. [Google Scholar] [CrossRef]
- Holzmann, G. The model checker SPIN. IEEE Trans. Softw. Eng. 1997, 23, 279–295. [Google Scholar] [CrossRef] [Green Version]
- Eker, S.; Meseguer, J.; Sridharanarayanan, A. The Maude LTL Model Checker. Electron. Notes Theor. Comput. Sci. 2002, 71, 162–187. [Google Scholar] [CrossRef] [Green Version]
- Do, C.M.; Phyo, Y.; Riesco, A.; Ogata, K. Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way. ACM Trans. Softw. Eng. Methodol. 2023. just accepted. [Google Scholar] [CrossRef]
- Eker, S.; Meseguer, J.; Sridharanarayanan, A. The Maude LTL Model Checker and Its Implementation. In Proceedings of the SPIN; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 2003; Volume 2648, pp. 230–234. [Google Scholar] [CrossRef] [Green Version]
- Aung, M.; Phyo, Y.; Ogata, K. Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). In Proceedings of the SEKE, Lisbon, Portugal, 10–12 July 2019; pp. 159–164. [Google Scholar] [CrossRef]
- Anderson, T.E. The Performance of Spin Lock Alternatives for Shared-Memory Multiprocessors. IEEE Trans. Parallel Distributed Syst. 1990, 1, 6–16. [Google Scholar] [CrossRef] [Green Version]
- Mellor-Crummey, J.M.; Scott, M.L. Algorithms for Scalable Synchronization on Shared-Memory Multiprocessors. ACM Trans. Comput. Syst. 1991, 9, 21–65. [Google Scholar] [CrossRef] [Green Version]
- Clarke, E.M.; Emerson, E.A.; Jha, S.; Sistla, A.P. Symmetry Reductions in Model Checking. In Proceedings of the 10th International Conference on Computer Aided Verification, Vancouver, BC, Canada, June/July 1998; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 1998; Volume 1427, pp. 147–158. [Google Scholar] [CrossRef] [Green Version]
- Clarke, E.M.; Biere, A.; Raimi, R.; Zhu, Y. Bounded Model Checking Using Satisfiability Solving. Form. Methods Syst. Des. 2001, 19, 7–34. [Google Scholar] [CrossRef]
- Sheeran, M.; Singh, S.; Stålmarck, G. Checking Safety Properties Using Induction and a SAT-Solver. In Proceedings of the 3rd FMCAD, Austin, TX, USA, 1–3 November 2000; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 2000; Volume 1954, pp. 108–125. [Google Scholar] [CrossRef]
- de Moura, L.M.; Rueß, H.; Sorea, M. Bounded Model Checking and Induction: From Refutation to Verification. In 15th International Conference on Computer Aided Verification; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 2003; Volume 2725, pp. 14–26. [Google Scholar] [CrossRef] [Green Version]
- Barnat, J.; Bloemen, V.; Duret-Lutz, A.; Laarman, A.; Petrucci, L.; van de Pol, J.; Renault, E. Parallel Model Checking Algorithms for Linear-Time Temporal Logic. In Handbook of Parallel Constraint Reasoning; Springer: Berlin/Heidelberg, Germany, 2018; pp. 457–507. [Google Scholar] [CrossRef]
- Barnat, J.; Brim, L.; Havel, V.; Havlícek, J.; Kriho, J.; Lenco, M.; Rockai, P.; Still, V.; Weiser, J. DiVinE 3.0—An Explicit-State Model Checker for Multithreaded C & C++ Programs. In Proceedings of the CAV 2013, Saint Petersburg, Russia, 13–19 July 2013; Springer: Berlin/Heidelberg, Germany, 2013; Volume 8044, LNCS. pp. 863–868. [Google Scholar] [CrossRef]
- Holzmann, G.J.; Bosnacki, D. The Design of a Multicore Extension of the SPIN Model Checker. IEEE Trans. Softw. Eng. 2007, 33, 659–674. [Google Scholar] [CrossRef] [Green Version]
- Inverso, O.; Tomasco, E.; Fischer, B.; Torre, S.L.; Parlato, G. Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. In Proceedings of the Computer Aided Verification–26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 18–22 July 2014; Proceedings; Lecture Notes in Computer Science; Biere, A., Bloem, R., Eds.; Springer: Berlin/Heidelberg, Germany, 2014; Volume 8559, pp. 585–602. [Google Scholar] [CrossRef] [Green Version]
- Inverso, O.; Trubiani, C. Parallel and distributed bounded model checking of multi-threaded programs. In Proceedings of the PPoPP ’20: 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, San Diego, CA, USA, 22–26 February 2020; Gupta, R., Shen, X., Eds.; ACM: New York, NY, USA, 2020; pp. 202–216. [Google Scholar] [CrossRef] [Green Version]
- Lerda, F.; Sisto, R. Distributed-Memory Model Checking with SPIN. In Proceedings of the 5th and 6th SPIN Workshops, Trento, Italy, 5 July 1999; Lecture Notes in Computer Science; Springer: Berlin/Heidelberg, Germany, 1999; Volume 1680, pp. 22–39. [Google Scholar] [CrossRef] [Green Version]
- Holzmann, G.J.; Joshi, R.; Groce, A. Swarm Verification Techniques. IEEE Trans. Softw. Eng. 2011, 37, 845–857. [Google Scholar] [CrossRef] [Green Version]
- DeFrancisco, R.; Cho, S.; Ferdman, M.; Smolka, S.A. Swarm model checking on the GPU. Int. J. Softw. Tools Technol. Transf. 2020, 22, 583–599. [Google Scholar] [CrossRef]
| Disclaimer/Publisher’s Note: The statements, opinions and data contained in all publications are solely those of the individual author(s) and contributor(s) and not of MDPI and/or the editor(s). MDPI and/or the editor(s) disclaim responsibility for any injury to people or property resulting from any ideas, methods, instructions or products referred to in the content. |
© 2023 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (https://creativecommons.org/licenses/by/4.0/).