opaal: A Lattice Model Checker

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F11%3A00067342" target="_blank" >RIV/00216224:14330/11:00067342 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-642-20398-5" target="_blank" >http://dx.doi.org/10.1007/978-3-642-20398-5</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-20398-5" target="_blank" >10.1007/978-3-642-20398-5</a>

Result language
angličtina
Original language name
opaal: A Lattice Model Checker
Original language description
We present a new open source model checker, opaal, for automatic verification of models using lattice automata. Lattice automata allow the users to incorporate abstractions of a model into the model itself. This provides an efficient verification procedure, while giving the user fine-grained control of the level of abstraction by using a method similar to Counter-Example Guided Abstraction Refinement. The opaal engine supports a subset of the UPPAAL timed automata language extended with lattice features. We report on the status of the first public release of opaal, and demonstrate how opaal can be used for efficient verification on examples from domains such as database programs, lossy communication protocols and cache analysis.
Czech name
—
Czech description
—

Publication year
2011
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Proceedings of the 3rd NASA Formal Methods Symposium ({NFM}'11)
ISBN
9783642203978
ISSN
0302-9743
e-ISSN
—
Number of pages
7
Pages from-to
487-493
Publisher name
Springer-Verlag
Place of publication
Neuveden
Event location
USA
Event date
Jan 1, 2011
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)