#	Pagina
attuale pagina	/open-h2020/projects/207194/index.html

Opendata, web and dolomites

VESSEDIA SIGNED

VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS

Total Cost €

EC-Contrib. €

Partnership

Views

Outcomes and
results

VESSEDIA project word cloud

Explore the words cloud of the VESSEDIA project. It provides you a very rough idea of what is the project "VESSEDIA" about.

contiki security benefits instance secure exponential extraction label methodology domain developers tackle brings fast individuals industries demonstrating standardisation forefront mostly iot modern safety exhaustive humans connect connected benefit validating technologies code threats live internet faults hacked risks toolbox smart platform ipv6 efficient critical phones vessedia generalising safe frama verified proposes world things source tools plan criteria certification software billions

Project "VESSEDIA" data sheet

The following table provides information about the project.

Coordinator	TECHNIKON FORSCHUNGS- UND PLANUNGSGESELLSCHAFT MBH Organization address address: BURGPLATZ 3A city: VILLACH postcode: 9500 website: www.technikon.at contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.
Coordinator Country	Austria [AT]
Project website	https://vessedia.eu/
Total cost	4˙192˙058 €
EC max contribution	4˙192˙058 € (100%)
Programme	1. H2020-EU.3.7. (Secure societies - Protecting freedom and security of Europe and its citizens) 2. H2020-EU.2.1.1. (INDUSTRIAL LEADERSHIP - Leadership in enabling and industrial technologies - Information and Communication Technologies (ICT))
Code Call	H2020-DS-LEIT-2016
Funding Scheme	RIA
Starting year	2017
Duration (year-month-day)	from 2017-01-01 to 2019-12-31

Partnership

Take a look of project's partnership.

#	participants	country	role	EC contrib. [€]
1	TECHNIKON FORSCHUNGS- UND PLANUNGSGESELLSCHAFT MBH TECHNIKON FORSCHUNGS- UND PLANUNGSGESELLSCHAFT MBH Organization address address: BURGPLATZ 3A city: VILLACH postcode: 9500 website: www.technikon.at contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	AT (VILLACH)	coordinator	343˙750.00
2	COMMISSARIAT A L ENERGIE ATOMIQUE ET AUX ENERGIES ALTERNATIVES COMMISSARIAT A L ENERGIE ATOMIQUE ET AUX ENERGIES ALTERNATIVES Organization address address: RUE LEBLANC 25 city: PARIS 15 postcode: 75015 website: www.cea.fr contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	FR (PARIS 15)	participant	1˙022˙887.00
3	FRAUNHOFER GESELLSCHAFT ZUR FOERDERUNG DER ANGEWANDTEN FORSCHUNG E.V. FRAUNHOFER GESELLSCHAFT ZUR FOERDERUNG DER ANGEWANDTEN FORSCHUNG E.V. Organization address address: HANSASTRASSE 27C city: MUNCHEN postcode: 80686 website: www.fraunhofer.de contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	DE (MUNCHEN)	participant	557˙750.00
4	SEARCH-LAB BIZTONSAGI ERTEKELO ELEMZO ES KUTATO LABORATORIUM KORLATOLT FELELOSSEGU TARSASAG SEARCH-LAB BIZTONSAGI ERTEKELO ELEMZO ES KUTATO LABORATORIUM KORLATOLT FELELOSSEGU TARSASAG Organization address address: SZERUSKERT UTCA 19 city: Budapest postcode: 1033 website: http://www.search-lab.hu contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	HU (Budapest)	participant	372˙500.00
5	DASSAULT AVIATION DASSAULT AVIATION Organization address address: 9 ROND POINT CHAMPS-ELYSEES-MARCEL DASSAULT city: PARIS postcode: 75008 website: www.dassault-aviation.com contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	FR (PARIS)	participant	366˙125.00
6	FUNDACION DEUSTO FUNDACION DEUSTO Organization address address: Avenida de las Universidades 24 city: Bilbao postcode: 48007 website: www.deusto.es contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	ES (Bilbao)	participant	352˙125.00
7	AMOSSYS SAS AMOSSYS SAS Organization address address: ALLEE DU BATIMENT 4 BIS city: RENNES postcode: 35000 website: n.a. contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	FR (RENNES)	participant	302˙500.00
8	INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE INSTITUT NATIONAL DE RECHERCHE ENINFORMATIQUE ET AUTOMATIQUE Organization address address: DOMAINE DE VOLUCEAU ROCQUENCOURT city: LE CHESNAY CEDEX postcode: 78153 website: www.inria.fr contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	FR (LE CHESNAY CEDEX)	participant	295˙952.00
9	TURUN AMMATTIKORKEAKOULU OY TURUN AMMATTIKORKEAKOULU OY Organization address address: JOUKAHAISENKATU 3A city: TURKU postcode: 20520 website: www.turkuamk.fi contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	FI (TURKU)	participant	293˙468.00
10	KATHOLIEKE UNIVERSITEIT LEUVEN KATHOLIEKE UNIVERSITEIT LEUVEN Organization address address: OUDE MARKT 13 city: LEUVEN postcode: 3000 website: www.kuleuven.be contact info title: n.a. name: n.a. surname: n.a. function: n.a. email: n.a. telephone: n.a. fax: n.a.	BE (LEUVEN)	participant	285˙000.00

