biblio.bib

biblio.bib

@inproceedings{popl17,
  author = {Mounir Assaf and
               David A. Naumann
               Julien Signoles and
               Éric Totel and
               Frédéric Tronel},
  title = {{Hypercollecting Semantics and its Application to Static 
Analysis of Information Flow}},
  booktitle = {Principles of Programming Languages
               (POPL 2017)},
  year = {2017},
  month = jan,
  url = {publis/2017_popl.pdf},
  abstract = {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.}
}
@article{scp16,
  title = {{Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring 
for C}},
  author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
  journal = {Science of Computer Programming},
  publisher = {Elsevier},
  pages = {226-246},
  language = {English},
  year = {2016},
  month = oct,
  url = {publis/2016_scp.pdf},
  note = {Extended version of \cite{sac15}},
  abstract = {
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 \EACSL, an expressive 
specification language 
offered by the \FramaC 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 \EACSL.
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 \EACSL.
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.
}
}
@inproceedings{isola16,
  title = {Static vs Dynamic Verification in Why3, Frama-C and SPARK 2014},
  author = {Nikolai Kosmatov and Claude March\'e and Julien Signoles and 
Yannick Moy},
  booktitle = {International Symposium On Leveraging Applications of Formal
 Methods, Verification and Validation (ISoLA 2016)},
  note = {Invited paper},
  year = 2016,
  month = oct,
  url = {publis/2016_isola.pdf},
  abstract = {
  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 \emph{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.
}
}
@inproceedings{rv16,
  title = {{Frama-C, a Collaborative Framework for C Code Verification.
Tutorial Synopsis}},
  author = {Nikolai Kosmatov and Julien Signoles},
  booktitle = {International Conference on
              Runtime Verification ({RV 2016})},
  year = 2016,
  month = sep,
  url = {publis/2016_rv.pdf},
  abstract = {
  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
  Path\-Crawler.  We also emphasize different possible collaborations between
  these plug-ins and a few others. The presentation is illustrated on concrete
  examples of C programs.
}
}
@inproceedings{fcs16,
  author = {Mounir Assaf and
               Julien Signoles and
               Éric Totel and
               Frédéric Tronel},
  title = {The Cardinal Abstraction for Quantitative Information Flow},
  booktitle = {Workshop on Foundations of Computer Security (FCS 2016)},
  month = jun,
  year = 2016,
  url = {publis/2016_fcs.pdf},
  abstract = {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.
}
}
@proceedings{jfla16,
  title = {{Actes des vingt-septièmes Journées Francophones des Langages
Applicatifs (JFLA 2016)}},
  year = {2016},
  editor = {Julien Signoles},
  month = jan,
  url = {https://hal.archives-ouvertes.fr/JFLA2016}
}
@inproceedings{lpar15,
  author = {Daniel Fava and
               Julien Signoles and
               Matthieu Lemerre and
               Martin Sch{\"{a}}f and
               Ashish Tiwari},
  title = {{Gamifying Program Analysis}},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning
               (LPAR 2015)},
  pages = {591--605},
  year = {2015},
  month = nov,
  url = {publis/2015_lpar.pdf},
  abstract = {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.}
}
@inproceedings{fide15,
  author = {Julien Signoles},
  title = {{Software Architecture of Code Analysis Frameworks Matters:
               The Frama-C Example}},
  booktitle = {Formal Integrated Development Environment (F-IDE 2015)},
  pages = {86--96},
  year = {2015},
  month = jun,
  url = {publis/2015_fide.pdf},
  abstract = {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.}
}
@inproceedings{sac15,
  title = {{Fast as a Shadow, Expressive as a Tree: Hybrid Memory Monitoring for
 C.}},
  author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
  booktitle = {Symposium On Applied Computing (SAC 2015)},
  year = 2015,
  month = apr,
  url = {publis/2015_sac.pdf},
  abstract = {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.}
}
@inproceedings{jfla15,
  title = {{Rester statique pour devenir plus rapide, plus pr{\'e}cis et plus mince}},
  author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
  booktitle = {Journées Francophones des Langages Applicatifs (JFLA'15)},
  address = {Le Val d'Ajol, France},
  editor = {David Baelde and Jade Alglave},
  year = {2015},
  month = jan,
  url = {publis/2015_jfla.pdf},
  abstract = {
  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. 
}
}
@article{fac15,
  title = {{Frama-C: A Software Analysis Perspective}},
  author = {Florent Kirchner and Nikolai Kosmatov and Virgile Prevosto and
Julien Signoles and Boris Yakobowski},
  journal = {Formal Aspects of Computing},
  publisher = {Springer London},
  pages = {1-37},
  language = {English},
  year = {2015},
  month = jan,
  url = {publis/2015_fac.pdf},
  note = {Extended version of \cite{sefm12}}
}
@inproceedings{scam14,
  author = {Guillaume Petiot and
               Bernard Botella and
               Jacques Julliand and
               Nikolai Kosmatov and
               Julien Signoles},
  title = {Instrumentation of Annotated {C} Programs for Test Generation},
  booktitle = {International Conference on Source Code Analysis
               and Manipulation ({SCAM 2014})},
  pages = {105--114},
  year = {2014},
  month = sep,
  url = {publis/2014_scam.pdf},
  abstract = {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.}
}
@inproceedings{tap14,
  author = {Nikolai Kosmatov and
               Julien Signoles},
  title = {Runtime Assertion Checking and Its Combinations with Static and Dynamic
               Analyses - Tutorial Synopsis},
  booktitle = {International Conference on Tests and Proofs ({TAP} 2014)},
  pages = {165--168},
  year = {2014},
  month = jul,
  url = {publis/2014_tap.pdf},
  abstract = {
  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.
}
}
@inproceedings{jfla14,
  author = {Julien Signoles},
  title = {Comment un chameau peut-il écrire un journal?},
  booktitle = {Journées Francophones des Langages Applicatifs (JFLA'14)},
  year = 2014,
  month = jan,
  note = {In French},
  url = {publis/2014_jfla.pdf},
  abstract = {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.}
}
@inproceedings{rv13,
  author = {Nikolaï Kosmatov and Guillaume Petiot and Julien Signoles},
  title = {An Optimized Memory Monitoring for Runtime Assertion Checking of 
             {C} Programs},
  booktitle = {International Conference on
              Runtime Verification ({RV 2013})},
  publisher = {Springer},
  series = {LNCS},
  volume = {8174},
  pages = {167--182},
  year = 2013,
  month = sep,
  url = {publis/2013_rv_2.pdf},
  abstract = {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.
}
}
@inproceedings{rv13tutorial,
  author = {Nikolaï Kosmatov and Julien Signoles},
  title = {A Lesson on Runtime Assertion Checking with {Frama-C}},
  booktitle = {International Conference on Runtime Verification ({RV 2013})},
  publisher = {Springer},
  series = {LNCS},
  volume = {8174},
  pages = {386--399},
  year = 2013,
  month = sep,
  url = {publis/2013_rv.pdf},
  abstract = {A tutorial about the Frama-C plug-in E-ACSL.}
}
@inproceedings{sarssi13,
  author = {Mounir Assaf and
               Julien Signoles and
               Éric Totel and
               Frédéric Tronel},
  title = {Moniteur hybride de flux d'information pour un langage 
               supportant des pointeurs},
  booktitle = {{Conférence sur la Sécurité des Architectures Réseaux et des Systèmes d'Information (SARSSI'13).}},
  year = 2013,
  month = sep,
  note = {In French. Mounir Assaf won the conference's best student paper 
award for this paper.},
  url = {publis/2013_sarssi.pdf},
  abstract = {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.}
}
@inproceedings{sec13,
  author = {Mounir Assaf and
               Julien Signoles and
               Éric Totel and
               Frédéric Tronel},
  title = {Program Transformation for Non-interference Verification on 
               Programs with Pointers},
  booktitle = {{International Information Security and Privacy Conference (SEC'13)}},
  pages = {231--244},
  year = 2013,
  month = jul,
  publisher = {Springer},
  note = {Mounir Assaf won the conference's best student paper award for this paper.},
  url = {publis/2013_sec.pdf},
  abstract = {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.}
}
@inproceedings{tap13,
  author = {Nikolaï Kosmatov and Virgile Prevosto and Julien Signoles},
  title = {A Lesson on Proof of Programs with {Frama-C}},
  booktitle = {International Conference on Tests and Proofs (TAP'13)},
  note = {Invited Tutorial Paper},
  abstract = {A tutorial about the Frama-C plug-in Jessie.},
  year = 2013,
  month = jun,
  url = {publis/2013_tap.pdf}
}
@inproceedings{sac13,
  author = {Mickaël Delahaye and Nikolaï Kosmatov and Julien Signoles},
  title = {Common Specification Language for Static and Dynamic Analysis of 
           {C} Programs},
  booktitle = {Symposium on Applied Computing ({SAC'13})},
  publisher = {ACM},
  year = 2013,
  month = mar,
  pages = {1230--1235},
  url = {publis/2013_sac.pdf},
  abstract = {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.
}
}
@inproceedings{sefm12,
  author = {Cuoq, Pascal and Kirchner, Florent and Kosmatov, Nikolai and
 Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
  title = {Frama-C: a software analysis perspective},
  booktitle = {International Conference on Software Engineering and Formal
 Methods (SEFM'12)},
  year = {2012},
  month = oct,
  pages = {233--247},
  numpages = {15},
  publisher = {Springer},
  url = {publis/2012_sefm.pdf},
  abstract = {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.}
}
@inproceedings{fmics12,
  title = {{Combining Analyses for C Program Verification}},
  author = {Correnson, Loïc and Signoles, Julien},
  booktitle = {Formal Methods for Industrial Case Studies (FMICS'12)},
  editor = {Stoelinga, Mariëlle and Pinger, Ralf},
  pages = {108-130},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 7437,
  year = 2012,
  month = aug,
  url = {publis/2012_fmics.pdf},
  abstract = {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.}
}
@inproceedings{ml11,
  author = {Pascal Cuoq and Damien Doligez and Julien Signoles},
  title = {Lightweight typed customizable unmarshaling},
  booktitle = {Workshop on ML (ML'11)},
  year = 2011,
  month = sep,
  publisher = {ACM},
  url = {publis/2011_ml.pdf},
  abstract = {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.
}
}
@inproceedings{jfla11,
  title = {{Une bibliothèque de typage dynamique en OCaml}},
  author = {Julien Signoles},
  booktitle = {Journées Francophones des Langages Applicatifs (JFLA'11)},
  year = 2011,
  note = {In French},
  series = {Studia Informatica Universalis},
  url = {publis/2011_jfla.pdf},
  abstract = {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.
}
}
@inproceedings{ertss10,
  title = {{Taster, a Frama-C plug-in to enforce Coding Standards}},
  author = {David Delmas and Stéphane Duprat and Victoria Moya-Lamiel and 
                Julien Signoles},
  booktitle = {{Embedded Real-Time Software and Systems Congress (ERTSS'10)}},
  year = 2010,
  url = {publis/2010_ertss.pdf},
  abstract = {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.}
}
@inproceedings{icfp09,
  title = {Experience report: OCaml for an industrial-strength static analysis framework.},
  author = {Cuoq, Pascal and Signoles, Julien and Baudin, Patrick and Bonichon, Richard and Canet, Géraud and Correnson, Loïc and Monate, Benjamin and Prevosto, Virgile and Puccetti, Armand},
  booktitle = {International Conference of Functional Programming (ICFP'09)},
  editor = {Hutton, Graham and Tolmach, Andrew P.},
  pages = {281-286},
  publisher = {ACM},
  year = 2009,
  month = sep,
  url = {publis/2009_icfp.pdf},
  abstract = {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.
}
}
@inproceedings{jfla09,
  title = {{Foncteurs impératifs et composés: la notion de projet dans 
               Frama-C}},
  author = {Julien Signoles},
  booktitle = {Journées Francophones des Langages Applicatifs (JFLA'09)},
  year = 2009,
  month = sep,
  note = {In French},
  editor = {Alan Schmitt},
  pages = {245-280},
  series = {Studia Informatica Universalis},
  volume = {7.2},
  url = {publis/2009_jfla.pdf},
  abstract = {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.
}
}
@inproceedings{trust08,
  title = {Slicing for Security of Code},
  author = {Benjamin Monate and Julien Signoles},
  booktitle = {TRUST},
  editor = {Peter Lipp and Ahmad-Reza Sadeghi and Klaus-Michael Koch},
  pages = {133--142},
  publisher = {Springer-Verlags},
  series = {Lecture Notes in Computer Science},
  volume = {4968},
  year = {2008},
  month = mar,
  url = {publis/2008_trust.pdf},
  abstract = {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, 
\emph{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 \emph{slicing}. 
Slicing transforms a source code into an equivalent one according to a set of criteria.
We show that existing slicing criteria do \emph{not} preserve the confidentiality
of information. We introduce a new automatic and correct source-to-source
method properly preserving the confidentiality of information \emph{i.e.}
confidentiality is guaranteed to be exactly the same in the original program
and in the sliced program.}
}
@inproceedings{tfp07,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien 
              Signoles},
  title = {Designing a Generic Graph Library using {ML} Functors},
  booktitle = {{Trends in Functional Programming (TFP'07)}},
  year = 2007,
  month = apr,
  url = {publis/2007_cfp.ps.gz},
  abstract = {This article details the design and implementation of 
\textsc{Ocamlgraph}, a highly generic graph library for the programming 
language \textsc{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
\textsc{Ocamlgraph} algorithm (resp. data structure). Genericity is obtained 
through massive use of the \textsc{OCaml} module system and its functions, 
the so-called \emph{functors}.
}
}
@phdthesis{signoles06phd,
  author = {Julien Signoles},
  title = {Extension de {ML} avec raffinement: syntaxe, 
              sémantiques et système de types},
  year = 2006,
  month = jul,
  school = {Universit\'e Paris-Sud, Orsay, France},
  note = {In French},
  url = {publis/2006_phd.ps.gz},
  abstract = {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 \emph{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.
}
}
@techreport{signoles06semrfn,
  author = {Julien Signoles},
  title = {{Towards a ML Extension with Refinement: a Semantic Issue}},
  year = 2006,
  month = mar,
  institution = {LRI, University of Paris Sud},
  number = 1440,
  url = {publis/2006_report.pdf},
  abstract = {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.
}
}
@inproceedings{cfs05jfla,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre and Julien 
               Signoles},
  title = {Le foncteur sonne toujours deux fois},
  booktitle = {{Journ\'ees Francophones des Langages Applicatifs (JFLA'05)}},
  year = 2005,
  month = mar,
  note = {In French},
  url = {publis/2005_jfla.ps.gz},
  abstract = {Cet article présente \textsc{Ocamlgraph}, une bibliothèque 
générique de graphes pour le langage de programmation \textsc{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'\textsc{OCaml} et 
notamment de ses fonctions, les foncteurs.
}
}
@inproceedings{signoles05jfla,
  author = {Julien Signoles},
  title = {Une approche fonctionnelle du mod\`ele vue-contr\^oleur},
  booktitle = {{Journ\'ees Francophones des Langages Applicatifs (JFLA'05)}},
  year = 2005,
  month = mar,
  note = {In French},
  url = {publis/2005_jfla_2.ps.gz},
  abstract = {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 {\oe}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 {\oe}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.
}
}
@inproceedings{signoles03jfla,
  author = {Julien Signoles},
  title = {Calcul statique des applications de modules param\'etr\'es},
  booktitle = {{Journ\'ees Francophones des Langages Applicatifs (JFLA'03)}},
  year = 2003,
  month = jan,
  note = {In French},
  url = {publis/2003_jfla.ps.gz},
  abstract = {Le système de module d'{\emph 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.
}
}
@phdthesis{signoles02dea,
  author = {Julien Signoles},
  title = {Calcul statique des applications de foncteurs en 
              pr{\'e}sence d'effets de bord},
  type = {M\'emoire de {DEA}},
  year = 2002,
  month = sep,
  school = {Universit\'e Paris-Sud, Orsay, France},
  note = {In French},
  url = {publis/2002_dea.ps.gz},
  abstract = {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 <>. Cependant, utiliser (<>) 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 \emph{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.
}
}
@manual{eacsl,
  author = {Julien Signoles},
  title = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.8},
  year = 2014,
  month = mar,
  pdf = {http://frama-c.com/download/e-acsl/e-acsl.pdf}
}
@manual{eacsl-implem,
  author = {Julien Signoles},
  title = {E-ACSL Version 1.8. 
            Implementation in Frama-C Plug-in E-ACSL version 0.4},
  year = 2014,
  month = mar,
  pdf = {http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}
}
@manual{eacsl-manual,
  author = {Julien Signoles},
  title = {E-ACSL User Manual},
  year = 2014,
  month = mar,
  pdf = {http://frama-c.com/download/e-acsl/e-acsl-manual.pdf}
}
@manual{framac,
  title = {Frama-C User Manual},
  author = {Loïc Correnson and Pascal Cuoq and Florent Kirchner and 
Virgile Prevosto and Armand Puccetti and Julien Signoles and Boris Yakobowski},
  year = {2014},
  month = mar,
  pdf = {http://frama-c.com/download/user-manual.pdf}
}
@manual{plugin-dev-guide,
  author = {Julien Signoles and Loïc Correnson and Virgile Prevosto},
  title = {{Frama-C} Plug-in Development Guide},
  year = 2014,
  month = mar,
  pdf = {http://frama-c.com/download/plugin-developer.pdf}
}
@manual{rte,
  author = {Philippe Herrmann and Julien Signoles},
  title = {Annotation generation: {Frama-C}'s {RTE} plug-in},
  year = 2014,
  month = mar,
  pdf = {http://frama-c.com/download/frama-c-rte-manual.pdf}
}