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.
['José Miguel Faria', 'João Miguel Alexandre Martins', 'Jorge Sousa Pinto']
An approach to model checking ada programs