Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] 2-year Postdoc Position on Frama-C/E-ACSL
- Subject: [Frama-c-discuss] 2-year Postdoc Position on Frama-C/E-ACSL
- From: Julien.Signoles at cea.fr (Julien Signoles)
- Date: Thu, 15 Nov 2018 12:26:29 +0100
Hello, The Software Reliability and Security Lab at CEA LIST (Paris Saclay, France) is hiring a 2-year postdoctoral researcher to improve the Frama-C runtime verification plug-in E-ACSL. Frama-C is an opensource framework providing several analyzers for C code. The analyzed programs can be annotated by formal specifications written in the ACSL specification language. E-ACSL is one of the existing Frama-C analyzers. It converts ACSL annotations into C code in order to verify their validity at runtime, when the program is being executed. The goal of this postdoctoral position is twofolds: on the one hand, the postdoctoral researcher shall propose new compilation schemes to support additional ACSL constructs; on the other hand (s)he shall adapt existing compilation techniques or define new ones in order to optimize the generated code for reducing the time overhead and the memory footprint of the generated program. The work will be guided by and evaluated on case studies providing by a few of our academic and industrial partners. Knowledge in at least one of the following fields is required: - OCaml programming (at least, functional programming) - C programming - runtime verification - compilation - static analysis - semantics of programming languages - formal specification A full description of the position is available online: http://julien.signoles.free.fr/positions/postdoc-eacsl.pdf Feel free to contact me for additional details, Julien Signoles -- Researcher-engineer CEA LIST, Software Reliability and Security Lab tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles at cea.fr
- Prev by Date: [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- Next by Date: [Frama-c-discuss] a closer look on std::unique_copy
- Previous by thread: [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
- Next by thread: [Frama-c-discuss] a closer look on std::unique_copy