Publications (5)
Abstract Compilation for Verification of Numerical Accuracy Properties
Maxime Jacquemin, Fonenantsoa Maurica, Nikolai Kosmatov +2
Verification of numerical accuracy properties in modern software remains an important and challenging task. This paper describes an original framework combining different solutions…
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
Mounir Assaf, David A. Naumann, Julien Signoles +2
We show how static analysis for secure information flow can be expressed and proved correct entirely within the framework of abstract interpretation. The key idea is to define a Ga…
Software Architecture of Code Analysis Frameworks Matters: The Frama-C Example
Julien Signoles
Implementing large software, as software analyzers which aim to be used in industrial settings, requires a well-engineered software architecture in order to ease its daily developm…
A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
César Sánchez, Gerardo Schneider, Wolfgang Ahrendt +13
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…
Context Generation from Formal Specifications for C Analysis Tools
Michele Alberti, Julien Signoles
Analysis tools like abstract interpreters, symbolic execution tools and testing tools usually require a proper context to give useful results when analyzing a particular function.…