Richard Bubel

Richard Bubel
Richard Bubel Dept. of Computer Science and Engineering Chalmers University of Technology and Göteborg University 412-96 Göteborg, Sweden Room: 5479, Computer Science and Engineering Building Mail: bubel@chalmers.se Tel: +46 (0)31 772 1078	I am a member of the Software Engineering using Formal Methods group lead by Prof. Dr. Reiner Hähnle. Short Facts About Me: ShortCV Research Interests: Software specification and verification, logics and automated theorem proving Projects: I am currently involved in EU-FP7 project HATS as project coordinator (working for scientific coordinator Prof. Dr. R. Hähnle) and researcher KeY as project member and main developer COST IC0701 as regular participant of meetings, conferences (no official role) Other Activities: co-PC chair of the 10-th KeY Symposium (part of the workshop programme of ITP 2011) co-presenter at the COST IC0701--Training School 2011 SET Division Wintermeeting 2010 (co-organiser) HATS Annual Meeting, Göteborg, 2009 (local co-organiser) COST IC0701 Action Meeting, Göteborg, 2008 (local co-organiser) 7th-KeY-Symposium, Göteborg, 2008 (local co-organiser) 5th-KeY-Symposium, Speyer, 2006 (local co-organiser) Reviewing: WING'11 (journal), TACAS'11, FM'11, FOVEOOS'10, LPAR-16, VERIFY'10, VMCAI'10, CADE'09, ECOOP'09, FMCO'09, TABLEAUX'09, TAP'09, WING'09 (journal and workshop) and many more Supervision I am thankful to be the PhD co-supervisor of Ran Ji (together with Reiner Hähnle) and Gabriele Paganelli (together with Wolfgang Ahrendt). Teaching Programming Paradigms 2010 (winter 2010) Software Engineering using Formal Methods 10 (autumn 2010) Software Engineering using Formal Methods 09 Publications Submitted Verified Resource Guarantees for Heap Manipulating Programs Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, and Guillermo Román-Díez submitted to CPP'11 2011 A Formalisation of Java Strings for Program Specification and Verification Richard Bubel, Reiner Hähnle and Ulrich Geilmann Proceedings of SEFM'11, LNCS, Springer (to appear) Program Specialization Via a Software Verification Tool Richard Bubel, Reiner Hähnle and Ran Ji Post-Proceedings of FMCO'10, LNCS, Springer, 2011 (to appear) Verified Resource Guarantees using COSTA and KeY Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, German Puebla and Guillermo Román-Díez Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2011), Austin, TX, USA, April 2011, ACM Specifying Imperative ML-like programs using Dynamic Logic Séverine Maingaud, Vincent Balat, Richard Bubel, Reiner Hähnle and Alexandre Miquel Post-Proceedings of the International Conference on Formal Verification of Object-oriented Software, Springer-Verlag LNCS, 2011 2010 Visual Interactive Debugger Based on Symbolic Execution Reiner Hähnle, Markus Baum, Richard Bubel and Marcel Rothe 25th IEEE/ACM International Conference on Automated Software Engineering, Antwerp, 2010, ACM Verification of Variable Software: An Experience Report Richard Bubel, Crystal Din and Reiner Hähnle Presented at and in pre-proceedings (technical report) of the International Conference on Formal Verification of Object-oriented Software, 2010 Interleaving Symbolic Execution and Partial Evaluation Richard Bubel, Reiner Hähnle and Ran Ji Post-Proceedings 7th Intl. Symposium on Formal Methods for Components and Objects, Eindhoven, Netherlands, Springer-Verlag LNCS,2010 2009 Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification Wolfgang Ahrendt, Richard Bubel and Reiner Hähnle Proceedings of the Second International Conference on Teaching Formal Methods, 2009 Abstract Interpretation of Symbolic Execution with Explicit State Updates Richard Bubel, Reiner Hähnle and Benjamin Weiß Post-Proceedings of FMCO'08, 2009 2008 Specification Predicates with Explicit Dependency Information Richard Bubel, Reiner Hähnle and Peter H. Schmitt Proceedings of the 5th International Verification Workshop, 2008 A Hoare-Style Calculus with Explicit State Updates Reiner Hähnle and Richard Bubel Proceedings Formal Methods in Computer Science Education (FORMED), Satellite Event of ETAPS 2008, Budapest, Hungary, Electronic Notes in Theoretical Computer Science, Elsevier 2007 and Older Pattern-Driven Formal Specification Richard Bubel and Reiner Hähnle In Verification of Object-Oriented Software: The KeY Approach (book chapter) Editors: Bernhard Beckert, Reiner Hähnle and Peter H. Schmitt, Springer-Verlag, LNCS 4334, pp 295-315 The Schorr-Waite-Algorithm Richard Bubel In Verification of Object-Oriented Software: The KeY Approach (book chapter) Editors: Bernhard Beckert, Reiner Hähnle and Peter H. Schmitt, Springer-Verlag, LNCS 4334, pp 295-315 The KeY Tool Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager and Peter H. Schmitt Software and Systems Modeling, Springer 2005 Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software - A Case Study with the KeY System Reiner Hähnle and Richard Bubel International Journal on Software Tools for Technology Transfer (STTT), Springer, 2005 Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software - A Case Study with the KeY System Reiner Hähnle and Richard Bubel Proceedings Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03).

