Abstract
This paper presents our results in the formal verification of kLIBC, a minimalistic C library, using the Frama-C/WP tool. We report how we were able to completely verify a significant number of functions from < string.h > and < stdio.h >. We discuss difficulties encountered and describe in detail a problem in the implementation of common < string.h > functions, for which we suggest alternative implementations. Our work shows that it is presently already viable to verify low-level C code, with heavy usage of pointers. Although the properties proved tend to be shallower as the code becomes of a lower-level nature, it is our view that this is an important direction towards real-world software verification, which cannot be attained by focusing on deep properties of cleaner code, written specifically to be verified.

Abstract
This work proposes an innovative method based on autoencoders to perform state estimation in distribution grids, which has as main advantage the fact of being independent of the network parameters and topology. The method was tested in a real low voltage grid (incorporating smart grid features), under different scenarios of smart meter deployment. Simulations were performed in order to understand the necessary requirements for an accurate distribution grid state estimator and to evaluate the performance of a state estimator based on autoencoders.

Abstract

Abstract
Interferometric fiber optic based sensors, namely those based on the Fabry-Perot (F-P) configuration seem very attractive for biomechanical and biomedical applications. The present study is focused on the proof of concept of two developed FP based sensors, for high and low pressure measurements of fluids. For low pressure sensor, it was used a polymeric diaphragm in a microstrutured fiber. It was obtained a good agreement between wavelength shift and the pressure, for the two tested sensors.

Abstract
Use case scenarios are known as powerful means for requirements specification. On the one hand, they join in the same modeling space the expectations of the stakeholders and the needs of the developers involved in the process. On the other hand, they describe the desired high level functionalities. By formalizing these descriptions we are able to extract relevant informations from them. Specifically, we are interested in identifying requirements patterns (common requirements with typical implementation solutions) in support for a requirements based software development approach. This paper addresses the transformation of use case descriptions expressed in a Controller Natural Language into an ontology expressed in the Web Ontology Language (OWL), as well as the query process for such information. It reports on a study aimed at validating our approach and our tool with real users. A preliminary set of results is discussed.

Abstract
Runtime verification is an emerging discipline that investigates methods and tools to enable the verification of program properties during the execution of the application. The goal is to complement static analysis approaches, in particular when static verification leads to the explosion of states. Non-functional properties, such as the ones present in real-time systems are an ideal target for this kind of verification methodology, as are usually out of the range of the power and expressiveness of classic static analyses. In this paper, we present a framework that allows real-time programs written in Ada to be augmented with runtime verification capabilities. Our framework provides the infrastructures which is needed to instrument the code with runtime monitors. These monitors are responsible for observing the system and reaching verdicts about whether its behavior is compliant with its non-functional properties. We also sketch a contract language to extend the one currently provided by Ada, with the long term goal of having an elegant way in which runtime monitors can be automatically synthesized and instrumented into the target systems. The usefulness of the proposed approach is demonstrated by showing its use for an application scenario.