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 Systematic Construction of Correct Systems group.

Activities

Chair, Austrian Rigorous Systems Engineering Society (with Helmut Veith)

Chair, CAV14 (with Armin Biere)

Chair, FMCAD 10 (with Natasha Sharygina)

Memocode 2009 (with Patrick Schaumont)

Students

Current:

  • Nicolas Braud-Santoni
  • Daniel Hein
  • Ayrat Khalimov
  • Bettina Koenighofer
  • Franz Roeck
  • Johannes Winter

Former students:

  • Andreas Griesmayer,
  • Georg Hofferek
  • Robert Koenighofer
  • Stefan Kraxberger,
  • Barbara Jobstmann,
  • Ingo Pill,
  • Martin Pirker,
  • Stefan Staber
  • Ronald Toegl
Miscellaneous

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.

Publications
PROCEEDINGS
2015Roderick Paul Bloem, Bettina Könighofer, Robert Könighofer, Chao Wang — «Shield Synthesis: — Runtime Enforcement for Reactive Systems» — Tools and Algorithms for the Construction and Analysis of Systems (TACAS) — 21st International Conference
2015Roderick Paul Bloem, Krishnendu Chatterjee, Swen Jacobs, Robert Könighofer — «Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information» — Tools and Algorithms for the Construction and Analysis of Systems (TACAS) — 21st International Conference
2015Roderick Bloem, Rüdiger Ehlers, Robert Könighofer — «Cooperative Reactive Synthesis» — Automated Technology for Verification and Analysis (ATVA'15)
2015Roderick Paul Bloem, Daniel Hein, Franz Röck, Richard Alexander Schumi — «Case Study: Automatic Test Case Generation for a Secure Cache Implementation» ( Note: to appear)
2015Rüdiger Ehlers, Robert Könighofer, Roderick Bloem — «Synthesizing cooperative reactive mission plans» — International Conference on Intelligent Robots and Systems (IROS'15)
2014Roderick Paul Bloem, Rüdiger Ehlers, Swen Jacobs, Robert Könighofer — «How to Handle Assumptions in Synthesis» — Proceedings 3rd Workshop on Synthesis
2014Roderick Paul Bloem, Robert Könighofer, Martina Seidl — «SAT-Based Synthesis Methods for Safety Specs» — Verification, Model Checking, and Abstract Interpretation, 15th International Conference
2014Roderick Paul Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Außerlechner, Raphael Spörk — «Synthesis of Synchronization using Uninterpreted Functions» — Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design FMCAD 2014
2014Robert Könighofer, Ronald Tögl, Roderick Paul Bloem — «Automatic Error Localization for Software using Deductive Verification» — Hardware and Software: Verification and Testing — Proceedings of the 10th International Haifa Verification Conference (HVC 2014)
2014Viktoria Pammer-Schindler, Hermann Stern, Stefan Edler, Daniel Hein, Martin Pirker, Roderick Paul Bloem, Alfred Wertner — «Security Concepts for a Distributed Architecture for Activity Logging and Analysis» — Proceeding i-KNOW '14 Proceedings of the 14th International Conference on Knowledge Technologies and Data-driven Business
2014Roderick Paul Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing — «SAT-based methods for circuit synthesis» — Formal Methods in Computer-Aided Design
2014Ayrat Khalimov, Roderick Paul Bloem, Swen Jacobs — «Parameterized Synthesis Case Study: AMBA AHB» — SYNT 2014
2014Roderick Paul Bloem, Robert Könighofer, Franz Röck, Michael Tautschnig — «Automating Test-Suite Augmentation»
2013Ayrat Khalimov, Swen Jacobs, Roderick Paul Bloem — «Towards Efficient Parameterized Synthesis» — Verification, Model Checking, and Abstract Interpretation
2013Georg Hofferek, Ashutosh Gupta, Bettina Könighofer, Jie-Hong Roland Jiang, Roderick Paul Bloem — «Synthesizing Multiple Boolean Functions using Interpolation on a Single Proof» — FMCAD 2013 — Formal Methods in Computer-Aided Design
2013Ayrat Khalimov, Swen Jacobs, Roderick Paul Bloem — «PARTY: parameterized synthesis of token rings»
2013Roderick Paul Bloem, Karin Greimel, Robert Könighofer, Franz Röck — «Model-Based MCDC Testing of Complex Decisions for the Java Card Applet Firewall» — VALID proceedings
2012Roderick Paul Bloem, Swen Jacobs — «Parameterized Synthesis» — Tools and Algorithms for the Construction and Analysis of Systems
2012Matthias 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
2012Roderick 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)
2012Robert Könighofer, Roderick Paul Bloem — «Repair with On-The-Fly Program Analysis» — Hardware and Software: Verification and Testing — 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers
2012Roderick 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»
2011Georg 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)
2011Robert 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)
2011Robert 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
2011Roderick Paul Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann — «Specification-centered robustness» — 2011 6th International Symposium on Industrial Embedded Systems
2010Roderick 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
2010Roderick Paul Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger, Barbara Jobstmann — «Robustness in the Presence of Liveness» — Computer Aided Verification
2009Roderick 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
2009Robert 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
2009Roderick Paul Bloem, Krishnendu Chatterjee, Thomas Henziger, Barbara Jobstmann — «Better Quality in Synthesis through Quantitative Objectives»
2008Andre 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
2008Ronald 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
2008Karin Greimel, Roderick Paul Bloem, Barbara Jobstmann, Moshe Vardi — «Open Implication» — Automata, Languages and Programming — ICALP 2008
2008Andre 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
2007Roderick 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
2007Barbara 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
2007Roderick 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
2007Stefan Simon Staber, Roderick Paul Bloem — «Fault localization and correction with QBF» — Theory and Applications of Satisfiability Testing – SAT 2007
2007Roderick 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
2006Ingo Hans Pill, Roderick Paul Bloem, Alessandro Cimatti, Marco Roveri, Simone Semprini — «Symbolic implementation of alternating automata» — Implementation and application of automata
2006Ingo Hans Pill, Roderick Paul Bloem, Simone Semprini, Marco Roveri, Alessandro Cimatti, Roberto Cavada — «Formal analysis of hardware requirements»
2006Barbara Jobstmann, Roderick Paul Bloem — «Optimizations for LTL synthesis»
2006Stefan Simon Staber, Goerschwin Fey, Roderick Paul Bloem, Rolf Drechsler — «Automatic Fault Localization for Property Checking» ( Note: to appear)
2006Ingo Hans Pill, Roderick Paul Bloem, Alessandro Cimatti, Marco Roveri, Simone Semprini, Andrei Tchaltsev — «Rat: A tool for formal analysis of requirements»
2006Andreas Griesmayer, Roderick Paul Bloem, Cook Byron — «Repair of boolean programs with an application to C» — Computer Aided Verification
2006Andreas Griesmayer, Stefan Simon Staber, Roderick Paul Bloem — «Automated Fault Localization for C Programs»
2006Barbara Jobstmann, Roderick Paul Bloem — «Game-based and simulation-based improvements for LTL synthesis»
2005Barbara Jobstmann, Andreas Griesmayer, Roderick Paul Bloem — «Program Repair as a Game » — Computer Aided Verification
2005Stefan Simon Staber, Barbara Jobstmann, Roderick Paul Bloem — «Finding and Fixing Faults» — Correct Hardware Design and Verification Methods
2005Stefan Simon Staber, Barbara Jobstmann, Roderick Paul Bloem — «Diagnosis is Repair» — 16th International Workshop on Principles of Diagnosis
2005Andreas Griesmayer, Roderick Paul Bloem, Martin Hautzendorfer, Franz Wotawa — «Formal verification of control software: A case study» — Innovations in Applied Artificial Intelligence
2005Andreas Griesmayer, Roderick Paul Bloem — «Repair of boolean programs using games»
2002Roderick Paul Bloem, F. Somenzi, K. Ravi — «Analysis of symbolic SCC hull algorithms»
2002Roderick Paul Bloem, S. Gurumurthy, F. Somenzi — «Fair simulation minimization»
2001C. Wang, Roderick Paul Bloem, G.D. Hachtel, K. Ravi, F. Somenzi — «Divide and compose: SCC refinement for language emptiness» — CONCUR 2001 — Concurrency Theory
2000Roderick Paul Bloem, K. Ravi, F. Somenzi — «A comparative study of symbolic algorithms for the computation of fair cycles»
2000Roderick Paul Bloem, H.N. Gabow, F. Somenzi — «An algorithm for strongly connected component analysis in n log n symbolic steps»
2000Roderick Paul Bloem, I.-H. Moon, K. Ravi, F. Somenzi — «Approximations for fixpoint computations in symbolic model chec king»
2000Roderick Paul Bloem, F. Somenzi — «Efficient Büchi automata from LTL formulae»
2000Roderick Paul Bloem, K. Ravi, F. Somenzi — «Symbolic guided search for CTL model checking»

