BUGSENG at IWES-2019 Workshop in Naples
We are happy to announce that our CTO Roberto Bagnara will be giving two presentations (see the abstracts below) at the fourth Italian Workshop on Embedded Systems (IWES), which will take place from September 30th to October 1st in Naples.
The Italian Workshop on Embedded Systems (IWES) is a meeting point for the exchange of research experience in academy and industry on all aspects of embedded systems.
ECLAIR: A Static Analysis Platform for the Verification of Critical Embedded Systems
ECLAIR is a framework for static analysis especially targeted at the verification of critical embedded system's software written in C and C++.
Some peculiarities of such programming languages, joined to the criticality of the software to be analyzed, required the solution of a number of technical and practical problems.
Challenges that had to be faced include:
- the implementation-defined behaviors of C and C++;
- the preprocessing phases of the compilation of C and C++ to machine language;
- sub-specification of floating-point arithmetic and of related mathematical libraries.
All these make it hard to ensure that static analysis results are relevant to the software that is actually embedded in the devices. At the same time, criticality makes it imperative that such a
connection is established in a reliable way, ruling out, to the extent this is possible, human errors and unsound approximations in the analysis software.
In this talk we describe the above mentioned issues and the solutions we incorporated into the ECLAIR analysis framework.
BUGSENG: Software Verification Done Right
BUGSENG, a spin-off company of the University of Parma, is built on 25 years of research on methodologies and techniques for automated software analysis and verification.
The main product developed by BUGSENG is ECLAIR, a powerful, flexible and extensible framework for the analysis of C, C++ and Java source and Java bytecode. Among its many applications we have: automatic detection of violations of coding rules included in popular coding
standards, such as MISRA C and MISRA C++; automatic detection of bugs and weaknesses that can lead to crashes, misbehaviors and security vulnerabilities; automatic generation of test cases.
ECLAIR design is based on solid scientific research results and on the best practices of software development and verification.
BUGSENG provides a full range of services related to software verification, including verification of customer code, definition of internal coding standards and realization of the corresponding automatic checkers, software audit reviews, training.
BUGSENG has offices in Parma and near Pisa, Italy.
We look forward to see you in Naples!