Name
Abstract | ||
|---|---|---|
We present the new tool Lodin for statistical model checking of LLVM-bitcode. Lodin implements a simulation engine for LLVM-bitcode and implements classic statistical model checking algorithms on top of it. The simulation engine implements only the core of LLVM but supports extending this core through a plugin-architecture. Besides the statistical model checking algorithms Lodin also provides an interactive simulation front-end. The simulator front-end was integral for our second contribution - an integration of Lodin into Plasma-Lab. The integration with Plasma-Lab is integral to allow reasoning about rare properties of programs. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-95582-7_32 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Programming language,Computer science,Interactive simulation,Statistical model checking,Theoretical computer science | Conference | 10951 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
13 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Axel Legay | 1 | 2982 | 181.47 |
| Dirk Nowotka | 2 | 213 | 42.90 |
| Danny Bøgsted Poulsen | 3 | 308 | 13.03 |
| Louis-Marie Traonouez | 4 | 243 | 18.50 |