%0 Conference Paper %B Industrial Track of the 6th Latin American Symposium on Dependable Computing - LADC %D 2013 %T Using Abstract Interpretation to Produce Dependable Aerospace Control Software %A Rovedy Aparecida Busquim Silva %A Nanci Naomi Arai %A Luciana Akemi Burgareli %A José M. Parente Oliveira %A Jorge Sousa Pinto %E Fátima Mattiello-Francisco %C Rio de Janeiro, Brazil %X

n the context of software dependability, the software verification process has an important role. Formal verification of programs is an activity that can be inserted in this process to improve software reliability. This paper presents the definition of an approach that employs a formal verification technique based on abstract interpretation. The main goal is to apply this technique as a formal activity in the software verification process to help software engineers identify programs faults. The applicability of the proposed approach is demonstrated by a case study based on embedded aerospace control software. The results obtained from its use show that abstract interpretation can contribute to software dependability.

%8 April %> https://haslab.uminho.pt/sites/default/files/jsp/files/ladc2013_-_industrial_track_using_abstract_interpretation_to_produce_dependable_aerospace_control_sw.pdf