[TYPES/announce] Call for Book Chapters: Guide to Software Verification with Frama-C

[Julien Signoles]

Call for Book Chapters


  Book Title:Guide to Software Verification with Frama-C. Core
  Components, Usages, and Applications.

Edited book to be published by Springer

Editors:Nikolai Kosmatov, Virgile Prevosto, Julien Signoles


      Description

This book aims at presenting Frama-C, an open source platform for 
analyzing C source code. It fosters collaborations between various 
techniques, by letting individual analyzers exchange information about 
the properties they can handle. In a similar manner, the platform is 
meant to be easily extensible, in particular, by third-party developers. 
Finally, Frama-C is aimed at being usable by software engineers that are 
not necessarily experts in formal methods. This implies providing as 
much automation as possible, as well as assessing the performances of 
the platform on real-world case studies. The purpose of this book is to 
provide a panorama of the platform, its core components, its usages, and 
its applications.

Frama-C is not a single tool, but a framework that groups together 
several tools. Each tool is provided as a plug-in. Roughly speaking, the 
plug-ins distributed with the platform can be decomposed in the 
following broad categories:

  *

    verification plug-ins;

  *

    plug-ins supporting the verification process;

  *

    plug-ins for better understanding the analyzed code;

  *

    plug-ins for simplifying the analyzed code;

  *

    plug-ins for extending the expressiveness of other analyzers.


Many industries in various domains rely on Frama-C to ensure safety 
and/or security of their critical applications. The extensibility of the 
platform allowed industrial engineers and tool developers to abstract 
from the groundwork of code parsing and data structure design, and to 
focus on new forms of verification.


      Target Audience

This book targets a large audience of readers interested in software 
verification and validation. They include industrial practitioners 
interested in verification of specific software products or development 
of new verification tools. They also include evaluation and 
certification authorities working on certification of critical software. 
Finally, this book will provide a helpful source of information to 
university professors and students taking courses in software analysis 
and verification.


As a preliminary background, the book will assume only a basic knowledge 
of the C programming language. In particular, the readers will not need 
to be familiar with Formal Methods.


      Information for authors

Authors are invited to submit chapter proposals related to Frama-C on 
the following (non-exhaustive) list of topics:

  *

    core verification techniques,

  *

    advanced usages,

  *

    combination of analysis techniques,

  *

    case studies and industrial applications,

  *

    emerging domains.

A chapter is expected to contain around 20-30 pages. The chapters will 
be blind-reviewed. Whenever possible, authors should try to make 
chapters self-contained.


      Submission

The authors will be asked to use the Springer Latex Template. Precise 
instructions on the Latex template and formatting will be communicated 
later.


      Important dates

  *

    Declaration of intention by the authors with an abstract of a few
    lines: at your earliest convenience, ideally before July 15, 2021

  *

    Chapter Submission deadline: November 1st, 2021

  *

    Notification: February 1, 2022

  *

    Final submission: September 1, 2022

  *

    Expected publication by Springer: End of 2022


      Contact Information

Email: nikolaikosmatov at gmail.com <mailto:nikolaikosmatov at gmail.com>, 
virgile.prevosto at cea.fr <mailto:virgile.prevosto at cea.fr>, 
julien.signoles at cea.fr <mailto:julien.signoles at cea.fr>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210701/7f2b2e7b/attachment-0001.htm>