Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{963628,
author = {Dalsgaard, Andreas E. and Hansen, Rene R. and Joergensen, Kenneth Y. and Larsen, Kim G. and Olesen, Mads Chr. and Srba, Jiří},
address = {Neuveden},
booktitle = {Proceedings of the 3rd NASA Formal Methods Symposium ({NFM}'11)},
doi = {http://dx.doi.org/10.1007/978-3-642-20398-5},
keywords = {verification; lattice; tool},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Neuveden},
isbn = {978-3-642-20397-8},
pages = {487-493},
publisher = {Springer-Verlag},
title = {opaal: A Lattice Model Checker},
url = {http://www.springerlink.com/content/978-3-642-20397-8},
year = {2011}
}
TY - JOUR
ID - 963628
AU - Dalsgaard, Andreas E. - Hansen, Rene R. - Joergensen, Kenneth Y. - Larsen, Kim G. - Olesen, Mads Chr. - Srba, Jiří
PY - 2011
TI - opaal: A Lattice Model Checker
PB - Springer-Verlag
CY - Neuveden
SN - 9783642203978
KW - verification
KW - lattice
KW - tool
UR - http://www.springerlink.com/content/978-3-642-20397-8
N2 - 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.
ER -
DALSGAARD, Andreas E., Rene R. HANSEN, Kenneth Y. JOERGENSEN, Kim G. LARSEN, Mads Chr. OLESEN a Jiří SRBA. opaal: A Lattice Model Checker. In \textit{Proceedings of the 3rd NASA Formal Methods Symposium ($\{$NFM$\}$'11)}. Neuveden: Springer-Verlag, 2011, s.~487-493. ISBN~978-3-642-20397-8. Dostupné z: https://dx.doi.org/10.1007/978-3-642-20398-5.
|
