Distributed CTL Model Checking in the Cloud
Carlo Bellettini, Matteo Camilli, Lorenzo Capra, Mattia Monga

TL;DR
This paper presents a distributed method leveraging cloud computing to perform CTL model checking on large state spaces, demonstrating improved scalability and efficiency through benchmark testing.
Contribution
It introduces a novel distributed approach for CTL model checking that utilizes big data techniques and cloud resources, enabling verification of very large systems.
Findings
Effective verification of large state spaces using distributed systems.
Benchmark results show improved performance and scalability.
Demonstrates feasibility of cloud-based CTL model checking.
Abstract
The recent extensive availability of "big data" platforms calls for a more widespread adoption by the formal verification community. In fact, formal verification requires high performance data processing software for extracting knowledge from the unprecedented amount of data which come from analyzed systems. Since cloud based computing resources have became easily accessible, there is an opportunity for verification techniques and tools to undergo a deep technological transition to exploit the new available architectures. This has created an increasing interest in parallelizing and distributing verification techniques. In this paper we introduce a distributed approach which exploits techniques typically used by the "big data" community to enable verification of Computation Tree Logic (CTL) formulas on very large state spaces using distributed systems and cloud computing facilities. The…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Logic, programming, and type systems
