EIT Digital and static source code analysis

The EIT Digital organization is announcing its 2018 call for collaborative project proposal on march 17^th, 2017.

Your organization is considering joing a consortium to work on a proposal, in one of the Digital Wellbeing, Digital Finance, Digital Industry, Digital Infrastructure, Digital Cities topics of that call.

I (Basile Starynkevitch) am a research engineer in the software safety lab (Laboratoire de Sûreté des Logiciels) of CEA, LIST (the Information Technology focused institute, 800 persons, of CEA, a public applied research organization of 16000 persons in France).

The LSL lab (software safety laboratory) of CEA, LIST has expertise in static source code analysis, both in a formal methods approach through its flagship product Frama-C and in more heuristic approaches by leveraging on existing compilers like with GCC MELT, which is a domain specific language to work on GCC internal representations, or Clang/LLVM.

We are looking to join a consortium working on a proposal for EIT Digital. As soon as you have software source code for one of the topics (Digital Wellbeing, Digital Finance, Digital Industry, Digital Infrastructure, Digital Cities) relevant to that call, we propose to to develop a specialized tool (preferably open source, above existing technologies), for developers & engineers writing source code (in C, C++, and Ada if needed...) targeting that topic. We are considering contributing to a project by working in some (one or several) of these aspects:

If your domain (one of Digital Wellbeing, Digital Finance, Digital Industry, Digital Infrastructure, Digital Cities) has some common or (de-facto) standard application programming interface (or API, cf. note 1), we could develop a specialized tool (preferably open source, above existing technologies), for developers & engineers writing source code (in C, C++, and Ada or Go if needed...) targeting that domain and using that API. This tool could assist your domain's application software developer by analysing and checking the validity of the source code against coding rules, invariants, and good practices specific to these software frameworks and domains. Such a tool would work both on small and large software pieces.
If your domain contains safety critical cyber-physical software where cybersecurity threats are important (risking lives or large assets), we could develop a software proving tool using formal methods targeting your domain. This approach (related to proof assistants) is particularily suitable for critical small pieces of software (less than a few hundred thousands of source code lines; cf. note 2).
If your domain has an eco-system of legacy code with hundred of millions of lines (cf. note 3), we propose to adopt a big data or machine learning approach to develop a tool to help in several software engineering tasks: code retrieval, i.e. finding some piece of code related to some subject in a large set of software packages; code comprehension, i.e. helping the newbie software developer to use a big software library, cf. note 4; code verification, i.e. using machine learning techniques to help debugging and testing some piece of software.

We are also more broadly interested in bringing static source code analysis techniques to software developers on EIT Digital topics.

Feel free to contact me (basile.starynkevitch@cea.fr) and to forward this message (downloadable on http://starynkevitch.net/Basile/gcc-melt/EIT_Digital2017-interest-Starynkevitch.html) to your colleagues and partners.

I look forward to discussing with you.

Basile Starynkevitch,
mobile: +33 6 8501 2359; office: +33 1 6908 6595
CEA LIST Nano-Innov b862 PC 174 - 91191 GIF/YVETTE CEDEX, France
basile.starynkevitch@cea.fr

Notes

note 1: So an API is defined as a set of functions or abstract classes' declarations, e.g. in some C or C++ #include-ed header files or their equivalent in another programming language, etc...

note 2: We are of course well aware that formal methods (notably sound static analyzers) do not scale well to huge multi-million lines software, and may require expertise to be used. They are particularily suitable for development of small but costly critical software.

note 3: an example of eco-system of legacy code is the GENIVI alliance in the automotive sector. Other industrial domains have also such alliances, or are building them.

note 4: Quite often, a software developer has to use large infrastructure code (such as Qt GUI framework, the POSIX API, RDBMS libraries like libmysqlclient, computer vision libraries like OpenCV, and many other various industry-specific libraries or software components etc...) and mastering such libraries require years of work. We suggest to develop tools helping that effort.