Name
Abstract | ||
|---|---|---|
This paper discusses the design and implementation of a bounded model checker for SPARK code, and provides a proof of concept of the utility and practicality of bounded verification for SPARK. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-11936-6_3 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
spark | Spark (mathematics),Model checking,Computer science,Theoretical computer science,Loop invariant,Proof of concept,Symbolic execution,Bounded function | Conference |
Volume | ISSN | Citations |
8837 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 12 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cláudio Belo Lourenço | 1 | 1 | 2.04 |
| Maria Joao Frade | 2 | 5 | 0.81 |
| Jorge Sousa Pinto | 3 | 160 | 23.19 |