Roderick Bloem

Biography

Roderick Bloem received an MS in computer science from Leiden University in the Netherlands (1996) and a PhD from the University of Colorado at Boulder (2001). His thesis work, under the supervision of Fabio Somenzi, was on formal verification using Linear Temporal Logic.

Since 2002, he has been an assistant professor at Graz University of Technology and a full profesor since 2008. His research interests are in formal methods for the design and verification of digital systems, including hardware, software, and combinations such as embedded systems. He studies applications of game theory to the automatic synthesis of systems from their specifications, connections between temporal logics and omega-automata, model checking, and automatic fault localization and repair.

Group

I lead the following groups

• Formal Methods for Design and Verification
• Trusted Computing

Activities

Chair, Austrian Rigorous Systems EngineeringSociety

Chair, FMCAD 10

Memocode 2009

CAV 2009

DATE 2009

COCV 2008

FMCAD 2008

CAV 2008

Alpine Verification Meeting 2008

DATE 2008

HVC 2008

Students

Current:

• Karin Greimel
• Georg Hofferek

Former students:

• Andreas Griesmayer,
• Barbara Jobstmann,
• Ingo Pill,
• Stefan Staber
• Christian Kargl,
• Andreas Leitner,
• Georg Weissenbacher

Miscellaneous

Software Software can be downloaded here.

Magisterpruefungen I will be an examiner for your Magisterpruefung if I have time and the subject is related to my research. If your subject is related to correctness or to theoretical computer science, you stand a good chance. I am not so happy with pure programming projects. I want a 2-10 page summary of your work. If you have written a good introduction to your thesis, you already have such a summary.

How to write an exam Manual.

Projects Bachelor's projects, master's projects, etc can be found here.

Books A list of books that every computer scientist should read.

Publications

Proceedings
2011	Matthias Schlaipfer, Georg Hofferek, Roderick Paul Bloem - "Generalized Reactivity(1) Synthesis without a Monolithic Strategy" (Note: to appear)
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) (Note: to appear)
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	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)
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	Roderick Paul Bloem, Krishnendu Chatterjee, Thomas Henziger, Barbara Jobstmann - "Better Quality in Synthesis through Quantitative Objectives"
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
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
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
2008	Andre Suelflow, Goerschwin Fey, Roderick Paul Bloem, Rolf Drechsler - "Debugging Design Errors by Using Unsatisfiable Cores" - Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
2007	Roderick Paul Bloem, Roberto Cavada, Ingo Hans Pill, Marco Roveri, Andrei Tchaltsev - "RAT: A Tool for the Formal Analysis of Requirements" - 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007. Proceedings
2007	Barbara Jobstmann, Stefan Galler, Martin Weiglhofer, Roderick Paul Bloem - "Anzu: A Tool for Property Synthesis" - Proceedings of the 19th International Conference of Computer Aided Verification 2007
2007	Roderick Paul Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer - "Specify, Compile, Run: Hardware from PSL" - 6th International Workshop on Compiler Optimization Meets Compiler Verification
2007	Stefan Simon Staber, Roderick Paul Bloem - "Fault localization and correction with QBF" - Theory and Applications of Satisfiability Testing – SAT 2007
2007	Roderick Paul Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer - "Interactive presentation: Automatic hardware synthesis from specifications: a case study" - Proceedings of the conference on Design, automation and test in Europe
2006	Andreas Griesmayer, Stefan Simon Staber, Roderick Paul Bloem - "Automated Fault Localization for C Programs"
2006	Barbara Jobstmann, Roderick Paul Bloem - "Optimizations for LTL synthesis"
2006	Barbara Jobstmann, Roderick Paul Bloem - "Game-based and simulation-based improvements for LTL synthesis"
2006	Ingo Hans Pill, Roderick Paul Bloem, Alessandro Cimatti, Marco Roveri, Simone Semprini, Andrei Tchaltsev - "Rat: A tool for formal analysis of requirements"
2006	Andreas Griesmayer, Roderick Paul Bloem, Cook Byron - "Repair of boolean programs with an application to C" - Computer Aided Verification
2006	Ingo Hans Pill, Roderick Paul Bloem, Alessandro Cimatti, Marco Roveri, Simone Semprini - "Symbolic implementation of alternating automata" - Implementation and application of automata
2006	Ingo Hans Pill, Roderick Paul Bloem, Simone Semprini, Marco Roveri, Alessandro Cimatti, Roberto Cavada - "Formal analysis of hardware requirements"
2006	Stefan Simon Staber, Goerschwin Fey, Roderick Paul Bloem, Rolf Drechsler - "Automatic Fault Localization for Property Checking" (Note: to appear)
2005	Stefan Simon Staber, Barbara Jobstmann, Roderick Paul Bloem - "Finding and Fixing Faults" - Correct Hardware Design and Verification Methods
2005	Andreas Griesmayer, Roderick Paul Bloem, Martin Hautzendorfer, Franz Wotawa - "Formal verification of control software: A case study" - Innovations in Applied Artificial Intelligence
2005	Andreas Griesmayer, Roderick Paul Bloem - "Repair of boolean programs using games"
2005	Barbara Jobstmann, Andreas Griesmayer, Roderick Paul Bloem - "Program Repair as a Game " - Computer Aided Verification
2005	Stefan Simon Staber, Barbara Jobstmann, Roderick Paul Bloem - "Diagnosis is Repair" - 16th International Workshop on Principles of Diagnosis
2002	Roderick Paul Bloem, F. Somenzi, K. Ravi - "Analysis of symbolic SCC hull algorithms"
2002	Roderick Paul Bloem, S. Gurumurthy, F. Somenzi - "Fair simulation minimization"
2001	C. Wang, Roderick Paul Bloem, G.D. Hachtel, K. Ravi, F. Somenzi - "Divide and compose: SCC refinement for language emptiness" - CONCUR 2001 - Concurrency Theory
2000	Roderick Paul Bloem, I.-H. Moon, K. Ravi, F. Somenzi - "Approximations for fixpoint computations in symbolic model chec king"
2000	Roderick Paul Bloem, K. Ravi, F. Somenzi - "Symbolic guided search for CTL model checking"
2000	Roderick Paul Bloem, H.N. Gabow, F. Somenzi - "An algorithm for strongly connected component analysis in n log n symbolic steps"
2000	Roderick Paul Bloem, K. Ravi, F. Somenzi - "A comparative study of symbolic algorithms for the computation of fair cycles"
2000	Roderick Paul Bloem, F. Somenzi - "Efficient Büchi automata from LTL formulae"

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)
2007	Roderick Paul Bloem, Alessandro Cimatti, Ingo Hans Pill, Marco Roveri - "Symbolic Implementation of Alternating Automata" - International journal of foundations of computer science (Volume: 18)
2006	C. Wang, Roderick Paul Bloem, G.D. Hachtel, K. Ravi, F. Somenzi - "Compositional SCC analysis for language emptiness" - Formal methods in system design (Volume: 28)
2003	Roderick Paul Bloem - "Recent trends in computer-aided verification" - CoLogNET newsletter [Elektronische Ressource] (Volume: 5)
2003	Roderick Paul Bloem - "Recent trends in computer-aided verification" - CoLogNET newsletter [Elektronische Ressource] (Volume: )
2002	Roderick Bloem, Franz Wotawa - "Verification and Fault Localization in VHDL Programs" - Telematik-Zeitschrift Nr. 2, pages 30-33
2002	Roderick Paul Bloem, Franz Wotawa - "Verification and Fault Localization for VHDL Programs" - Telematik (Volume: 8)
2000	Roderick Paul Bloem, J. Engelfriet - "A comparison of tree transductions defined by monadic second order logic and by attribute grammars" - Journal of computer and system sciences (Volume: 61)

