DALSGAARD, Andreas E., Rene R. HANSEN, Kenneth Y. JOERGENSEN, Kim G. LARSEN, Mads Chr. OLESEN and Jiří SRBA. opaal: A Lattice Model Checker. In Proceedings of the 3rd NASA Formal Methods Symposium ({NFM}'11). Neuveden: Springer-Verlag, 2011, p. 487-493. ISBN 978-3-642-20397-8. Available from: https://dx.doi.org/10.1007/978-3-642-20398-5.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name opaal: A Lattice Model Checker
Authors DALSGAARD, Andreas E. (208 Denmark), Rene R. HANSEN (208 Denmark), Kenneth Y. JOERGENSEN (208 Denmark), Kim G. LARSEN (208 Denmark), Mads Chr. OLESEN (208 Denmark) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution).
Edition Neuveden, Proceedings of the 3rd NASA Formal Methods Symposium ({NFM}'11), p. 487-493, 7 pp. 2011.
Publisher Springer-Verlag
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Netherlands
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
WWW URL
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/11:00067342
Organization unit Faculty of Informatics
ISBN 978-3-642-20397-8
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-20398-5
UT WoS 000301947700037
Keywords in English verification; lattice; tool
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 29/4/2014 06:05.
Abstract
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.
Links
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
PrintDisplayed: 30/4/2024 13:00