Map

Project objective

The VESSEDIA project will bring safety and security to many new software applications and devices. In the fast evolving world we live in, the Internet has brought many benefits to individuals, organisations and industries. With the capabilities offered now (such as IPv6) to connect billions of devices and therefore humans together, the Internet brings new threats to the software developers and VESSEDIA will allow connected applications to be safe and secure. VESSEDIA proposes to enhance and scale up modern software analysis tools, namely the mostly open-source Frama-C Analysis platform, to allow developers to benefit rapidly from them when developing connected applications. At the forefront of connected applications is the IoT, whose growth is exponential and whose security risks are real (for instance in hacked smart phones). VESSEDIA will take this domain as a target for demonstrating the benefits of using our tools on connected applications. VESSEDIA will tackle this challenge by 1) developing a methodology that allows to adopt and use source code analysis tools efficiently and produce similar benefits than already achieved for highly-critical applications (i.e. an exhaustive analysis and extraction of faults), 2) enhancing the Frama-C toolbox to enable efficient and fast implementation, 3) demonstrating the new toolbox capabilities on typical IoT (Internet of Things) applications including an IoT Operating System (Contiki), 4) developing a standardisation plan for generalising the use of the toolbox, 5) contributing to the Common Criteria certification process, and 6) defining a label “Verified in Europe” for validating software products with European technologies such as Frama-C.

Deliverables

List of deliverables.
Inriaâ€™s use case intermediate report	Documents, reports	2020-04-14 23:39:22
Project quality plan	Documents, reports	2020-04-14 23:39:22
Data Management Plan (DMP)	Open Research Data Pilot	2020-04-14 23:39:22
Internal and external IT communication infrastructure and project website	Websites, patent fillings, videos etc.	2020-04-14 23:39:22
Basic analyzers intermediate release	Other	2020-04-14 23:39:22
Metrics for VESSEDIA tools in quality assurance	Documents, reports	2020-04-14 23:39:21
Updated plan and initial report on Exploitation, Dissemination & Communication activities	Documents, reports	2020-04-14 23:39:22
CEAâ€™s use case intermediate report	Documents, reports	2020-04-14 23:39:22
Modelling framework description	Documents, reports	2020-04-14 23:39:22
Risk Assessment Plan	Documents, reports	2020-04-14 23:39:22
DAâ€™s use case intermediate report	Documents, reports	2020-04-14 23:39:22
Security requirements for connected medium security-critical applications	Documents, reports	2020-04-14 23:39:21
VESSEDIA approach for security evaluation	Documents, reports	2020-04-14 23:39:21
Methodological report for modular reasoning for system validation and verification	Documents, reports	2020-04-14 23:39:21