Dissertation
2001	Roderick Paul Bloem - "Search Techniques and Automata for Symbolic Model Checking"

Tech report
2011	Ronald Tögl, Martin Pirker, Roderick Paul Bloem, Georg Lindsberger, Stefan Posch - "acTvSM Deliverable 6.1: Business Model and Product Roadmap"
2010	Tarmo Robal, Jaan Raik, Georg Hofferek, Roderick Paul Bloem, Cindy Eisner, Gunnar Carlsson - "DIAMOND Website (Deliverable D5.1)"

Presentation
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)
2007	Roderick Paul Bloem - "Haifa Verification Conference Award Ceremony" (Haifa Verification Conference, 24.10.07)
2006	Roderick Paul Bloem - "Fault Localization" (OneSpin Solutions, München, 08.03.06)
2006	Roderick Paul Bloem - "Sugar" (Te-DES Workshop, 09.01.06)
2005	Roderick Paul Bloem - "Fault Localization and Correction" (Alpine Verification Meeting, Lausanne, 05.10.05)
2005	Roderick Paul Bloem - "Fault Localization" (Technion Workshop, Haifa, 21.11.05)
2005	Roderick Paul Bloem - "Fault Localization and Correction" (PROSYD Technical Advisory Committee Meeting, Edinburgh, 12.07.05)
2005	Roderick Paul Bloem - "Program Repair as a Game" (PROSYD Workshop, IBM, Haifa, 10.02.05)
2005	Roderick Paul Bloem - "Program Repair" (Universitäre Vortragsreihe an der Hebrew University, Jerusalem, 12.02.05)
2004	Roderick Paul Bloem - "Property-Based Software Verification" (PROSYD Workshop, ETH Zürich, Zürich, 12.04.04)
2004	Roderick Paul Bloem - "VeriDACS, a Prototype for Formal Verification of DACS Programs" (VeriDACS WOrkshop, Festo, Wien, 27.05.04)