Julien Signoles

Maxime Jacquemin, Fonenantsoa Maurica, Nikolai Kosmatov et al.

Verification of numerical accuracy properties in modern software remains an important and challenging task. This paper describes an original framework combining different solutions for numerical accuracy. First, we extend an existing runtime verification tool called E-ACSL with rational numbers to monitor accuracy properties at runtime. Second, we present an abstract compiler, FLDCompiler, that performs a source-to-source transformation such that the execution of the resulting program, called an abstract execution, is an abstract interpretation of the initial program. Third, we propose an instrumentation library FLDLib that formally propagates accuracy properties along an abstract execution. While each of these solutions has its own interest, we emphasize the benefits of their combination for an industrial setting. Initial experiments show that the proposed technique can efficiently and soundly analyze the accuracy of industrial programs by restricting the analysis on thin numerical scenarios.

César Sánchez, Gerardo Schneider, Wolfgang Ahrendt et al.

Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.