BOOK
2015Ayrat Khalimov, Roderick Bloem, Helmut Veith, Josef Widder, Igor Konnov, Sasha Rubin, Swen Jacobs — «Decidability of Parameterized Verification»

ARTICLE
2014Roderick Paul Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, Robert Könighofer — «Synthesizing Robust Systems» — Acta informatica (Volume: 51 3)
2013Robert 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: 15)
2008Goerschwin 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)
2007Roderick Paul Bloem, Alessandro Cimatti, Ingo Hans Pill, Marco Roveri — «Symbolic Implementation of Alternating Automata» — International journal of foundations of computer science (Volume: 18)
2006C. Wang, Roderick Paul Bloem, G.D. Hachtel, K. Ravi, F. Somenzi — «Compositional SCC analysis for language emptiness» — Formal methods in system design (Volume: 28)
2003Roderick Paul Bloem — «Recent trends in computer-aided verification» — CoLogNET newsletter [Elektronische Ressource] (Volume: )
2003Roderick Paul Bloem — «Recent trends in computer-aided verification» — CoLogNET newsletter [Elektronische Ressource] (Volume: 5)
2002Roderick Paul Bloem, Franz Wotawa — «Verification and Fault Localization for VHDL Programs» — Telematik (Volume: 8)
2002Roderick Bloem, Franz Wotawa — «Verification and Fault Localization in VHDL Programs» — Telematik-Zeitschrift Nr. 2, pages 30-33
2000Roderick 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
2001Roderick Paul Bloem — «Search Techniques and Automata for Symbolic Model Checking»

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

