25 citations · 45 across the 6 of their papers we have counts for
6 papers
Verification of High-Level Transformations with Inductive Refinement Types
Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar S. Dimovski +1
High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backt…
Skeletal Semantics and their Interpretations
Martin Bodin, Philippa Gardner, Thomas Jensen +1
The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge ef…
Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)
Martin Bodin, Thomas Jensen, Alan Schmitt
We present a technique for deriving semantic program analyses from a natural semantics specification of the programming language. The technique is based on a particular kind of sem…
Secure the Clones
Thomas Jensen, Florent Kirchner, David Pichardie
Exchanging mutable data objects with untrusted code is a delicate matter because of the risk of creating a data space that is accessible by an attacker. Consequently, secure progra…
Sawja: Static Analysis Workshop for Java
Laurent Hubert, Nicolas Barré, Frédéric Besson +5
Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when developing a full-fledged analyzer for a realistic langu…
Enforcing Secure Object Initialization in Java
Laurent Hubert, Thomas Jensen, Vincent Monfort +1
Sun and the CERT recommend for secure Java development to not allow partially initialized objects to be accessed. The CERT considers the severity of the risks taken by not followin…