biblio
[1] Mounir Assaf, David A. Naumann Julien Signoles, Éric Totel, and Frédéric Tronel. Hypercollecting Semantics and its Application to Static Analysis of Information Flow. In Principles of Programming Languages (POPL 2017), January 2017. [ bib | .pdf ]
We show how static analysis for secure information flow can be expressed and proved correct entirely within the framework of abstract interpretation. The key idea is to define a Galois connection that directly approximates the hyperproperty of interest. To enable use of such Galois connections, we introduce a fixpoint characterisation of hypercollecting semantics, i.e. a “set of sets" transformer. This makes it possible to systematically derive static analyses for hyperproperties entirely within the calculational framework of abstract interpretation. We evaluate this technique by deriving example static analyses. For qualitative information flow, we derive a dependence analysis similar to the logic of Amtoft and Banerjee (SAS'04) and the type system of Hunt and Sands (POPL'06). For quantitative information flow, we derive a novel cardinality analysis that bounds the leakage conveyed by a program instead of simply deciding whether it exists. This encompasses problems that are hypersafety but not k-safety. We put the framework to use and introduce variations that achieve precision rivalling the most recent and precise static analyses for information flow.

[2] Arvid Jakobsson, Nikolai Kosmatov, and Julien Signoles. Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring for C. Science of Computer Programming, pages 226-246, October 2016. Extended version of [9]. [ bib | .pdf ]
One classical approach to ensuring memory safety of C programs is based on storing block metadata in a tree-like datastructure. However it becomes relatively slow when the number of memory locations in the tree becomes high. Another solution, based on shadow memory, allows very fast constant-time access to metadata and led to development of several highly optimized tools for the detection of memory safety errors. However, this solution appears to be insufficient for evaluation of complex memory-related properties of an expressive specification language.

In this work, we address memory monitoring in the context of runtime assertion checking of C programs annotated in , an expressive specification language offered by the framework for the analysis of C code. We present an original combination of a tree-based and a shadow-memory-based techniques that reconciles the efficiency of shadow memory and the higher expressiveness of annotations that can be evaluated using a tree of metadata. Shadow memory with its instant access to stored metadata is used whenever small shadow metadata suffices to evaluate required annotations, while richer metadata stored in a compact prefix tree (Patricia trie) is used for evaluation of more complex memory annotations supported by . We also present a preliminary static analysis step that determines which variables should be monitored (and in which way) in order to be able to evaluate annotations present in the program.

The combined monitoring technique and the pre-analysis step have been implemented in the runtime assertion checking tool for . Our initial experiments confirm that the proposed hybrid approach leads to a significant speedup with respect to an earlier implementation based on a Patricia trie alone without any loss of precision, while the proposed static analysis reduces the monitoring of irrelevant variables and further improves the performances of the instrumented code.

[3] Nikolai Kosmatov, Claude Marché, Julien Signoles, and Yannick Moy. Static vs dynamic verification in why3, frama-c and spark 2014. In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), October 2016. Invited paper. [ bib | .pdf ]
Why3 is an environment for static verification, generic in the sense that it is used as an intermediate tool by different front-ends for the verification of Java, C or Ada programs. Yet, the choices made when designing the specification languages provided by those front-ends differ significantly, in particular with respect to the executability of specifications. We review these differences and the issues that result from these choices. We emphasize the specific feature of ghost code which turns out to be extremely useful for both static and dynamic verification. We also present techniques, combining static and dynamic features, that help users understand why static verification fails.

[4] Nikolai Kosmatov and Julien Signoles. Frama-C, a Collaborative Framework for C Code Verification. Tutorial Synopsis. In International Conference on Runtime Verification (RV 2016), September 2016. [ bib | .pdf ]
Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static and dynamic analysis for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language, ACSL.

This paper presents a three-hour tutorial on Frama-C in which we provide a comprehensive overview of its most important plug-ins: the abstract-interpretation based plug-in Value, the deductive verification tool WP, the runtime verification tool E-ACSL and the test generation tool PathCrawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs.

