activity
20152019
most citedHypercollecting Semantics and its Application to Static Analysis of Information Flow

25 citations · 30 across the 4 of their papers we have counts for

collaborators

5 papers

cs.SE2019

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…

cs.SE2018

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…

cs.PL2017★ 1 cited

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.…

cs.PL2016★ 25 cited

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…

cs.SE2015★ 4 cited

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…