Coconut

Design and verification of modern embedded platforms are two highly related problems which are still mainly addressed by using unrelated methodologies. This effectively reduces development productivity and complicates achieving predictable system properties.

The COCONUT project thus focuses on the definition of a formal framework based on a tight integration of design and verification through all refinement steps of an embedded platform design flow, from specifications to logic synthesis and software compilation. In particular, it is intended to propose a modelling and verification flow to enhance and speed-up embedded platform design and configuration with particular regard to application fields related to mixed continuous/discrete models, like for example networked multimedia and sensor network managing.

Coconut is funded by the European Commission as an FP7 STReP.

Publications

Proceedings
2010	Roderick Paul Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger, Barbara Jobstmann - "Robustness in the Presence of Liveness" - Computer Aided Verification
2010	Roderick Paul Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan, Richard Seeber - "RATSY - A new Requirements Analysis Tool with Synthesis" - Computer Aided Verification
2009	Roderick Paul Bloem, Karin Greimel, Thomas Henzinger, Barbara Jobstmann - "Synthesizing Robust Systems" - Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009
2009	Robert Könighofer, Georg Hofferek, Roderick Paul Bloem - "Debugging Formal Specifications Using Simple Counterstrategies" - Proceedings of 9th International Conference 2009 Formal Methods in Computer Aided Design FMCAD 2009
2009	Roderick Paul Bloem, Krishnendu Chatterjee, Thomas Henziger, Barbara Jobstmann - "Better Quality in Synthesis through Quantitative Objectives"
2008	Karin Greimel, Roderick Paul Bloem, Barbara Jobstmann, Moshe Vardi - "Open Implication" - Automata, Languages and Programming - ICALP 2008
2008	Ronald Tögl, Georg Hofferek, Karin Greimel, Adrian Leung, Raphael C-W. Phan, Roderick Paul Bloem - "Formal Analysis of a TPM-Based Secrets Distribution and Storage Scheme" - International Symposium on Trusted Computing (TrustCom 2008) Proceedings, in 9th ICYCS Conference Proceedings

Article
2011	Robert Könighofer, Georg Hofferek, Roderick Paul Bloem - "Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies" - International journal on software tools for technology transfer (Volume: ) (Note: to appear)

Tech report
2010	Graziano Pravadelli, Franco Fummi, Florian Letombe, Georg Hofferek, Giovanni Perbellini, Marco Roveri, Christophe Hui-Bon-Hoa, Wolfgang Müller, Samuel Dellacherie - "Final report"
2010	Florian Letombe, Georg Hofferek, Graziano Pravadelli, Giovanni Perbellini, Marco Roveri, Iman Narasamdya, Christophe Hui-Bon-Hoa, Rob Quigley, Markus Becker, Wolfgang Müller, Samuel Dellacherie, Franco Fummi - "Future plan on use and dissemination"
2010	Samuel Dellacherie, Georg Hofferek, Graziano Pravadelli, Davide Bresolin, Nicola Bombieri, Luigi Di Guglielmo, Luca Geretti, Tiziano Villa, Giovanni Perbellini, Marco Roveri, Iman Narasamdya, Rob Quigley, Joao Marques-Silva, Florian Letombe, Wolfgang Müller, Markus Becker, Christophe Hui-Bon-Hoa - "Final validation of the COCONUT flow and Tools Integration"

Presentation
2010	Robert Könighofer - "RATSY - A New Requirements Analysis Tool with Synthesis" (CAV 2010, Edinburgh, 18.07.10)
2010	Georg Hofferek - "Controller Synthesis Using Uninterpreted Functions" (Synthesis, Verification, and Analysis of Rich Models (SVARM 2010), 20.07.10)
2009	Robert Könighofer, Georg Hofferek, Roderick Paul Bloem - "Debugging Unrealizable Specifications Using Simple Counterstrategies" (Workshop on Games for Design, Verification and Synthesis (GASICS), Grenoble, 28.06.09)
2008	Ronald Tögl - "Formal Analysis of a TPM-Based Secrets Distribution and Storage Scheme" (International Symposium on Trusted Computing (TrustCom 2008), Zhang Jia Jie, 21.11.08)