[5] Mounir Assaf, Julien Signoles, Éric Totel, and Frédéric Tronel. The cardinal abstraction for quantitative information flow. In Workshop on Foundations of Computer Security (FCS 2016), June 2016. [ bib | .pdf ]
Qualitative information flow aims at detecting information leaks, whereas the emerging quantitative techniques target the estimation of information leaks. Quantifying information flow in the presence of low inputs is challenging, since the traditional techniques of approximating and counting the reachable states of a program no longer suffice.

This paper proposes an automated quantitative information flow analysis for imperative deterministic programs with low inputs. This approach relies on a novel abstract domain, the cardinal abstraction, in order to compute a precise upper-bound over the maximum leakage of batch-job programs. We prove the soundness of the cardinal abstract domain by relying on the framework of abstract interpretation. We also prove its precision with respect to a flow-sensitive type system for the two-point security lattice.

[6] Julien Signoles, editor. Actes des vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), January 2016. [ bib | http ]
[7] Daniel Fava, Julien Signoles, Matthieu Lemerre, Martin Schäf, and Ashish Tiwari. Gamifying Program Analysis. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015), pages 591-605, November 2015. [ bib | .pdf ]
Abstract interpretation is a powerful tool in program verification. Several commercial or industrial scale implementations of abstract interpretation have demonstrated that this approach can verify safety properties of real-world code. However, using abstract interpretation tools is not always simple. If no user-provided hints are available, the abstract interpretation engine may lose precision during widening and produce an overwhelming number of false alarms. However, manually providing these hints is time consuming and often frustrating when re-running the analysis takes a lot of time.

We present an algorithm for program verification that combines abstract interpretation, symbolic execution and crowdsourcing. If verification fails, our procedure suggests likely invariants, or program patches, that provide helpful information to the verification engineer and makes it easier to find the correct specification. By complementing machine learning with well-designed games, we enable program analysis to incorporate human insights that help improve their scalability and usability.

[8] Julien Signoles. Software Architecture of Code Analysis Frameworks Matters: The Frama-C Example. In Formal Integrated Development Environment (F-IDE 2015), pages 86-96, June 2015. [ bib | .pdf ]
Implementing large software, as software analyzers which aim to be used in industrial settings, requires a well-engineered software architecture in order to ease its daily development and its maintenance process during its lifecycle. If the analyzer is not only a single tool, but an open extensible collaborative framework in which external developers may develop plug-ins collaborating with each other, such a well designed architecture even becomes more important.

In this experience report, we explain difficulties of developing and maintaining open extensible collaborative analysis frameworks, through the example of Frama-C, a platform dedicated to the analysis of code written in C. We also present the new upcoming software architecture of Frama-C and how it aims to solve some of these issues.

[9] Arvid Jakobsson, Nikolai Kosmatov, and Julien Signoles. Fast as a Shadow, Expressive as a Tree: Hybrid Memory Monitoring for C. In Symposium On Applied Computing (SAC 2015), April 2015. [ bib | .pdf ]
One classical approach to ensuring memory safety of C programs is based on storing block metadata in a tree-like datastructure. However it becomes relatively slow when the number of memory locations in the tree becomes high. Another solution, based on shadow memory, allows very fast constant-time access to metadata and led to development of several highly optimized tools for detection of memory safety errors. However, this solution appears to be insufficient for evaluation of complex memory-related properties of an expressive specification language.

In this work, we address memory monitoring in the context of runtime assertion checking of C programs annotated in E-ACSL, an expressive specification language offered by the Frama-C framework for analysis of C code. We present an original combination of a tree-based and a shadow-memory-based techniques that reconciles both the efficiency of shadow memory with the higher expressiveness of annotations whose runtime evaluation can be ensured by a tree of metadata. Shadow memory with its instant access to stored metadata is used whenever small shadow metadata suffices to evaluate required annotations, while richer metadata stored in a compact prefix tree (Patricia trie) is used for evaluation of more complex memory annotations supported by E-ACSL. This combined monitoring technique has been implemented in the runtime assertion checking tool for E-ACSL. Our initial experiments confirm that the proposed hybrid approach leads to a significant speedup with respect to an earlier implementation based on a Patricia trie alone without any loss of precision.

