@conference {PintoJS:usiaipdacs, title = {Using Abstract Interpretation to Produce Dependable Aerospace Control Software}, booktitle = {Industrial Track of the 6th Latin American Symposium on Dependable Computing - LADC}, year = {2013}, month = {April}, address = {Rio de Janeiro, Brazil}, abstract = {

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.

}, attachments = {https://haslab.uminho.pt/sites/default/files/jsp/files/ladc2013_-_industrial_track_using_abstract_interpretation_to_produce_dependable_aerospace_control_sw.pdf}, author = {Rovedy Aparecida Busquim Silva and Nanci Naomi Arai and Luciana Akemi Burgareli and Jos{\'e} M. Parente Oliveira and Jorge Sousa Pinto}, editor = {F{\'a}tima Mattiello-Francisco} }