Dependency Analysis of Functional Specifications with Algebraic Data Structures

Thomas Jensen 1 Stephane Lescuyer 2 Andreescu Oana 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : In the context of interactive formal verification of complex systems, much effort is spent on proving the preservation of the systems invariants. However, most operations have a localized effect on the system, which only really impacts few invariants at the same time. Identifying those invariants that are unaffected by an operation can substantially ease the proof burden for the programmer. We present a dependency analysis for a strongly-typed, functional language, which computes a conservative approximation of the input fragments on which the operations depend. It is a flow-sensitive interprocedural analysis that handles arrays, structures and variant data types. For the latter, it simultaneously computes a subset of possible constructors. We have validated the scalability of the analysis to complex transition systems by applying it to a functional specification of the MINIX operating system.
Type de document :
Communication dans un congrès
17th International Conference on Formal Engineering Methods, ICFEM 2015, Nov 2015, Paris, France. Springer Verlag, Proc. of 17th International Conference on Formal Engineering Methods (ICFEM 2015), Springer LNCS vol. 9407, 9407, pp.18, 2015, Springer LNCS. 〈10.1007/978-3-319-25423-4_8〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01243002
Contributeur : Thomas Jensen <>
Soumis le : lundi 14 décembre 2015 - 14:10:03
Dernière modification le : jeudi 15 novembre 2018 - 11:57:43

Identifiants

Citation

Thomas Jensen, Stephane Lescuyer, Andreescu Oana. Dependency Analysis of Functional Specifications with Algebraic Data Structures. 17th International Conference on Formal Engineering Methods, ICFEM 2015, Nov 2015, Paris, France. Springer Verlag, Proc. of 17th International Conference on Formal Engineering Methods (ICFEM 2015), Springer LNCS vol. 9407, 9407, pp.18, 2015, Springer LNCS. 〈10.1007/978-3-319-25423-4_8〉. 〈hal-01243002〉

Partager

Métriques

Consultations de la notice

1292