Name
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-20398-5_37 | NASA Formal Methods |
Keywords | Field | DocType |
lattice model checker,counter-example guided abstraction refinement,automatic verification,lattice feature,cache analysis,automata language,efficient verification procedure,lattice automaton,efficient verification,opaal engine,new open source model,communication protocol,lattice model | Programming language,Abstraction,Lattice (order),Lossy compression,Cache,Computer science,Automaton,Theoretical computer science,Lattice model (finance),High-level verification,Communications protocol,Distributed computing | Conference |
Volume | ISSN | Citations |
6617 | 0302-9743 | 7 |
PageRank | References | Authors |
0.46 | 9 | 7 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Engelbredt Dalsgaard | 1 | 71 | 4.25 |
| René Rydhof Hansen | 2 | 392 | 32.52 |
| Kenneth Yrke Jørgensen | 3 | 40 | 2.87 |
| Kim G. Larsen | 4 | 3922 | 254.03 |
| Mads Chr. Olesen | 5 | 120 | 8.43 |
| Petur Olsen | 6 | 114 | 5.72 |
| Jiří Srba | 7 | 629 | 31.24 |