Name
Abstract | ||
|---|---|---|
This paper describes a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automatically extracts from an Ada program a SPIN model, together with a set of desirable properties. ATOS is also capable of extracting properties from a specification annotated by the user in the program, inspired by the SPARK Annotation language. The goal of ATOS is to help in the verification of sequential and concurrent Ada programs, based on model checking. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-30598-6_8 | Ada-Europe |
Keywords | Field | DocType |
tool-supported method,spark annotation language,model checking,concurrent ada program,ada program,spin model,desirable property,formal verification | Spark (mathematics),Programming language,Annotation,Model checking,Computer science,Linear temporal logic,Symbolic execution,Spin model,Formal verification | Conference |
Citations | PageRank | References |
1 | 0.35 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| José Miguel Faria | 1 | 1 | 0.35 |
| João Martins | 2 | 1 | 0.69 |
| Jorge Sousa Pinto | 3 | 160 | 23.19 |