Take a look to the deliverables list in detail: detailed list of VESSEDIA deliverables.

Publications

List of publications.
year	authors and title	journal	last update
2020	Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, Bart Jacobs The future is ours: prophecy variables in separation logic published pages: 1-32, ISSN: 2475-1421, DOI: 10.1145/3371113	Proceedings of the ACM on Programming Languages 4/POPL	2020-04-14
2018	Hoang Le, Viet; Correnson, LoÃ¯c; Signoles, Julien; Wiels, Virginie Verication Coverage for Combining Test and Proof published pages: , ISSN: , DOI: 10.5281/zenodo.3609494	International Conference on Tests and Proofs TAP 2018 (Pre-Print)	2020-04-14
2019	Ly, Dara; Kosmatov, Nikolai; Signoles, Julien; Loulergue, FrÃ©dÃ©ric Soundness of a Dataflow Analysis for Memory Monitoring. published pages: 97-108, ISSN: , DOI: 10.5281/zenodo.3609499	ACM SIGAda Ada Letters (Pre-print) Volume 38, Issue 2	2020-04-14
2019	Hamin Jafar; Jacobs Bart Transferring Obligations Through Synchronizations published pages: , ISSN: , DOI:	ECOOP	2020-04-14
2018	Blanchard, Allan; Kosmatov, Nikolai; Loulergue, FrÃ©dÃ©ric Des listes et leurs fantÃ´mes : vÃ©rification d\'un module critique de Contiki avec FRAMA-C published pages: , ISSN: , DOI:	17Ã¨mes JournÃ©es AFADL : Approches Formelles Dans L\'assistance Au DÃ©veloppement De Logiciels 14	2020-04-14
2018	Allan Blanchard, Nikolai Kosmatov, FrÃ©dÃ©ric Loulergue MMFilter : A CHR-Based Solver for Generation of Executions under Weak Memory Models published pages: 121-142, ISSN: 1477-8424, DOI: 10.1016/j.cl.2018.03.002	Computer Languages, Systems & Structures 53	2020-04-14
2017	Pariente, Dillon; Signoles, Julien Static Analysis and Runtime-Assertion Checking: Contribution to Security Counter-Measures published pages: , ISSN: , DOI: 10.5281/zenodo.820856		2020-04-14
2017	Peyrard , Alexandre; Kosmatov , Nikolai; Duquennoy , Simon; Raza , Shahid *Towards Formal Verification of Contiki: Analysis of the AESâ€“CCM Modules with Frama-C** published pages: , ISSN: , DOI: 10.5281/zenodo.1160349	RED-IOT 2018 - Workshop on Recent advances in secure management of data and resources in the IoT 4	2020-04-14
2017	Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prevosto Symbolic execution of transition systems with function summaries published pages: 41-58, ISSN: , DOI: 10.1007/978-3-319-61467-0_3	11th International Conference on Tests	2020-04-14
2018	Blanchard , Allan; Kosmatov , Nikolai; Loulergue , FrÃ©dÃ©ric Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C published pages: , ISSN: , DOI: 10.5281/zenodo.1402494	Tenth NASA Formal Methods Symposium - NFM 2018 1	2020-04-14
2017	Oliveira , S. ,; BENSALEM , S.; Prevosto , V. Synthesizing invariants by solving solvable loops published pages: , ISSN: 0302-9743, DOI: 10.5281/zenodo.893067	Automated Technology for Verification and Analysis (ATVA) 2	2020-04-14

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "VESSEDIA" project.

For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.

Send me an email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.

Thanks. And then put a link of this page into your project's website.

The information about "VESSEDIA" are provided by the European Opendata Portal: CORDIS opendata.