default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDRichard Bubel
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c43]Adele Veschetti, Richard Bubel, Reiner Hähnle:
SmartML: Enhancing Security and Reliability in Smart Contract Development. DLT 2024- [c42]Bernhard Beckert
, Richard Bubel, Daniel Drodt, Reiner Hähnle, Florian Lanzinger, Wolfram Pfeifer, Mattias Ulbrich, Alexander Weigl:
The Java Verification Tool KeY:A Tutorial. FM (2) 2024: 597-623 - [i3]Adele Veschetti, Richard Bubel, Reiner Hähnle:
SmartML: Towards a Modeling Language for Smart Contracts. CoRR abs/2403.06622 (2024) - 2023
- [c41]Richard Bubel, Dilian Gurov, Reiner Hähnle, Marco Scaletta:
Trace-based Deductive Verification. LPAR 2023: 73-95 - 2022
- [c40]Lukas Grätz, Reiner Hähnle, Richard Bubel:
Finding Semantic Bugs Fast. FASE 2022: 145-154 - [c39]Asmae Heydari Tabar, Richard Bubel, Reiner Hähnle:
Automatic Loop Invariant Generation for Data Dependence Analysis. FormaliSE@ICSE 2022: 34-45 - [c38]Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich:
Towards a Usable and Sustainable Deductive Verification Tool. ISoLA (2) 2022: 281-300 - [e3]Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Einar Broch Johnsen:
The Logic of Software. A Tasting Menu of Formal Methods - Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 13360, Springer 2022, ISBN 978-3-031-08165-1 [contents] - [d2]Lukas Grätz, Reiner Hähnle, Richard Bubel:
Examples For FASE NIER Paper "Finding Semantic Bugs Fast". Zenodo, 2022
- [d1]Lukas Grätz, Reiner Hähnle, Richard Bubel:
Examples For FASE NIER Paper "Finding Semantic Bugs Fast". Zenodo, 2022 - [i2]Richard Bubel, Dilian Gurov, Reiner Hähnle, Marco Scaletta:
Towards Trace-based Deductive Verification (Tech Report). CoRR abs/2211.09487 (2022) - 2021
- [c37]Marco Scaletta, Reiner Hähnle, Dominic Steinhöfel, Richard Bubel:
Delta-based verification of software product families. GPCE 2021: 69-82 - 2020
- [c36]Wolfgang Ahrendt, Richard Bubel:
Functional Verification of Smart Contracts via Strong Data Integrity. ISoLA (3) 2020: 9-24 - [p10]Alexander Knüppel, Stefan Krüger, Thomas Thüm, Richard Bubel, Sebastian Krieter, Eric Bodden, Ina Schaefer:
Using Abstract Contracts for Verifying Evolving Features and Their Interactions. 20 Years of KeY 2020: 122-148 - [p9]Jonas Schiffl, Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel:
Formal Analysis of Smart Contracts: Applying the KeY System. 20 Years of KeY 2020: 204-218 - [e2]Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich:
Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY. Lecture Notes in Computer Science 12345, Springer 2020, ISBN 978-3-030-64353-9 [contents]
2010 – 2019
- 2019
- [j9]Stijn de Gouw, Frank S. de Boer, Richard Bubel, Reiner Hähnle, Jurriaan Rot, Dominic Steinhöfel:
Verifying OpenJDK's Sort Method for Generic Collections. J. Autom. Reason. 62(1): 93-126 (2019) - [j8]Martin Hentschel, Richard Bubel, Reiner Hähnle:
The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more. Int. J. Softw. Tools Technol. Transf. 21(5): 485-513 (2019) - [c35]Wolfgang Ahrendt, Richard Bubel, Joshua Ellul, Gordon J. Pace, Raúl Pardo, Vincent Rebiscoul, Gerardo Schneider:
Verification of Smart Contract Business Logic - Exploiting a Java Source Code Verifier. FSEN 2019: 228-243 - [c34]Richard Bubel, Reiner Hähnle, Asmae Heydari Tabar:
A Program Logic for Dependence Analysis. IFM 2019: 83-100 - 2017
- [j7]Quoc Huy Do, Richard Bubel, Reiner Hähnle:
Automatic detection and demonstrator generation for information flow leaks in object-oriented programs. Comput. Secur. 67: 335-349 (2017) - [c33]Quoc Huy Do, Richard Bubel, Reiner Hähnle:
Inferring Secrets by Guided Experiments. ICTAC 2017: 269-287 - 2016
- [j6]Richard Bubel, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, Olaf Owe, Ina Schaefer, Ingrid Chieh Yu:
Proof Repositories for Compositional Verification of Evolving Software Systems - Managing Change When Proving Software Correct. LNCS Trans. Found. Mastering Chang. 1: 130-156 (2016) - [j5]Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, Guillermo Román-Díez:
A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. Softw. Syst. Model. 15(4): 987-1012 (2016) - [j4]Stijn de Gouw, Frank S. de Boer, Wolfgang Ahrendt, Richard Bubel:
Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic. Softw. Syst. Model. 15(4): 1117-1140 (2016) - [c32]Reiner Hähnle, Nathan Wasser, Richard Bubel:
Array Abstraction with Symbolic Pivots. Theory and Practice of Formal Methods 2016: 104-121 - [c31]Dominic Scheurer, Reiner Hähnle, Richard Bubel:
A General Lattice Model for Merging Symbolic Execution Branches. ICFEM 2016: 57-73 - [c30]Martin Hentschel, Reiner Hähnle, Richard Bubel:
Can Formal Methods Improve the Efficiency of Code Reviews? IFM 2016: 3-19 - [c29]Martin Hentschel, Reiner Hähnle, Richard Bubel:
An empirical evaluation of two user interfaces of an interactive program verifier. ASE 2016: 403-413 - [c28]Martin Hentschel, Reiner Hähnle, Richard Bubel:
The interactive verification debugger: effective understanding of interactive proof attempts. ASE 2016: 846-851 - [p8]Peter H. Schmitt, Richard Bubel:
Theories. Deductive Software Verification 2016: 149-166 - [p7]Nathan Wasser, Reiner Hähnle, Richard Bubel:
Abstract Interpretation. Deductive Software Verification 2016: 167-189 - [p6]Daniel Grahl, Richard Bubel, Wojciech Mostowski, Peter H. Schmitt, Mattias Ulbrich, Benjamin Weiß:
Modular Specification and Verification. Deductive Software Verification 2016: 289-351 - [p5]Martin Hentschel, Reiner Hähnle, Richard Bubel:
Debugging and Visualization. Deductive Software Verification 2016: 383-413 - [p4]Ran Ji, Richard Bubel:
Program Transformation and Compilation. Deductive Software Verification 2016: 473-492 - [p3]Richard Bubel, Reiner Hähnle:
KeY-Hoare. Deductive Software Verification 2016: 571-589 - [e1]Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, Mattias Ulbrich:
Deductive Software Verification - The KeY Book - From Theory to Practice. Lecture Notes in Computer Science 10001, Springer 2016, ISBN 978-3-319-49811-9 [contents] - 2015
- [j3]Peter Y. H. Wong, Richard Bubel, Frank S. de Boer, Miguel Gómez-Zamalloa, Stijn de Gouw, Reiner Hähnle, Karl Meinke, Muddassar Azam Sindhu:
Testing abstract behavioral specifications. Int. J. Softw. Tools Technol. Transf. 17(1): 107-119 (2015) - [c27]Crystal Chang Din, Richard Bubel, Reiner Hähnle:
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS. CADE 2015: 517-526 - [c26]Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, Reiner Hähnle:
OpenJDK's Java.utils.Collection.sort() Is Broken: The Good, the Bad and the Worst Case. CAV (1) 2015: 273-289 - [c25]Quoc Huy Do, Richard Bubel, Reiner Hähnle:
Exploit Generation for Information Flow Leaks in Object-Oriented Programs. SEC 2015: 401-415 - [c24]Richard Bubel, Crystal Chang Din, Reiner Hähnle, Keiko Nakata:
A Dynamic Logic with Traces and Coinduction. TABLEAUX 2015: 307-322 - [i1]Bart van Delft, Richard Bubel:
Dependency-Based Information Flow Analysis with Declassification in a Program Logic. CoRR abs/1509.04153 (2015) - 2014
- [c23]Martin Hentschel, Stefan Käsdorf, Reiner Hähnle, Richard Bubel:
An Interactive Verification Tool Meets an IDE. IFM 2014: 55-70 - [c22]Richard Bubel, Reiner Hähnle, Maria Pelevina:
Fully Abstract Operation Contracts. ISoLA (2) 2014: 120-134 - [c21]Crystal Chang Din, Olaf Owe, Richard Bubel:
Runtime Assertion Checking and Theorem Proving for Concurrent and Distributed Systems. MODELSWARD 2014: 480-487 - [c20]Martin Hentschel, Richard Bubel, Reiner Hähnle:
Symbolic Execution Debugger (SED). RV 2014: 255-262 - [c19]Richard Bubel, Antonio Flores-Montoya, Reiner Hähnle:
Analysis of Executable Software Models. SFM 2014: 1-25 - [c18]Martin Hentschel, Reiner Hähnle, Richard Bubel:
Visualizing Unbounded Symbolic Execution. TAP@STAF 2014: 82-98 - [c17]Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, Mattias Ulbrich:
The KeY Platform for Verification and Analysis of Java Programs. VSTTE 2014: 55-71 - 2013
- [c16]Reiner Hähnle, Ina Schaefer, Richard Bubel:
Reuse in Software Verification by Abstract Method Calls. CADE 2013: 300-314 - [c15]Ran Ji, Reiner Hähnle, Richard Bubel:
Program Transformation Based on Symbolic Execution and Deduction. SEFM 2013: 289-304 - [c14]Stijn de Gouw, Frank S. de Boer, Wolfgang Ahrendt, Richard Bubel:
Weak Arithmetic Completeness of Object-Oriented First-Order Assertion Networks. SOFSEM 2013: 207-219 - 2012
- [c13]Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Guillermo Román-Díez:
Verified Resource Guarantees for Heap Manipulating Programs. FASE 2012: 130-145 - [c12]Ran Ji, Richard Bubel:
PE-KeY: A Partial Evaluator for Java Programs. IFM 2012: 283-295 - 2011
- [c11]Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla, Guillermo Román-Díez:
Verified resource guarantees using COSTA and KeY. PEPM 2011: 73-76 - [c10]Richard Bubel, Reiner Hähnle, Ulrich Geilmann:
A Formalisation of Java Strings for Program Specification and Verification. SEFM 2011: 90-105 - 2010
- [c9]Richard Bubel, Reiner Hähnle, Ran Ji:
Program Specialization via a Software Verification Tool. FMCO 2010: 80-101 - [c8]Séverine Maingaud, Vincent Balat, Richard Bubel, Reiner Hähnle, Alexandre Miquel:
Specifying Imperative ML-Like Programs Using Dynamic Logic. FoVeOOS 2010: 122-137 - [c7]Reiner Hähnle, Marcus Baum, Richard Bubel, Marcel Rothe:
A visual interactive debugger based on symbolic execution. ASE 2010: 143-146
2000 – 2009
- 2009
- [c6]Richard Bubel, Reiner Hähnle, Ran Ji:
Interleaving Symbolic Execution and Partial Evaluation. FMCO 2009: 125-146 - [c5]Wolfgang Ahrendt, Richard Bubel, Reiner Hähnle:
Integrated and Tool-Supported Teaching of Testing, Debugging, and Verification. TFM 2009: 125-143 - 2008
- [c4]Richard Bubel, Reiner Hähnle, Peter H. Schmitt:
Specification Predicates with Explicit Dependency Information. VERIFY 2008 - [c3]Richard Bubel, Reiner Hähnle, Benjamin Weiß:
Abstract Interpretation of Symbolic Execution with Explicit State Updates. FMCO 2008: 247-277 - 2007
- [b1]Richard Bubel:
Formal verification of recursive predicates. Karlsruhe Institute of Technology, Germany, 2007, pp. 1-141 - [p2]Richard Bubel, Reiner Hähnle:
Pattern-Driven Formal Specification. The KeY Approach 2007: 295-315 - [p1]Richard Bubel:
The Schorr-Waite-Algorithm. The KeY Approach 2007: 569-587 - 2005
- [j2]Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, Peter H. Schmitt:
The KeY tool. Softw. Syst. Model. 4(1): 32-54 (2005) - [j1]Richard Bubel, Reiner Hähnle:
Integration of informal and formal development of object-oriented safety-critical software. Int. J. Softw. Tools Technol. Transf. 7(3): 197-211 (2005) - 2004
- [c2]Richard Bubel, Andreas Roth, Philipp Rümmer:
Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic. LFM@IJCAR 2004: 107-128 - 2003
- [c1]Richard Bubel, Reiner Hähnle:
Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software: A Case Study with the KeY System. FMICS 2003: 1-23
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-22 21:15 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
