caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] Call for Book Chapters: Guide to Software Verification with Frama-C
@ 2021-07-01 13:38 Julien Signoles
  0 siblings, 0 replies; only message in thread
From: Julien Signoles @ 2021-07-01 13:38 UTC (permalink / raw)
  To: Caml List

[-- Attachment #1: Type: text/plain, Size: 3711 bytes --]

*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

 * 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

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

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

*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: <>
<> <>, <>

[-- Attachment #2: Type: text/html, Size: 4602 bytes --]

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2021-07-01 13:39 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-07-01 13:38 [Caml-list] Call for Book Chapters: Guide to Software Verification with Frama-C Julien Signoles

caml-list - the Caml user's mailing list

This inbox may be cloned and mirrored by anyone:

	git clone --mirror
	git clone --mirror

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V1 caml-list caml-list/ \
	public-inbox-index caml-list

Example config snippet for mirrors.
Newsgroup available over NNTP:

AGPL code for this site: git clone