Výsledky vyhledávání - "Distributed model checking"

Publikováno v: Lecture Notes in Computer Science ISBN: 9783319779348
NFM

Model checking larger specifications can take a lot of time, from several minutes up to weeks. Naturally, this renders the development of a correct specification very cumbersome. If the model offers enough non-determinism, however, we can distribute

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::e0eb432909a320fd58cb5f693fa6dfc2
https://doi.org/10.1007/978-3-319-77935-5_18

Zobrazit plný text záznamu

Distributed Partial Order Reduction of State Spaces

Autor: Pavel Moravec, Ivana Černá, Luboš Brim, Jiri Simsa

Publikováno v: Electronic Notes in Theoretical Computer Science. 128(3):63-74

State space explosion is a fundamental obstacle in formal verification of concurrent systems. Several techniques for combating this problem have emerged in the past few years, among which the two we are interested in are: partial order reduction and

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d56cee182df87e03e02a2957e1331874

Zobrazit plný text záznamu

Multi-Core LTSmin: Marrying Modularity and Scalability

Autor: Laarman, Alfons, van de Pol, Jan Cornelis, Weber, M., Bobaru, Michaela, Havelund, Klaus, Holzmann, Gerard J., Joshi, Rajeev

Publikováno v: Lecture Notes in Computer Science ISBN: 9783642203978
NASA Formal Methods
Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011, 506-511
STARTPAGE=506;ENDPAGE=511;TITLE=Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011

The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c610488c39cde9378ae9c8302857bbd9
https://doi.org/10.1007/978-3-642-20398-5_40

Zobrazit plný text záznamu

A Database Approach to Distributed State-Space Generation

Autor: Blom, Stefan, Cerna, I., Haverkort, Boudewijn R.H.M., Lisser, Bert, van de Pol, Jan Cornelis, Weber, M.

Publikováno v: Journal of logic and computation, Advance Ac(1):10.1093/logcom/exp004, 45-62. Oxford University Press

We study distributed state-space generation on a cluster of workstations. It is explained why state-space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive dat

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b0a7601cf6d8c12546fc60af747708b2
https://doi.org/10.1093/logcom/exp004

Zobrazit plný text záznamu

Distributed Verification of Multi-threaded C++ Programs

Autor: Stefan Edelkamp, Shahid Jabbar, Damian Sulewski

Publikováno v: Electronic Notes in Theoretical Computer Science. 198(1):33-46

Verification of multi-threaded C++ programs poses three major challenges: the large number of states, states with huge sizes, and time intensive expansions of states. This paper presents our efforts in addressing these issues by combining an efficien

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2cc54fbbff647284e8c9de0dc96d1c7c

Zobrazit plný text záznamu

State Distribution Policy for Distributed Model Checking of Actor Models

Autor: Khamespanah, Ehsan, Sirjani, Marjan, Mousavi, Mohammad Reza, Sabahi Kaviani, Zeynab, Razzazi, Mohammad Reza

Model checking temporal properties is often reduced to finding accepting cycles in Buchi automata. A key ingredient for an effective distributed model checking technique is a distribution policy that does not split the potential accepting cycles of t

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ceb1561bc877d6e95213adf27f6eebd4

Zobrazit plný text záznamu

A state space distribution policy based on abstract interpretation

Publikováno v: Electronic Notes in Theoretical Computer Science. 128(3):35-45

We aim at improving the performance of distributed algorithms for model checking and state space reduction. To this end, we introduce a new distribution policy of states over workers. This policy reduces the number of transitions between states locat

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dris___00893::5fcb7c17ab206c282a239de3fb9b3e3b
https://ir.cwi.nl/pub/14576

Zobrazit plný text záznamu

Distributed Model Checking: From Abstract Algorithms to Concrete Implementations

Autor: Christophe Joubert

Publikováno v: Electronic Notes in Theoretical Computer Science. 89(1):114-127

Distributed Model Checking ( DMC ) is based on several distributed algorithms, which are often complex and error prone. In this paper, we consider one fundamental aspect of DMC design: message passing communication, the implementation of which presen

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::99519feeb5607080c3a20b381e0f28c1

Zobrazit plný text záznamu

A state space distribution policy based on abstract interpretation

Autor: Orzan, S.M., Pol, van de, J.C., Valero Espada, M.A., Brim, L., Leucker, M.

Publikováno v: Electronic Notes in Theoretical Computer Science, 128(3), 35-45
Proceedings 3rd International Workshop on Parallel and Distributed Methods in Verification (PDMC '04, London, UK, September 4, 2004), 35-45
STARTPAGE=35;ENDPAGE=45;TITLE=Proceedings 3rd International Workshop on Parallel and Distributed Methods in Verification (PDMC '04, London, UK, September 4, 2004)

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5c8c4d9d305b649be7b893b02f6bd419
https://ir.cwi.nl/pub/14576

Zobrazit plný text záznamu

Mechanised Verification of Distributed State-Space Algorithms for Security Protocols

Autor: Frédéric Gava, Jean Fortin, Arthur Hidalgo

Publikováno v: PDCAT

Explicit model-checking (MC) is a classical solution to find flaws in a security protocol. But it is well-known that for non trivial protocols, MC may enumerate state-spaces of astronomical sizes - the famous state-space explosion problem. Distribute

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::7822cd6f37894e32c894e94f5e5552d7
https://doi.org/10.1109/pdcat.2012.93

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání