Formal Methods for Design & Verification
We study the use of formal methods for the design and verification of systems. Such systems may consist of hardware, software, or both, as in the case of Embedded Systems or Systems on Chip.
We are part of the Secure and Correct Systems (SCoS) Group at IAIK.
More about SCoS »In the context of model checking, we look at the connections between temporal logics such as PSL and finite automata on infinite words. We also study the question of requirements analysis, i.e., of making sure that a specification is correct. One way to do this is to automatically generate and explain scenarios that satisfy (or violate) a given specification. We are also looking at alternative specification methods for properties that are hard to formulate.
When a system has a fault, we want to help the user to fix it. Thus, we consider the questions of automatic fault localization and automatic repair. For the former we employ model-based diagnosis, the latter problem is solved using game theory.
Finally, we think that it should be enough to specify a system. The implementation can be derived automatically using property synthesis. We study how to make synthesis efficient and how to assist the user to design a system by specification.
ARiSE
We are part of the association Austrian Rigorous Systems Engineering (ARiSE), which was founded in 2010 to further the research in formal methods for the design of correct computer systems. It brings together top researchers in formal methods in Austria in order to foster collaboration and a common research platform.
More information about ARiSE is available on the ARiSE webiste http://www.arise.or.at/.
People
Former Members:
- Karin Greimel (NXP)
- Andreas Griesmayer (UNU-ist)
- Barbara Jobstmann (VERIMAG)
- Ingo Pill (TU Graz)
- Stefan Staber (Onespin Solutions)
Projects
We are/were involved in the following projects.
Publications
| Proceedings | ||||
|---|---|---|---|---|
| 2013 | Ayrat Khalimov, Swen Jacobs, Roderick Paul Bloem - "Towards Efficient Parameterized Synthesis" - Verification, Model Checking, and Abstract Interpretation |  |
 |
 |
| 2012 | Roderick Paul Bloem, Hans-Jürgen Gamauf , Georg Hofferek, Bettina Könighofer, Robert Könighofer - "Synthesizing Robust Systems with RATSY" - Proceedings First Workshop on Synthesis (SYNT 2012) | |
|
|
| 2012 | Roderick Paul Bloem, Swen Jacobs - "Parameterized Synthesis" - Tools and Algorithms for the Construction and Analysis of Systems | |
 |
|
| 2012 | Rüdiger Ehlers, Robert Könighofer, Georg Hofferek - "Symbolically Synthesizing Small Circuits" - Proceedings of the 12th Conference on Formal Methods in Computer-Aided Design (FMCAD 2012) | |
|
|
| 2012 | Matthias Schlaipfer, Georg Hofferek, Roderick Paul Bloem - "Generalized Reactivity(1) Synthesis without a Monolithic Strategy" - Hardware and Software: Verification and Testing. 7th International Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, Revised Selected Papers | |
|
|
| 2012 | Roderick Paul Bloem, Rolf Drechsler, Görschwin Fey, Alexander Finder, Georg Hofferek, Robert Könighofer, Jaan Raik, Urmas Repinski, Andre Sülflow - "FoREnSiC - An Automatic Debugging Environment for C Programs" (Note: to appear) | |
|
|
| 2012 | Robert Könighofer, Roderick Paul Bloem - "Repair with On-The-Fly Program Analysis" (Note: to appear) | |
|
|
| 2011 | Georg Hofferek, Roderick Paul Bloem - "Controller Synthesis for Pipelined Circuits Using Uninterpreted Functions" - Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MemoCODE 2011) | |
|
|
| 2011 | Robert Könighofer, Georg Hofferek, Roderick Paul Bloem - "Debugging Unrealizable Specifications with Model-Based Diagnosis" - Hardware and Software: Verification and Testing 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers | |
|
|
| 2011 | Robert Könighofer, Roderick Paul Bloem - "Automated Error Localization and Correction for Imperative Programs" - Proceedings of 11th International Conference 2011 Formal Methods in Computer Aided Design (FMCAD 2011) | |
|
|
| 2011 | Roderick Paul Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann - "Specification-centered robustness" - 2011 6th International Symposium on Industrial Embedded Systems | |
|
|
| 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 | |
|
|
| 2010 | Roderick Paul Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger, Barbara Jobstmann - "Robustness in the Presence of Liveness" - 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 | 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 | |
|
|
| 2008 | Karin Greimel, Roderick Paul Bloem, Barbara Jobstmann, Moshe Vardi - "Open Implication" - Automata, Languages and Programming - ICALP 2008 | |
|
 |
| 2008 | Andre Suelflow, Goerschwin Fey, Roderick Paul Bloem, Rolf Drechsler - "Using unsatisfiable cores to debug multiple design errors" - Proceedings of the 18th ACM Great Lakes symposium on VLSI | |
|
|
| 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) | |
|
|
| 2008 | Goerschwin Fey, Stefan Simon Staber, Roderick Paul Bloem, Rolf Drechsler - "Automatic Fault Localization for Property Checking" - IEEE transactions on computer-aided design of integrated circuits and systems (Volume: 27 6) | |
|
|
| Master thesis | ||||
|---|---|---|---|---|
| 2009 | Robert Könighofer - "Debugging Formal Specifications with Simplified Counterstrategies" | |
|
|
| 2007 | Karin Greimel - "Open Implication" | |
|
|
| Tech report | ||||
|---|---|---|---|---|
| 2011 | Georg Hofferek, Robert Könighofer, Görschwin Fey, Alexander Finder, Erik Larsson, Urmas Repinski, Jaan Raik - "Transaction-Level Diagnosis" | |
|
|
| 2011 | Rolf Drechsler, Görschwin Fey, Alexander Finder, Andre Sülflow, Robert Könighofer, Georg Hofferek, Urban Ingelsson, Eli Arbel, Jaan Raik, Stephen Scholefield, Artur Jutman - "Definition of the Diagnostic Model" | |
|
|
| 2011 | Georg Hofferek, Robert Könighofer, Jörn-Marc Schmidt, Görschwin Fey, Alexander Finder, Andre Sülflow, Urban Ingelsson, Urmas Repinski, Jaan Raik, Anton Karputkin, Stephen Scholefield - "Status on Implementation-Level Correction" | |
|
|
| 2011 | Rolf Drechsler, Görschwin Fey, Alexander Finder, Georg Hofferek, Robert Könighofer, Eli Arbel, Jaan Raik, Urmas Repinski, Artur Jutman, Stephen Scholefield - "Report on Reasoning Engines and Dynamic Techniques" | |
|
|
| 2011 | Erik Larsson, Urban Ingelsson, Gunnar Carlsson, Artur Jutman, Georg Hofferek - "Status on Post-Silicon and In-Situ Repair" | |
|
|
| 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" | |
|
|
| 2010 | Oleg Rokhlenko, Cindy Eisner, Görschwin Fey, Alexander Finder, Jaan Raik, Maksim Jenihhin, Gunnar Carlsson, Georg Hofferek, Robert Könighofer - "Definition of the DIAMOND Platform" | |
|
|
| 2010 | Tarmo Robal, Jaan Raik, Georg Hofferek, Roderick Paul Bloem, Cindy Eisner, Gunnar Carlsson - "DIAMOND Website (Deliverable D5.1)" | |
|
|
| 2010 | Görschwin Fey, Alexander Finder, Georg Hofferek, Robert Könighofer, Erik Larsson, Jaan Raik, Oleg Rokhlenko - "Requirements & Concept of the Diagnostic Model" | |
|
|
| 2010 | Görschwin Fey, Alexander Finder, Georg Hofferek, Robert Könighofer, Erik Larsson, Urban Ingelsson, Jaan Raik, Eli Arbel, Artur Jutman, Gunnar Carlsson, Stephen Scholefield - "Status on Implementation-Level Diagnosis" | |
|
|
| 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 | Rolf Drechsler, Görschwin Fey, Alexander Finder, Georg Hofferek, Robert Könighofer, Jaan Raik, Oleg Rokhlenko, Stephen Scholefield - "Status on Reasoning Engines and Dynamic Techniques" | |
|
|
| 2010 | Graziano Pravadelli, Franco Fummi, Florian Letombe, Georg Hofferek, Giovanni Perbellini, Marco Roveri, Christophe Hui-Bon-Hoa, Wolfgang Müller, Samuel Dellacherie - "Final report" | |
|
|
| Presentation | ||||
|---|---|---|---|---|
| 2012 | Georg Hofferek - "Automated Synthesis and Design Error Repair of Systems" (IEEE 15th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, Tallinn, 19.04.12) | |
|
|
| 2012 | Robert Könighofer - "FoREnSiC - An Automatic Debugging Environment for C Programs" (Haifa Verification Conference, Haifa, 06.11.12) | |
|
|
| 2012 | Robert Könighofer - "Repair with On-The-Fly Program Analysis" (Haifa Verification Conference, Haifa, 06.11.12) | |
|
|
| 2011 | Georg Hofferek - "Controller Synthesis for Pipelined Circuits Using Uninterpreted Functions" (ACM/IEEE Ninth International Conference on Formal Methods and Models for Codesign (MemoCODE), Microsoft Research Cambridge, 11.07.11) | |
|
|
| 2011 | Robert Könighofer - "Automated Diagnosis and Repair of Simple Software" (DIAMOND tutorial at DATE, Grenoble, 17.03.11) | |
|
|
| 2011 | Robert Könighofer - "Automated error localization and correction for imperative programs" (Formal Methods in Computer Aided Design (FMCAD), Texas, 31.10.11) | |
|
|
| 2010 | Robert Könighofer - "Debugging Unrealizable Specifications with Model-Based Diagnosis" (Haifa Verification Conference, Haifa, 06.10.10) | |
|
|
| 2010 | Georg Hofferek - "Controller Synthesis Using Uninterpreted Functions" (Synthesis, Verification, and Analysis of Rich Models (SVARM 2010), 20.07.10) | |
|
|
| 2010 | Robert Könighofer - "RATSY - A New Requirements Analysis Tool with Synthesis" (CAV 2010, Edinburgh, 18.07.10) | |
|
|
| 2010 | Karin Greimel - "Robustness in the Presence of Liveness" (CAV 2010, 18.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 | Karin Greimel - "Open Implication" (Alpine Verification Meeting, Semmering, 19.05.08) | |
|
|
| 2008 | Karin Greimel - "Open Implication" (International Colloquium on Automata, Languages and Programming, 06.07.08) | |
|
|
| 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) | |
|
|
| Miscellaneous | ||||
|---|---|---|---|---|
| 2012 | Roderick Paul Bloem, Rolf Drechsler, Görschwin Fey, Alexander Finder, Georg Hofferek, Robert Könighofer, Jaan Raik, Urmas Repinski, Andre Sülflow - "FoREnSiC - An Automatic Debugging Environment for C Programs" | |
|
|