HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Dependency Analysis of Functional Specifications with Algebraic Data Structures

Oana Andreescu 1 Thomas Jensen 1 Stephane Lescuyer 2
1 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
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.
Complete list of metadata

Contributor : Thomas Jensen Connect in order to contact the contributor
Submitted on : Monday, December 14, 2015 - 2:10:03 PM
Last modification on : Thursday, January 20, 2022 - 5:33:19 PM



Oana Andreescu, Thomas Jensen, Stephane Lescuyer. Dependency Analysis of Functional Specifications with Algebraic Data Structures. 17th International Conference on Formal Engineering Methods, ICFEM 2015, Michael Butler Sylvain Conchon Fatiha Zaïdi, Nov 2015, Paris, France. pp.18, ⟨10.1007/978-3-319-25423-4_8⟩. ⟨hal-01243002⟩



Record views