From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id D74915D5 for ; Thu, 1 Jul 2021 13:39:14 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.83,314,1616454000"; d="scan'208,217";a="517764311" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 01 Jul 2021 15:39:11 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id AA681E0B0B; Thu, 1 Jul 2021 15:39:11 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 62752E0B0B for ; Thu, 1 Jul 2021 15:39:07 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=julien.signoles@gmail.com; spf=Pass smtp.mailfrom=julien.signoles@gmail.com; spf=None smtp.helo=postmaster@mail-lj1-f178.google.com IronPort-PHdr: =?us-ascii?q?A9a23=3AfpcZHx3LHCVi1skAsmDOcgQyDhhOgF0UFjAc5pd?= =?us-ascii?q?vsb9SaKPrp82kYBWOo64z0hSUAc3y0LFts6LuqafuWGgNs96qkUspV9hybSIDk?= =?us-ascii?q?tgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF?= =?us-ascii?q?5Ovn5FpTdgsiq0+2+4ZPebgRJiTayYb5/Iwi9oBnMuMURnYZsMLs6xAHTontPd?= =?us-ascii?q?eRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRb?= =?us-ascii?q?YUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpi?= =?us-ascii?q?CcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZUclfVyJPDIC?= =?us-ascii?q?hYYURE+UMJvxXo5XnqlYUsReyGQuhCeXywTFInH/22qg63vwlHwHb2AwgHswBs?= =?us-ascii?q?HLJp9voNacSXua1zK7MzTrddPNdxDDw6IrVchAloPGDQ7RwfdDKyUkuGAPFiFK?= =?us-ascii?q?QqYj7MDOOzekNvG2b4PBhVeKrkWIotwZxoj22y8oql4LGiZ4bxEre+iVl3IY6O?= =?us-ascii?q?8e4SEhjbNCrE5Zcqi+UOYt4TM4iXm1luDg3x6MatJO5cyUEyJAqyh7fZvGafYa?= =?us-ascii?q?F4BbuWfufLDp5hn9oZa6yihSs/UWj1OHxUNS/3lVSriddjNXAqnQA2wbQ58WHU?= =?us-ascii?q?Pdx4Fut1DWV2wzO6OxJIkY5nrfBJZE72L4/jJ8TvFzDHiDonEX2i7ebdkA+9ei?= =?us-ascii?q?p7+Tre7Hmpp2BO4NthAHyL6Yjl8+lDeQ3NQgOWGeb+eCi27H54UL5R7BKguU3k?= =?us-ascii?q?qnfrp/aOdwWqrClDwJRyIou6BayAy243NgEnnQLNk9JdRCEgoTxPlHBOvH4DfO?= =?us-ascii?q?xg1S2lzdrwujLPr/8ApXJL3jMjrHhcaxm605dxwozy9df55ZKBbEaO//zVUrxu?= =?us-ascii?q?8bZDh89KQC73+HnCNBl2oMERW2PGrOZML/VsVKQ+u0gOeyMZIsMtDb5Kvgl/OL?= =?us-ascii?q?ugGQimV4deKmpxYEYZGq5HvRgOUWZYGDjjs0PEWcQ7UICS7nBgViGGRpSfGr6C?= =?us-ascii?q?6k14zV+DIO9Ea/CQJqsifqPxnHoMIdRYzVkF1SNHHGgTISLXfAIZTnads18lj0?= =?us-ascii?q?JU/66SoAn0hWjryf1zrNmKqzf/ShO5sGr78R8++CGzUJ6zjdzFcnIljjVFwmce?= =?us-ascii?q?0sHQjY32OZ0pkkvkj9rPoB3hvVZEZpY4PYbC2/S1LbZxu1+TtTwA0fPJ4jZDlm?= =?us-ascii?q?hRdqiDHc6Sddjm7cz?= IronPort-HdrOrdr: =?us-ascii?q?A9a23=3ACGQnGK4MYa8VnVVznAPXwBjXdLJyesId70hD?= =?us-ascii?q?6qkRc3xom6mj/PxG88526faKskd2ZJhNo6H4BED4ewKlyXct2/h3AV7AZniFhI?= =?us-ascii?q?LXFu9fxK34wzPhHGn7+vRG3altU6UWMrzN5DFB5K7HCW+DYrUdKbK8n5xA692y?= =?us-ascii?q?854jd3APV4hQqyNwCgOaFQlbZCQuP/AE/CP23Lsjmwad?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CfAgD4w91gf7LQVdFaHQEBPAEFBQECA?= =?us-ascii?q?QkBgW4Cg3Y7MYRIgR6QU4pmkHAUgWgLAQMBDRIBLgQBAYFegnQCgnMCHQcBBDI?= =?us-ascii?q?HDgIEFQEBBQEBAQIBAwMEARMBAQ0LCwgnHIVoDYI4KQGDfAsGHQEbDw8DEhA0A?= =?us-ascii?q?wIjAQERAQUBCxcTIoUkAQMvmWyCHoEEPYsygRUFAReBAYIIBoUjChkoDWMDgVc?= =?us-ascii?q?CBxKBKAGFaYEdAQGBF4VxEIFVRIFLgjgFAm2CIIFvARIBV4JhgmQEgxMxSoFXD?= =?us-ascii?q?i4NOgwMkWYnixKHVoJNBZReLywHgyQEgScGC4taiyyFYCumIZERlDmJM4ZjE4U?= =?us-ascii?q?HECMSgXkFgRhwTSMvITGCOFAZDlaROYpgQi84AgYBCQEBAwmJMC2CGAEB?= X-IPAS-Result: =?us-ascii?q?A0CfAgD4w91gf7LQVdFaHQEBPAEFBQECAQkBgW4Cg3Y7MYR?= =?us-ascii?q?IgR6QU4pmkHAUgWgLAQMBDRIBLgQBAYFegnQCgnMCHQcBBDIHDgIEFQEBBQEBA?= =?us-ascii?q?QIBAwMEARMBAQ0LCwgnHIVoDYI4KQGDfAsGHQEbDw8DEhA0AwIjAQERAQUBCxc?= =?us-ascii?q?TIoUkAQMvmWyCHoEEPYsygRUFAReBAYIIBoUjChkoDWMDgVcCBxKBKAGFaYEdA?= =?us-ascii?q?QGBF4VxEIFVRIFLgjgFAm2CIIFvARIBV4JhgmQEgxMxSoFXDi4NOgwMkWYnixK?= =?us-ascii?q?HVoJNBZReLywHgyQEgScGC4taiyyFYCumIZERlDmJM4ZjE4UHECMSgXkFgRhwT?= =?us-ascii?q?SMvITGCOFAZDlaROYpgQi84AgYBCQEBAwmJMC2CGAEB?= X-IronPort-AV: E=Sophos;i="5.83,314,1616454000"; d="scan'208,217";a="517764281" X-MGA-submission: =?us-ascii?q?MDEmh9ufaIeOzh48Bjkh7I6mFyhA6+TSHzeL9E?= =?us-ascii?q?tK8d913eifFHNWblu6QIizaTcxOKSeoUYPnDsHK5cS4R1aHyQ07NeWfA?= =?us-ascii?q?PEG/WwzpsL4u71WhBFWN38alxd06jeIvZcg0aCG3vCI0S1VFJbocC1jz?= =?us-ascii?q?SUBCx5B4Hboj8JHo6hmaI7xw=3D=3D?= Received: from mail-lj1-f178.google.com ([209.85.208.178]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 01 Jul 2021 15:39:06 +0200 Received: by mail-lj1-f178.google.com with SMTP id d25so8494004lji.7 for ; Thu, 01 Jul 2021 06:39:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=/3Zz55my+YX73ZUTN8QTeYPVAvgZEuQbb/fd40yVHBc=; b=cC02DlfXO4EfdvJ2kshYK2UaKWJD0IY+3AfvOcHA7YKgmDUg2P/kjhFPmrAQfjdYym y9b0jqkaJHmrctThhQvFOUqmW9bsv0F3J6qXhOLcV+40mATIXg7plfgZG7Aa1hN6E2mQ d8rZqilm4T9fbYoYVq31SUHevEkPlRBVb+A5h3ea25mUffs9MCou21Fr38L7rj3RCCDW pgHhjKRL2o0P6dpRRSjonrzKyGd1qvIbblneEL6uYk/NyfZxR84TKgQPh3vLnhDIvrHC u6KYvD7erL1bkzYiuIKLSmVG+rgNNVOR9RGnOYimqQfVbcHvK3yVgNac+VsQJBa10W2c 2SUw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=/3Zz55my+YX73ZUTN8QTeYPVAvgZEuQbb/fd40yVHBc=; b=UiVL0CvkEjE6Z4WV2ae25SElaQoyeWEZ5CA8nBrIcjBva3Cxx/Tn7h9Fb6QdTN3Aqf Psk/bZk+En0si3Amxz5yRwAhSxlgfw7kxiCKwwBdHEdwRoF6+FDohlVvTbeB9JDXFRtV 8MhgJ3MgMppMrlgw4jeWzAoIIZXQgdsq0IK8yVqdTTnogEHmfQ1/kluF1SQ3pPnnzwx8 W0q70xkA7cdOz0jhAb0RbgJ86H1eQSw0VdL3gtzhzj3XAp/5doWHi1r/8v1jn0j1C/Jf 00oxHPbls+Pg7SZ/HoAfZWNPUQFqTHDldUZFHlB/5QLaeyC2TLd0puKoCJpdko91r6zU 6yNA== X-Gm-Message-State: AOAM530CADYIY3fBY4CkJ+GQ++PQUk7SXlVXP1Q7jiBOS79fr2JDqnuz NkUryP2nQwqYv47I5wODuzLE53+2sy8NXxPVilWdwa8vYzCP2w== X-Google-Smtp-Source: ABdhPJwkbKaFoSE87axGo6l/k9XlffYrUBAL9gJQMsSCNdOR3Uq7HysLO7irqRydigmFCHsiXxzgFZ3+ia3bgr4wXIw= X-Received: by 2002:a05:651c:1507:: with SMTP id e7mr12254548ljf.9.1625146743956; Thu, 01 Jul 2021 06:39:03 -0700 (PDT) MIME-Version: 1.0 From: Julien Signoles Date: Thu, 1 Jul 2021 15:38:53 +0200 Message-ID: To: Caml List Content-Type: multipart/alternative; boundary="00000000000061a8a505c60ff6ee" Subject: [Caml-list] Call for Book Chapters: Guide to Software Verification with Frama-C Reply-To: Julien Signoles X-Loop: caml-list@inria.fr X-Sequence: 18535 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: --00000000000061a8a505c60ff6ee Content-Type: text/plain; charset="UTF-8" *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@gmail.com , virgile.prevosto@cea.fr , julien.signoles@cea.fr --00000000000061a8a505c60ff6ee Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Call for Book Chapters

