Latest news

No news at this moment


Press Release

Commissariat à l’Energie Atomique, France

An Introduction to VeriFast for Java

Jochen Burghardt, Hans Werner Pohl

A Trusted Virtual Security Module

Ronald Toegl, Florian Reimair, Martin Pirker


Some deliverables are for public use and shall be made available for consultation on this web page once they are complete.


Deliverable name
D1.1 Security requirements and vulnerabilities
D1.2 Industrial and platform segmentation (click here for the related appendix)
D1.3 Vulnerability traces in C/C++ and Java code (Prototypes)
D1.4 Formal security properties (Prototypes)
D2.1 Specification of the common IRL for the C++ and Java languages, including an AST format and a formal specification language. (Prototypes)
D2.2 Specification of the methods for the verification of security properties of C, C++ and Java code (Cryptographic Protocols)
D3.1.2 Documentation and implementation of a Java front-end supporting classes and exceptions
D3.1.5 Validation report of the C++ and Java front-ends
D3.2.5 Validation report of the Frama-C and VeriFast analysis extensions
D4.1 C-code security analysis plug-ins and associated documentation (Prototypes)
D4.2.2 C++ and Java code security analysis plug and associated documentation
D5.4.1 Annotated code of the Single Sign On use case and associated documentation
D5.4.2 Annotated code of the Embedded TPM use case and associated documentation
D5.6.1 Report on Single Sign On use case analysis
D5.6.2 Report on the Embedded TPM use case analysis
D5.6.3 Report on the Software Upload use case analysis
D6.1.1 Report on the  STANCE security assessment approach for Security evaluation (Prototypes)
D6.1.2 Evaluation using the industrial use cases (Prototypes)
D6.2.1 Evaluation of the STANCE outcomes as support for a CC evaluation
D6.2.2 Assessment using the industrial use cases
D7.2 Communication Plan
D7.4 Preliminary Exploitation Plan
D7.7 Exploitation Plan
D7.8 Dissemination Report  (including copy of or link to dissemination material)
D7.9 White paper on the methods to verify security properties in software using static analysis tools
D7.10 Final project report