PRESENTATION
2013Roderick Paul Bloem, Karin Greimel, Robert Könighofer, Franz Röck — «Model-Based MCDC Testing of Complex Decisions for the Java Card Applet Firewall» (VALID 2013, Venice, 28.10.13)
2009Robert 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)
2007Roderick Paul Bloem — «Haifa Verification Conference Award Ceremony» (Haifa Verification Conference, 24.10.07)
2006Roderick Paul Bloem — «Fault Localization» (OneSpin Solutions, München, 08.03.06)
2006Roderick Paul Bloem — «Sugar» (Te-DES Workshop, 09.01.06)
2005Roderick Paul Bloem — «Fault Localization» (Technion Workshop, Haifa, 21.11.05)
2005Roderick Paul Bloem — «Fault Localization and Correction» (Alpine Verification Meeting, Lausanne, 05.10.05)
2005Roderick Paul Bloem — «Program Repair as a Game» (PROSYD Workshop, IBM, Haifa, 10.02.05)
2005Roderick Paul Bloem — «Program Repair» (Universitäre Vortragsreihe an der Hebrew University, Jerusalem, 12.02.05)
2005Roderick Paul Bloem — «Fault Localization and Correction» (PROSYD Technical Advisory Committee Meeting, Edinburgh, 12.07.05)
2004Roderick Paul Bloem — «Property-Based Software Verification» (PROSYD Workshop, ETH Zürich, Zürich, 12.04.04)
2004Roderick Paul Bloem — «VeriDACS, a Prototype for Formal Verification of DACS Programs» (VeriDACS WOrkshop, Festo, Wien, 27.05.04)

MISCELLANEOUS
2012Roderick 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»
  • ...
  • 0
  • 0
0 comments