Book Title: Guide to Software Verification with Frama-C. Core Compon= ents, 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=20 analyzing C source code. It fosters collaborations between various=20 techniques, by letting individual analyzers exchange information about=20 the properties they can handle. In a similar manner, the platform is=20 meant to be easily extensible, in particular, by third-party developers.=20 Finally, Frama-C is aimed at being usable by software engineers that are=20 not necessarily experts in formal methods. This implies providing as=20 much automation as possible, as well as assessing the performances of=20 the platform on real-world case studies. The purpose of this book is to=20 provide a panorama of the platform, its core components, its usages, and=20 its applications.

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

=C2=A0* verification plug-ins;
=C2=A0* plug-ins supporting the verification process;
=C2=A0* plug-ins for better understanding the analyzed code;
=C2=A0* plug-ins for simplifying the analyzed code;
=C2=A0* plug-ins for extending the expressiveness of other analyzers.

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

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

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

Information for authors
Authors are invited to submit chapter proposals related to Frama-C = on=20 the following (non-exhaustive) list of topics:
=C2=A0* core verification techniques,
=C2=A0* advanced usages,
=C2=A0* combination of analysis techniques,
=C2=A0* case studies and industrial applications,
=C2=A0* emerging domains.
A chapter is expected to contain around 20-30 pages. The chapters will=20 be blind-reviewed. Whenever possible, authors should try to make=20 chapters self-contained.

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

Important dates
=C2=A0* Declaration of intention by the authors with an abstract of a few
=C2=A0=C2=A0 lines: at your earliest convenience, ideally before July 1= 5, 2021
=C2=A0* Chapter Submission deadline: November 1st, 2021
=C2=A0* Notification: February 1, 2022
=C2=A0* Final submission: September 1, 2022
=C2=A0* Expected publication by Springer: End of 2022

=C2=A0Contact Information
Email: nikolaikosmatov@gmail.com <mailto:= nikolaikosmatov@gmail.com>,=20 virgile.prevosto@cea.fr <mailto:virgile.prevosto@cea.= fr>,=20 julien.signoles@cea.fr <mailto:julien.signoles@cea.fr&g= t;

--00000000000061a8a505c60ff6ee--