Richard Bubel
Dept. of Computer Science and Engineering
Chalmers University of Technology and Göteborg University
412-96 Göteborg, Sweden
Room: 5479, Computer Science and Engineering Building
Mail: bubel@chalmers.se
Tel: +46 (0)31 772 1078

I am a member of the Software Engineering using Formal Methods group lead by Prof. Dr. Reiner Hähnle.

Short Facts

About Me: ShortCV
Research Interests: Software specification and verification, logics and automated theorem proving
Projects: I am currently involved in

EU-FP7 project HATS as project coordinator (working for scientific coordinator Prof. Dr. R. Hähnle) and researcher
KeY as project member and main developer
COST IC0701 as regular participant of meetings, conferences (no official role)

Other Activities:

co-PC chair of the 10-th KeY Symposium (part of the workshop programme of ITP 2011)
co-presenter at the COST IC0701--Training School 2011
SET Division Wintermeeting 2010 (co-organiser)
HATS Annual Meeting, Göteborg, 2009 (local co-organiser)
COST IC0701 Action Meeting, Göteborg, 2008 (local co-organiser)
7th-KeY-Symposium, Göteborg, 2008 (local co-organiser)
5th-KeY-Symposium, Speyer, 2006 (local co-organiser)

Reviewing: WING'11 (journal), TACAS'11, FM'11, FOVEOOS'10, LPAR-16, VERIFY'10, VMCAI'10,
CADE'09, ECOOP'09, FMCO'09, TABLEAUX'09, TAP'09, WING'09 (journal and workshop) and many more

Supervision

I am thankful to be the PhD co-supervisor of Ran Ji (together with Reiner Hähnle) and Gabriele Paganelli (together with Wolfgang Ahrendt).

Teaching

Publications

Submitted

Verified Resource Guarantees for Heap Manipulating Programs: Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, and Guillermo Román-Díez
submitted to CPP'11

2011

A Formalisation of Java Strings for Program Specification and Verification: Richard Bubel, Reiner Hähnle and Ulrich Geilmann
Proceedings of SEFM'11, LNCS, Springer (to appear)

Verified Resource Guarantees using COSTA and KeY: Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, German Puebla and Guillermo Román-Díez
Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2011), Austin, TX, USA, April 2011, ACM

Specifying Imperative ML-like programs using Dynamic Logic: Séverine Maingaud, Vincent Balat, Richard Bubel, Reiner Hähnle and Alexandre Miquel
Post-Proceedings of the International Conference on Formal Verification of Object-oriented Software, Springer-Verlag LNCS, 2011

2010

Visual Interactive Debugger Based on Symbolic Execution: Reiner Hähnle, Markus Baum, Richard Bubel and Marcel Rothe
25th IEEE/ACM International Conference on Automated Software Engineering, Antwerp, 2010, ACM

Verification of Variable Software: An Experience Report: Richard Bubel, Crystal Din and Reiner Hähnle
Presented at and in pre-proceedings (technical report) of the International Conference on Formal Verification of Object-oriented Software, 2010

Interleaving Symbolic Execution and Partial Evaluation: Richard Bubel, Reiner Hähnle and Ran Ji
Post-Proceedings 7th Intl. Symposium on Formal Methods for Components and Objects, Eindhoven, Netherlands, Springer-Verlag LNCS,2010

2009

Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification: Wolfgang Ahrendt, Richard Bubel and Reiner Hähnle
Proceedings of the Second International Conference on Teaching Formal Methods, 2009

Abstract Interpretation of Symbolic Execution with Explicit State Updates: Richard Bubel, Reiner Hähnle and Benjamin Weiß
Post-Proceedings of FMCO'08, 2009

2008

Specification Predicates with Explicit Dependency Information: Richard Bubel, Reiner Hähnle and Peter H. Schmitt
Proceedings of the 5th International Verification Workshop, 2008

A Hoare-Style Calculus with Explicit State Updates: Reiner Hähnle and Richard Bubel
Proceedings Formal Methods in Computer Science Education (FORMED),
Satellite Event of ETAPS 2008, Budapest, Hungary,
Electronic Notes in Theoretical Computer Science, Elsevier

2007 and Older

Pattern-Driven Formal Specification: Richard Bubel and Reiner Hähnle
In Verification of Object-Oriented Software: The KeY Approach
(book chapter) Editors: Bernhard Beckert, Reiner Hähnle and Peter H. Schmitt, Springer-Verlag, LNCS 4334, pp 295-315

The Schorr-Waite-Algorithm: Richard Bubel
In Verification of Object-Oriented Software: The KeY Approach
(book chapter) Editors: Bernhard Beckert, Reiner Hähnle and Peter H. Schmitt, Springer-Verlag, LNCS 4334, pp 295-315

The KeY Tool: Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager and Peter H. Schmitt
Software and Systems Modeling, Springer 2005

Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software - A Case Study with the KeY System: Reiner Hähnle and Richard Bubel
International Journal on Software Tools for Technology Transfer (STTT), Springer, 2005

Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software - A Case Study with the KeY System: Reiner Hähnle and Richard Bubel
Proceedings Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03).