Author
|
Conference
|
Journal
|
Organization
|
Year
|
DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all domains
Limit my searches in the following domains
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(5)
Distributed Models
Load Balance
Safety Properties
State Space
On The Fly
Subscribe
Academic
Publications
Multi-Core LTSmin: Marrying Modularity and Scalability
Edit
Multi-Core LTSmin: Marrying Modularity and Scalability
(
Citations: 1
)
BibTex
|
RIS
|
RefWorks
Download
Alfons Laarman
,
Jaco van de Pol
,
Michael Weber
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 key feature is modularity: language frontends, optimization layers, and algorithmic backends are completely decoupled, without sacrificing performance. To complement our existing symbolic and distributed
model checking
algorithms, we added a multi-core backend for checking safety properties, with several new features to improve efficiency and memory usage: low-overhead load balancing, incremental hashing and scalable state compression.
Published in 2011.
DOI:
10.1007/978-3-642-20398-5_40
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
www.informatik.uni-trier.de
)
(
dx.doi.org
)
More »
Citation Context
(1)
...Now that tree compression reduces the space required for state storage, we observed that the open sets of the parallel reachability algorithm can become a memory bottleneck [
15
]...
...We measured compression ratios and performance characteristics for the models of the Beem database [19] with three tools: DiVinE 2.2, Spin 5.2.5 and our own model checker LTSmin [3,
15
]...
Alfons Laarman
,
et al.
Parallel Recursive State Compression for Free
References
(7)
A Database Approach to Distributed State Space Generation
(
Citations: 9
)
Stefan Blom
,
Bert Lisser
,
Jaco Van De Pol
,
Michael Weber
Journal:
Electronic Notes in Theoretical Computer Science - ENTCS
, vol. 198, no. 1, pp. 17-32, 2008
LTSmin: Distributed and Symbolic Reachability
(
Citations: 4
)
Stefan Blom
,
Jaco van de Pol
,
Michael Weber
Conference:
Computer Aided Verification - CAV
, pp. 354-359, 2010
The Design of a Multicore Extension of the SPIN Model Checker
(
Citations: 38
)
Gerard J. Holzmann
,
Dragan Bosnacki
Journal:
IEEE Transactions on Software Engineering - TSE
, vol. 33, no. 10, pp. 659-674, 2007
Boosting Multi-Core Reachability Performance with Shared Hash Tables
(
Citations: 3
)
Alfons Laarman
,
Jaco van de Pol
,
Michael Weber
Journal:
Computing Research Repository - CORR
, vol. abs/1004.2, pp. 247-255, 2010
Incremental Hashing for SPIN
(
Citations: 4
)
Viet Yen Nguyen
,
Theo C. Ruys
Published in 2008.
Order by:
Citations
(1)
Parallel Recursive State Compression for Free
(
Citations: 1
)
Alfons Laarman
,
Jaco van de Pol
,
Michael Weber
Journal:
Computing Research Repository - CORR
, vol. abs/1104.3, 2011