Latest news

Stance Press Release


07/09/2016: Please click here to read the press release!

Read More

Frama-C Day 2016


In a society driven by information technologies and communication, the safety and security of software have become crucial challenges. Frama-C is a software analysis platform that enables the design, implementation, and dissemination of formal verification solutions.

Speakers at the Frama-C Day will demonstrate and discuss innovative approaches to software analysis, from both academic and industrial points of views.

In addition to invited presentations, this will be a space for community discussions, updates on new developments, and upcoming projects.

Click here for more details

Read More


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