[10] Arvid Jakobsson, Nikolai Kosmatov, and Julien Signoles. Rester statique pour devenir plus rapide, plus précis et plus mince. In David Baelde and Jade Alglave, editors, Journées Francophones des Langages Applicatifs (JFLA'15), Le Val d'Ajol, France, January 2015. [ bib | .pdf ]
E-ACSL est un greffon de Frama-C, une plateforme d'analyse de codes C qui est développée en OCaml. Son but est de transformer un programme C formellement annoté dans le langage de spécification éponyme E-ACSL en un autre programme C dont le comportement à l'exécution est équivalent si toutes les spécifications sont dynamiquement vérifiées et qui échoue sur la première spécification fausse sinon. Pour cela, une instrumentation du programme source est notamment effectuée afin, d'une part, de conserver les informations nécessaires à l'évaluation des prédicats E-ACSL et, d'autre part, de traduire correctement ces derniers.

Cet article présente deux analyses statiques qui améliorent grandement la précision de cette transformation de programmes en réduisant l'instrumentation effectuée. Ainsi, le code généré est plus rapide et consomme moins de mémoire lors de son exécution. La première analyse est un système de types fondé sur une inférence d'intervalles et permettant de distinguer les entiers (mathématiques) pouvant être convertis en des expressions C de type << entier machine >> de ceux devant être traduits vers des entiers en précision arbitraire. La seconde analyse est une analyse flot de données arrière sur-approximante paramétrée par une analyse d'alias. Elle permet de limiter l'instrumentation des opérations sur la mémoire à celles ayant un impact potentiel sur la validité d'une annotation formelle.

[11] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A Software Analysis Perspective. Formal Aspects of Computing, pages 1-37, January 2015. Extended version of [21]. [ bib | .pdf ]
[12] Guillaume Petiot, Bernard Botella, Jacques Julliand, Nikolai Kosmatov, and Julien Signoles. Instrumentation of annotated C programs for test generation. In International Conference on Source Code Analysis and Manipulation (SCAM 2014), pages 105-114, September 2014. [ bib | .pdf ]
Software verification and validation often rely on formal specifications that encode desired program properties. Recent research proposed a combined verification approach in which a program can be incrementally verified using alternatively deductive verification and testing. Both techniques should use the same specification expressed in a unique specification language. This paper addresses this problem within the Frama-C framework for analysis of C programs, that offers ACSL as a common specification language. We provide a formal description of an automatic translation of ACSL annotations into C code that can be used by a test generation tool either to trigger and detect specification failures, or to gain confidence, or, under some assumptions, even to confirm that the code is in conformity with respect to the annotations. We implement the proposed specification translation in a combined verification tool StaDy. Our initial experiments suggest that the proposed support for a common specification language can be very helpful for combined static-dynamic analyses.

[13] Nikolai Kosmatov and Julien Signoles. Runtime assertion checking and its combinations with static and dynamic analyses - tutorial synopsis. In International Conference on Tests and Proofs (TAP 2014), pages 165-168, July 2014. [ bib | .pdf ]
Among various static and dynamic software verification techniques, runtime assertion checking traditionally holds a particular place. Commonly used by most software developers, it can provide a fast feedback on the correctness of a property for one or several concrete executions of the program. Quite easy to realize for simple program properties, it becomes however much more complex for complete program contracts written in an expressive specification language. This paper presents a one-hour tutorial on runtime assertion checking in which we give an overview of this popular dynamic verification technique, present its various combinations with other verification techniques (such as static analysis, deductive verification, test generation, etc.) and emphasize the benefits and difficulties of these combinations. They are illustrated on concrete examples of C programs within the Frama-C software analysis framework using the executable specification language E-ACSL.

[14] Julien Signoles. Comment un chameau peut-il écrire un journal? In Journées Francophones des Langages Applicatifs (JFLA'14), January 2014. In French. [ bib | .pdf ]
Dans Frama-C, plate-forme d'analyse de code C développée en OCaml, un journal est un script OCaml généré automatiquement et permettant de reproduire les actions utilisateurs, notamment effectuées via l'interface utilisateur. Outre la reproductibilité des résultats qui est nécessaire dans un contexte industriel soumis à des exigences de certification fortes comme la norme avionique DO-178C, un journal permet d'automatiser le pilotage de l'outil dans un contexte d'utilisation particulier. Cet article présente comment le mécanisme de génération du journal de Frama-C, appelé journalisation et requérant intrinsèquement de l'introspection, a été développé en OCaml, en combinant typage statique et dynamique.

[15] Nikolaï Kosmatov, Guillaume Petiot, and Julien Signoles. An optimized memory monitoring for runtime assertion checking of C programs. In International Conference on Runtime Verification (RV 2013), volume 8174 of LNCS, pages 167-182. Springer, September 2013. [ bib | .pdf ]
Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. However, monitoring of annotations for pointers and memory locations (such as being valid, initialized, in a particular block, with a particular offset, etc.) is not straightforward and requires systematic instrumentation and monitoring of memory-related operations.

This paper describes the runtime memory monitoring library we developed for execution support of E-ACSL, executable specification language for C programs offered by the Frama-C platform for analysis of C code. We present the global architecture of our solution as well as various optimizations we realized to make memory monitoring more efficient. Our experiments confirm the benefits of these optimizations and illustrate the bug detection potential of runtime assertion checking with E-ACSL.

[16] Nikolaï Kosmatov and Julien Signoles. A lesson on runtime assertion checking with Frama-C. In International Conference on Runtime Verification (RV 2013), volume 8174 of LNCS, pages 386-399. Springer, September 2013. [ bib | .pdf ]
A tutorial about the Frama-C plug-in E-ACSL.

[17] Mounir Assaf, Julien Signoles, Éric Totel, and Frédéric Tronel. Moniteur hybride de flux d'information pour un langage supportant des pointeurs. In Conférence sur la Sécurité des Architectures Réseaux et des Systèmes d'Information (SARSSI'13)., September 2013. In French. Mounir Assaf won the conference's best student paper award for this paper. [ bib | .pdf ]
Les nouvelles approches combinant contrôle dynamique et statique de flux d'information sont prometteuses puisqu'elles permettent une approche permissive tout en garantissant la correction de l'analyse réalisée vis-à-vis de la non-interférence. Dans ce papier, nous présentons une approche hybride de suivi de flux d'information pour un langage gérant des pointeurs. Nous formalisons la sémantique d'un moniteur sensible aux flux de données qui combine analyse statique et dynamique. Nous prouvons ensuite la correction de notre moniteur vis-à-vis de la non-interférence.

[18] Mounir Assaf, Julien Signoles, Éric Totel, and Frédéric Tronel. Program transformation for non-interference verification on programs with pointers. In International Information Security and Privacy Conference (SEC'13), pages 231-244. Springer, July 2013. Mounir Assaf won the conference's best student paper award for this paper. [ bib | .pdf ]
Novel approaches for dynamic information flow monitoring are promising since they enable permissive (accepting a large subset of executions) yet sound (rejecting all unsecure executions) enforcement of non-interference. In this paper, we present a dynamic information flow monitor for a language supporting pointers. Our flow-sensitive monitor relies on prior static analysis in order to soundly enforce non-interference. We also propose a program transformation that preserves the behavior of initial programs and soundly inlines our security monitor. This program transformation enables both dynamic and static verification of non-interference.

[19] Nikolaï Kosmatov, Virgile Prevosto, and Julien Signoles. A lesson on proof of programs with Frama-C. In International Conference on Tests and Proofs (TAP'13), June 2013. Invited Tutorial Paper. [ bib | .pdf ]
A tutorial about the Frama-C plug-in Jessie.

[20] Mickaël Delahaye, Nikolaï Kosmatov, and Julien Signoles. Common specification language for static and dynamic analysis of C programs. In Symposium on Applied Computing (SAC'13), pages 1230-1235. ACM, March 2013. [ bib | .pdf ]
Various combinations of static and dynamic analysis techniques were recently shown to be beneficial for software verification. A frequent obstacle to combining different tools in a completely automatic way is the lack of a common specification language. Our work proposes to translate a Pre-Post based specification into executable C code. This paper presents E-ACSL, subset of the ACSL specification language for C programs, and its automatic translator into C implemented as a Frama-C plug-in. The resulting C code is executable and can be used by a dynamic analysis tool. We illustrate how the PathCrawler test generation tool automatically treats such pre- and postconditions specified as C functions.

[21] Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-c: a software analysis perspective. In International Conference on Software Engineering and Formal Methods (SEFM'12), pages 233-247. Springer, October 2012. [ bib | .pdf ]
Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.

[22] Loïc Correnson and Julien Signoles. Combining Analyses for C Program Verification. In Mariëlle Stoelinga and Ralf Pinger, editors, Formal Methods for Industrial Case Studies (FMICS'12), volume 7437 of Lecture Notes in Computer Science, pages 108-130. Springer, August 2012. [ bib | .pdf ]
Static analyzers usually return partial results. They can assert that some properties are valid during all possible executions of a program, but generally leave some other properties to be verified by other means. In practice, it is common to combine results from several methods manually to achieve the full verification of a program. In this context, Frama-C is a platform for analyzing C source programs with multiple analyzers. Hence, one analyzer might conclude about properties assumed by another one, in the same environment. We present here the semantical foundations of validity of program properties in such a context. We propose a correct and complete algorithm for combining several partial results into a fully consolidated validity status for each program property. We illustrate how such a framework provides meaningful feedback on partial results.

[23] Pascal Cuoq, Damien Doligez, and Julien Signoles. Lightweight typed customizable unmarshaling. In Workshop on ML (ML'11). ACM, September 2011. [ bib | .pdf ]
The contribution of this work is threefold. First, we offer an OCaml unmarshaling algorithm that uses a lightweight type-directed description of the expected structure of data to make consistency checks. The second contribution is the opportunity to specify functions to be systematically applied on values as they are being unmarshaled. Our third contribution is a type-safe layer for these functions and for the unmarshaling algorithm itself.

[24] Julien Signoles. Une bibliothèque de typage dynamique en OCaml. In Journées Francophones des Langages Applicatifs (JFLA'11), Studia Informatica Universalis, 2011. In French. [ bib | .pdf ]
Cet article présente une bibliothèque OCaml fournissant une représentation dynamique des types monomorphes, y compris pour les instances des types polymorphes et les types de données abstraits. Elle permet ainsi de voir les types OCaml comme des citoyens de première classe. Elle comble aussi le fossé séparant OCaml des langages dynamiques en mêlant vérifications statiques et dynamiques des types. Nous nous concentrons ici sur le coeur de son implantation, ses propriétés théoriques et l'usage qui en est fait dans Frama-C, plateforme logicielle libre d'analyse statique de programmes C au sein de laquelle cette bibliothèque est distribuée.

[25] David Delmas, Stéphane Duprat, Victoria Moya-Lamiel, and Julien Signoles. Taster, a Frama-C plug-in to enforce Coding Standards. In Embedded Real-Time Software and Systems Congress (ERTSS'10), 2010. [ bib | .pdf ]
Enforcing Coding Standards is part of the traditional concerns of industrial software developments. In this paper, we present a framework based on the open source Frama-C platform for easily developing syntactic, typing (and even some semantic) analyses of C source code, among which conformance to Coding Standards. We report on our successful attempt to develop a Frama-C plug-in named Taster, in order to replace a commercial, off-the-shelf, legacy tool in the verification process of several Airbus avionics software products. We therefore present the types of coding rules to be verified, the Frama-C platform and the Taster plug-in. We also discuss ongoing industrial deployment and qualification activities.

[26] Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon, Géraud Canet, Loïc Correnson, Benjamin Monate, Virgile Prevosto, and Armand Puccetti. Experience report: Ocaml for an industrial-strength static analysis framework. In Graham Hutton and Andrew P. Tolmach, editors, International Conference of Functional Programming (ICFP'09), pages 281-286. ACM, September 2009. [ bib | .pdf ]
This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources...) but could have prevented the use of OCaml for this project if they had been missing.

[27] Julien Signoles. Foncteurs impératifs et composés: la notion de projet dans Frama-C. In Alan Schmitt, editor, Journées Francophones des Langages Applicatifs (JFLA'09), volume 7.2 of Studia Informatica Universalis, pages 245-280, September 2009. In French. [ bib | .pdf ]
Cet article présente la bibliothèque de projets de Frama-C, une plateforme facilitant le développement d'analyseurs statiques de programmes C. Grâce à sa description, nous présentons une utilisation originale des foncteurs du système de modules de ML qui exploite aussi bien leur caractère impératif que compositionnel. Ceci est le seul véritable recours pour réaliser la fonctionalité souhaitée de manière bien typée. En outre, nous montrons un exemple peu fréquent d'un même foncteur appliqué plusieurs centaines de fois. Cet article introduit aussi la plateforme Frama-C elle-même, à travers un de ses aspects essentiels, la notion de projet.

[28] Benjamin Monate and Julien Signoles. Slicing for security of code. In Peter Lipp, Ahmad-Reza Sadeghi, and Klaus-Michael Koch, editors, TRUST, volume 4968 of Lecture Notes in Computer Science, pages 133-142. Springer-Verlags, March 2008. [ bib | .pdf ]
Bugs in programs implementing security features can be catastrophic: for example they may be exploited by malign users to gain access to sensitive data. These exploits break the confidentiality of information. All security analyses assume that softwares implementing security features correctly implement the security policy, i.e. are security bug-free. This assumption is almost always wrong and IT security administrators consider that any software that has no security patches on a regular basis should be replaced as soon as possible. As programs implementing security features are usually large, manual auditing is very error prone and testing techniques are very expensive. This article proposes to reduce the code that has to be audited by applying a program reduction technique called slicing. Slicing transforms a source code into an equivalent one according to a set of criteria. We show that existing slicing criteria do not preserve the confidentiality of information. We introduce a new automatic and correct source-to-source method properly preserving the confidentiality of information i.e. confidentiality is guaranteed to be exactly the same in the original program and in the sliced program.

[29] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a generic graph library using ML functors. In Trends in Functional Programming (TFP'07), April 2007. [ bib | .ps.gz ]
This article details the design and implementation of Ocamlgraph, a highly generic graph library for the programming language OCaml. This library features a large set of graph data structures-directed or undirected, with or without labels on vertices and edges, as persistent or mutable data structures, etc.-and a large set of graph algorithms. Algorithms are written independently from graph data structures, which allows combining user data structure (resp. algorithm) with Ocamlgraph algorithm (resp. data structure). Genericity is obtained through massive use of the OCaml module system and its functions, the so-called functors.

[30] Julien Signoles. Extension de ML avec raffinement: syntaxe, sémantiques et système de types. PhD thesis, Université Paris-Sud, Orsay, France, July 2006. In French. [ bib | .ps.gz ]
Refinement is a method to derive correct programs from specifications. An expressive type language is another way to ensure program correctness. We propose an extension of ML mixing both above approaches: programs may be built by successive refinements of specifications and a type system ensures the correctness of each refinement step.

At the syntactic level, our extension adds base types into expressions, introducing underdeterminism and dependent types. It also introduces a new construct, called demonic application, which increases the expressiveness of the specification language.

We study the denotational and operational semantics of this extension. We prove that their are equivalent and conservative with respect to the usual ML semantics. We also propose a system which generates proof obligations: their validities imply the correctness of the input program with respect to its specification is ensured.

Besides, we have implemented a prototype and the first experimental results are promising. Additions of missing ML features are also discussed.

[31] Julien Signoles. Towards a ML Extension with Refinement: a Semantic Issue. Technical Report 1440, LRI, University of Paris Sud, March 2006. [ bib | .pdf ]
Refinement is a method to derive correct programs from specifications. A rich type language is another way to ensure program correctness. In this paper, we propose a wide-spectrum language mixing both approaches for the ML language. Mainly, base types are simply included into expressions, introducing underdeterminism and dependent types. We focus on the semantic aspects of such a language. We study three different semantics: a denotational, a deterministic operational and a nondeterministic operational semantics. We prove their equivalence. We show that this language is a conservative extension of ML.

[32] Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Le foncteur sonne toujours deux fois. In Journées Francophones des Langages Applicatifs (JFLA'05), March 2005. In French. [ bib | .ps.gz ]
Cet article présente Ocamlgraph, une bibliothèque générique de graphes pour le langage de programmation OCaml. L'originalité de cette bibliothèque est de proposer d'une part un grand nombre de structures de données différentes pour représenter les graphes - graphes orientés ou non, structures persistantes ou modifiées en place, sommets et arcs avec ou sans étiquettes, marques sur les sommets, etc. - et d'autre part des algorithmes sur les graphes écrits indépendamment de la structure de données représentant les graphes. Le codage de ces deux aspects originaux a été rendu possible par une utilisation massive du système de modules d'OCaml et notamment de ses fonctions, les foncteurs.

[33] Julien Signoles. Une approche fonctionnelle du modèle vue-contrôleur. In Journées Francophones des Langages Applicatifs (JFLA'05), March 2005. In French. [ bib | .ps.gz ]
Le << Modèle-Vue-Contrôleur >> (MVC) est un patron de conception fréquemment utilisé pour aider au développement d'interfaces graphiques en séparant l'état d'une entité (son modèle) de ses interactions avec l'utilisateur, notamment ses diverses représentations graphiques (ses vues). À l'instar de tous les patrons de conception, le MVC est toujours lié au paradigme de la programmation objet alors que les seules notions nécessaires à sa mise en œuvre sont les types, le polymorphisme, les interfaces et les implantations. Dans cet article, nous étudions le MVC dans un autre cadre tout aussi propice à sa mise en œuvre : celui d'un système de modules à la ML. Cette étude nous conduit à implanter le MVC de manière générique ; ce qui limite le schéma de code à implanter à chacune de ses utilisations.

[34] Julien Signoles. Calcul statique des applications de modules paramétrés. In Journées Francophones des Langages Applicatifs (JFLA'03), January 2003. In French. [ bib | .ps.gz ]
Le système de module d'ph Objective Caml fournit au programmeur la possibilité de réutiliser facilement du code grâce aux modules paramétrés encore appelés foncteurs. Cependant, l'utilisation des foncteurs entraîne un surcoût à l'exécution et pose problème aux outils d'analyse statique.

Bêta-réduire statiquement les applications de foncteurs pallie ces défauts mais pose des problèmes de captures de variables et de préservation des effets de bord. Dans cet article, nous présentons une méthode effectuant cette opération en résolvant ces problèmes. D'un point de vue théorique, nous montrons qu'elle préserve la sémantique, y compris en présence d'effets de bord. Nous présentons également son implantation.

[35] Julien Signoles. Calcul statique des applications de foncteurs en présence d'effets de bord. Mémoire de DEA, Université Paris-Sud, Orsay, France, September 2002. In French. [ bib | .ps.gz ]
Le système de module d'OCaml fournit au programmeur la possibilité de réutiliser facilement du code grâce aux modules paramétrés encore appelés <<foncteurs>>. Cependant, utiliser (<<appliquer>>) ces foncteurs réduit la rapidité d'un programme et empêche en général les outils d'analyse statique de fonctionner correctement.

Dans cette étude, nous présentons une méthode pour calculer statiquement les applications de foncteur d'un programme OCaml pour pallier ces défauts. Cette opération, nommée défonctorisation, se base sur des techniques de réécriture. Nous montrons qu'elle préserve la sémantique d'un programme, y compris d'un programme impératif en présence d'effets de bord. En outre, nous présentons l'implantation que nous avons réalisée de cette opération et un cas d'utilisation possible.

[36] Julien Signoles. E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.8, March 2014. [ bib | .pdf ]
[37] Julien Signoles. E-ACSL Version 1.8. Implementation in Frama-C Plug-in E-ACSL version 0.4, March 2014. [ bib | .pdf ]
[38] Julien Signoles. E-ACSL User Manual, March 2014. [ bib | .pdf ]
[39] Loïc Correnson, Pascal Cuoq, Florent Kirchner, Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski. Frama-C User Manual, March 2014. [ bib | .pdf ]
[40] Julien Signoles, Loïc Correnson, and Virgile Prevosto. Frama-C Plug-in Development Guide, March 2014. [ bib | .pdf ]
[41] Philippe Herrmann and Julien Signoles. Annotation generation: Frama-C's RTE plug-in, March 2014. [ bib | .pdf ]