Publications
Rather group by categories.
Title | Author(s) | Source |
---|---|---|
Scalable and Precise Refinement Types for Imperative Languages | Florian Lanzinger, Joshua Bachmeier, Mattias Ulbrich, and Werner Dietl | iFM 2023 - 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13-15, 2023, Proceedings |
The 'Choc-Machine' - an Introduction to Algorithmic Thinking Using Finite State Machines | Annika Vielsack, Miriam Klein, Thomas Niesenhaus, and Mattias Ulbrich | Proceedings of the 18th WiPSCE Conference on Primary and Secondary Computing Education Research |
Transformations de graphes décorés | Pascale Le Gall and Romain Pascual | Informatique Mathématique Une photographie en 2023 |
A SAT-Benchmark Set from the Approximation of Trigonometric Functions for SAT-based Verification | Kai Hiller and Alexander Weigl | Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions |
Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeY | Rosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich, and Wolfgang Ahrendt | Int. J. Softw. Tools Technol. Transf. 25(2) |
Formal Specification and Verification of JDK's Identity Hash Map Implementation | Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, and Alexander Weigl | Formal Aspects Comput. 35(3) |
Neue Einblicke in den Berufswahlprozess von Informatiklehrkräften | Claudia Hildebrandt, Barbara Pampel, Bernhard Standl, Franz J. Hauck, Mattias Ulbrich, and Barbara Paech | Informatikunterricht zwischen Aktualität und Zeitlosigkeit: 20. GI-Fachtagung Informatik und Schule, INFOS 2023, Volume P-336 |
Title | Author(s) | Source |
---|---|---|
Inference of graph transformation rules for the design of geometric modeling operations | Romain Pascual | Université Paris-Saclay |
A Refactoring for Data Minimisation Using Formal Verification | Florian Lanzinger, Mattias Ulbrich, and Alexander Weigl | 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA 2022) |
Why is Online Voting Still Largely a Black Box? | Michael Kirsten, Melanie Volkamer, and Bernhard Beckert | First International Workshop on Election Infrastructure Security (EIS 2022) in conjunction with ESORICS 2022: European Symposium on Research in Computer Security |
Optimized Symbolic Interval Propagation for Neural Network Verification | Philipp Kern, Marko Kleine Büning, and Carsten Sinz | 1st Workshop on Formal Verification of Machine Learning (WFVML 2022) colocated with ICML 2022: International Conference on Machine Learning |
The Karlsruhe Java Verification Suite | Jonas Klamroth, Florian Lanzinger, Wolfram Pfeifer, and Mattias Ulbrich | The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday |
Algorithmic Fairness and Secure Information Flow (Extended Abstract) | Bernhard Beckert, Michael Kirsten, and Michael Schefczyk | European Workshop on Algorithmic Fairness (EWAF '22), Lightning round track |
Formal Specification and Verification of JDK’s Identity Hash Map Implementation | Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, and Alexander Weigl | 17th International Conference on integrated Formal Methods (iFM 2022) |
Certified Verification of Relational Properties | Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, and Pascale Le Gall | 17th International Conference on integrated Formal Methods (iFM 2022) |
Inferring topological operations on generalized maps: Application to subdivision schemes | Romain Pascual, Hakim Belhaouari, Agnès Arnould, and Pascale Le Gall | Graphics and Visual Computing 6 |
Formal Specification and Verification of JDK’s Identity Hash Map Implementation (Long Version) | Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, and Alexander Weigl | Karlsruhe Institute of Technology (KIT) 1000145727 |
Inferring Interval-Valued Floating-Point Preconditions | Jonas Krämer, Lionel Blatter, Eva Darulova, and Mattias Ulbrich | 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), held as part of ETAPS 2022: European Joint Conferences on Theory and Practice of Software, Part I |
Preserving consistency in geometric modeling with graph transformations | Agnès Arnould, Hakim Belhaouari, Thomas Bellet, Pascale Le Gall, and Romain Pascual | Mathematical Structures in Computer Science 32(3) |
Topological consistency preservation with graph transformation schemes | Romain Pascual, Pascale Le Gall, Agnès Arnould, and Hakim Belhaouari | Science of Computer Programming 214 |
The counterSharp Model Counting Benchmark | Samuel Teuber and Alexander Weigl | Karlsruhe Institute of Technology 2022-02 |
Formal Methods for Trustworthy Voting Systems | Michael Kirsten | Karlsruhe Institute of Technology (KIT) (January 2022) |
Towards a Formal Approach for Data Minimization in Programs | Florian Lanzinger and Alexander Weigl | Data Privacy Management, Cryptocurrencies and Blockchain Technology |
Generalized Test Tables: A Domain-Specific Specification Language for Automated Production Systems | Bernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander Weigl | Theoretical Aspects of Computing - ICTAC 2022 |
SpecifyThis - Bridging Gaps Between Program Specification Paradigms | Wolfgang Ahrendt, Paula Herber, Marieke Huisman, and Mattias Ulbrich | Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles (ISoLA) 2022 |
Towards a Usable and Sustainable Deductive Verification Tool | Bernhard Beckert, Richard Bubel, Reiner Hähnle, and Mattias Ulbrich | Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA) 2022 |
Title | Author(s) | Source |
---|---|---|
Card-Based Cryptography Meets Formal Verification | Alexander Koch, Michael Schrempp, and Michael Kirsten | 25th International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT 2019), Part I |
Card-Based Cryptography Meets Formal Verification | Alexander Koch, Michael Schrempp, and Michael Kirsten | IACR Cryptology ePrint Archive 2019(1037) |
Formal Property-Oriented Design of Voting Rules Using Composable Modules | Karsten Diekhoff, Michael Kirsten, and Jonas Krämer | 6th International Conference on Algorithmic Decision Theory (ADT 2019), Part Short Papers |
KASTEL Industry 4.0 Demonstrator: Provably Forgetting Information in PLC software | Alexander Weigl | Presentation in the KASTEL Seminar, Karlsruhe, Germany, October 10 |
User Interaction in Deductive Interactive Program Verification | Sarah Caecilia Grebing | Karlsruhe Institute of Technology (October 2019) |
Smart Contracts: Application Scenarios for Deductive Program Verification | Bernhard Beckert, Jonas Schiffl, and Mattias Ulbrich | 1st Workshop on Formal Methods for Blockchains (FMBC 2019) hosted by the 3rd Formal Methods World Congress (FM’19) |
GI Elections with POLYAS: a Road to End-to-End Verifiable Elections | Bernhard Beckert, Achim Brelle, Rüdiger Grimm, Nicolas Huber, Michael Kirsten, Ralf Küsters, Jörn Müller‑Quade, Maximilian Noppel, Kai Reinhard, Jonas Schwab, Rebecca Schwerdt, Tomasz Truderung, Melanie Volkamer, and Cornelia Winter | Fourth International Joint Conference on Electronic Voting (E-Vote-ID 2019) |
Relational properties for specification and verification of C programs in Frama-C | Lionel Blatter | Université Paris-Saclay (September 2019) |
Using Relational Verification for Program Slicing | Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich | 17th International Conference on Software Engineering and Formal Methods (SEFM 2019) |
Understanding Counterexamples for Relational Properties with DIbugger | Mihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, and Bernhard Beckert | Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019) |
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning | Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos, and Mattias Ulbrich | abs/1907.03523 2019 |
Seamless Interactive Program Verification | Sarah Grebing, Jonas Klamroth, and Mattias Ulbrich | 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019) |
Formal Verification of Evolutionary Changes | Bernhard Beckert, Jakob Mund, Mattias Ulbrich, and Alexander Weigl | Managed Software Evolution |
Using Relational Verification for Program Slicing | Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich | Department of Informatics, Karlsruhe Institute of Technology 2019,5 |
VerifyThis – Verification Competition with a Human Factor | Gidon Ernst, Marieke Huisman, Wojciech Mostowski, and Mattias Ulbrich | 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019) |
Modular Verification of JML Contracts Using Bounded Model Checking | Jonas Klamroth | Karlsruhe Institute of Technology (March 2019) |
Efficient unpacking of required software from CERNVM-FS | Samuel Teuber | Zenodo 2019-02 |
Verification-based Test Case Generation for Information-Flow Properties | Mihai Herda, Shmuel Tyszberowicz, Joachim Müssig, and Bernhard Beckert | 34rd Annual ACM Symposium on Applied Computing (SAC 2019) |
Learning from Evolution for Evolution | Stefan Kögel, Matthias Tichy, Abhishek Chakraborty, Alexander Fay, Birgit Vogel‑Heuser, Christopher Haubeck, Gabriele Taentzer, Timo Kehrer, Jan Ladiges, Lars Grunske, Mattias Ulbrich, Safa Bougouffa, Sinem Getir, Suhyun Cha, Udo Kelter, Winfried Lamersdorf, Kiana Busch, Robert Heinrich, and Sandro Koch | Managed Software Evolution |
Addressed Challenges | Reiner Jung, Lukas Märtin, Jan Ole Johanssen, Barbara Paech, Malte Lochau, Thomas Thüm, Kurt Schneider, Matthias Tichy, and Mattias Ulbrich | Managed Software Evolution |
Title | Author(s) | Source |
---|---|---|
Dynamic Logic for Java | Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß | Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations |
Deductive Software Verification - The KeY Book: From Theory to Practice | Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich | Lecture Notes in Computer Science 10001 (Springer 2016) |
Formal Verification with KeY: A Tutorial | Bernhard Beckert, Reiner Hähnle, Martin Hentschel, and Peter H. Schmitt | Deductive Software Verification - The KeY Book: From Theory to Practice, Part IV: The KeY System in Action |
Proof-based Test Case Generation | Wolfgang Ahrendt, Christoph Gladisch, and Mihai Herda | Deductive Software Verification - The KeY Book: From Theory to Practice, Part III: From Verification to Analysis |
First-Order Logic | Peter H. Schmitt | Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations |
Theories | Peter H. Schmitt and Richard Bubel | Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations |
Formal Specification with the Java Modeling Language | Marieke Huisman, Wolfgang Ahrendt, Daniel Grahl, and Martin Hentschel | Deductive Software Verification - The KeY Book: From Theory to Practice, Part II: Specification and Verification |
Functional Verification and Information Flow Analysis of an Electronic Voting System | Daniel Grahl and Christoph Scheben | Deductive Software Verification - The KeY Book: From Theory to Practice, Part V: Case Studies |
Information Flow Analysis | Christoph Scheben and Simon Greiner | Deductive Software Verification - The KeY Book: From Theory to Practice, Part III: From Verification to Analysis |
Using the KeY Prover | Wolfgang Ahrendt and Sarah Grebing | Deductive Software Verification - The KeY Book: From Theory to Practice, Part IV: The KeY System in Action |
From Specification to Proof Obligations | Daniel Grahl and Mattias Ulbrich | Deductive Software Verification - The KeY Book: From Theory to Practice, Part II: Specification and Verification |
Modular Specification and Verification | Daniel Grahl, Richard Bubel, Wojciech Mostowski, Peter H. Schmitt, Mattias Ulbrich, and Benjamin Weiß | Deductive Software Verification - The KeY Book: From Theory to Practice, Part II: Specification and Verification |
Proof Search with Taclets | Philipp Rümmer and Mattias Ulbrich | Deductive Software Verification - The KeY Book: From Theory to Practice, Part I: Foundations |
Computing Specification-Sensitive Abstractions for Program Verification | Tianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, and Mana Taghdiri | Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016) |
Relational Program Reasoning Using Compiler IR | Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich | 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Revised Selected Papers |
Deductive Verification of Legacy Code | Bernhard Beckert, Thorsten Bormer, and Daniel Grahl | 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), Volume I: Foundational Techniques |
Sound Probabilistic #SAT with Projection | Vladimir Klebanov, Alexander Weigl, and Jörg Weisbarth | 14th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2016) |
Practical Detection of Entropy Loss in Pseudo-Random Number Generators: Extended Version | Felix Dörre and Vladimir Klebanov | Department of Informatics, Karlsruhe Institute of Technology 2016,12 |
Practical Detection of Entropy Loss in Pseudo-Random Number Generators | Felix Dörre and Vladimir Klebanov | 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS 2016) |
Efficient SAT-based Pre-image Enumeration for Quantitative Information Flow in Programs | Alexander Weigl | 5th International Workshop on Quantitative Aspects of Security Assurance (QASA 2016) |
Dynamic Dispatch for Method Contracts through Abstract Predicates | Wojciech Mostowski and Mattias Ulbrich | Transactions on Modularity and Composition 1 |
A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory Automation | Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten, Franziska Wiebe, Bernhard Beckert, and Birgit Vogel‑Heuser | IEEE International Symposium on Assembly and Manufacturing (ISAM 2016) |
Automated Verification for Functional and Relational Properties of Voting Rules | Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and Mattias Ulbrich | Sixth International Workshop on Computational Social Choice (COMSOC 2016) |
Deductive Verification with Relational Properties | Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, and Virgile Prevosto | CoRR abs/1606.00678 |
Non-Interference with What-Declassification in Component-Based Systems | Simon Greiner and Daniel Grahl | 29th IEEE Computer Security Foundations Symposium (CSF 2016) |
Dual Pivot Quicksort: Specification and Verification Using KeY | Jonas Schiffl | Karlsruhe Institute of Technology (May 2016) |
A Natural Language Dialog System Based on Active Ontologies | Alexander Wachtel, Jonas Klamroth, and Walter F. Tichy | The Ninth International Conference on Advances in Computer-Human Interactions (ACHI 2016) |
Praxis der Forschung: Eine Lehrveranstaltung des forschungsnahen Lehrens und Lernens in der Informatik am KIT | Matthias Budde, Sarah Grebing, Erik Burger, Max Kramer, Bernhard Beckert, Michael Beigl, and Ralf Reussner | Neues Handbuch Hochschullehre 74, Volume A: Lehren und Lernen, Part 3: Neue Lehr- und Lernkonzepte |
Security in E-Voting | Daniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel, and Richard Gay | Poster at the 25th USENIX Security Symposium |
Title | Author(s) | Source |
---|---|---|
A Dynamic Logic for Deductive Verification of Concurrent Programs | Bernhard Beckert and Vladimir Klebanov | 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007) |
The KeY System 1.0 (Deduction Component) | Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. Schmitt | 21st International Conference on Automated Deduction (CADE-21) |
How C differs from Java for Symbolic Program Execution | Christoph Gladisch | C/C++ Verification Workshop |
A Fixpoint-based Rule for Loop Verification | Daniel Bruns | Universität Karlsruhe (June 2007) |
Preface: Special Issue on Automated Reasoning with Analytic Tableaux and Related Methods | Bernhard Beckert and Lawrence C. Paulson | Journal of Automated Reasoning 38(1-3) |
White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing | Bernhard Beckert and Christoph Gladisch | First International Conference on Tests and Proofs (TAP 2007), Revised Papers |
KeY: A Formal Method for Object-Oriented Systems | Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt | IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2007) |
4th International Verification Workshop (VERIFY '07) co-located with CADE-21: the 21st Conference on Automated Deduction | Bernhard Beckert | CEUR Workshop Proceedings 259 (CEUR-WS.org 2007) |
A Dynamic Logic for Deductive Verification of Concurrent Java Programs With Condition Variables | Bernhard Beckert and Vladimir Klebanov | 1st International Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP 2007), Satellite Workshop of CONCUR 2007: the 18th International Conference on Concurrency Theory |
Verification of Object-Oriented Software: The KeY Approach | Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt | Lecture Notes in Computer Science 4334 (Springer 2007) |
Dynamic Logic | Bernhard Beckert, Vladimir Klebanov, and Steffen Schlager | Verification of Object-Oriented Software: The KeY Approach, Part I: Foundations |
Formal Specification | Andreas Roth and Peter H. Schmitt | Verification of Object-Oriented Software: The KeY Approach, Part II: Expressing and Formalising Requirements |
Proof Reuse | Vladimir Klebanov | Verification of Object-Oriented Software: The KeY Approach, Part III: Using the KeY System |
Software Verification for Java 5 | Mattias Ulbrich | Fakultät für Informatik, Universität Karlsruhe (January 2007) |
Title | Author(s) | Source |
---|---|---|
Verifying Object-Oriented Programs with KeY: A Tutorial | Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, and Peter H. Schmitt | 5th International Symposium on Formal Methods for Components and Objects (FMCO 2006), Revised Lectures |
Integrating Object-oriented Design and Deductive Verification of Software, Tutorial Abstract | Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt | 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006) |
Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program Verification | Bernhard Beckert and André Platzer | Third International Joint Conference on Automated Reasoning (IJCAR 2006) |
A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces | Bernhard Beckert and Gerd Beuster | Eight International Conference on Formal Engineering Methods (ICFEM 2006) |
Intelligent Systems and Formal Methods in Software Engineering | Bernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, and Sriram K. Rajamani | IEEE Intelligent Systems 21(6) |
Must Program Verification Systems and Calculi be Verified? | Bernhard Beckert and Vladimir Klebanov | 3rd International Verification Workshop (VERIFY 2006), Workshop at Federated Logic Conferences (FLoC) |
Guaranteeing Consistency in Text-Based Human-Computer Interaction | Bernhard Beckert and Gerd Beuster | International Workshop on Formal Methods for Interactive Systems (FMIS 2006) |
Title | Author(s) | Source |
---|---|---|
Software Verification with Integrated Data Type Refinement for Integer Arithmetic | Bernhard Beckert and Steffen Schlager | 4th International Conference on Integrated Formal Methods (IFM 2004) |
Taclets: A New Paradigm for Constructing Interactive Theorem Provers | Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen Schlager | Department of Computer Science, University of Koblenz 9-2004 |
Email Client Specification | Bernhard Beckert, Gerd Beuster, and Pia Breuer | Verisoft Project #6 |
Taclets: A New Paradigm for Constructing Interactive Theorem Provers | Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen Schlager | Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales, Serie A: Matemáticas (RACSAM) 98(1) |
Proof Reuse for Deductive Program Verification | Bernhard Beckert and Vladimir Klebanov | 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004) |
Formal Specification of Security-relevant Properties of User Interfaces | Bernhard Beckert and Gerd Beuster | Department of Computer Science, University of Koblenz 10-2004 |
Formal Specification of Security-relevant Properties of User Interfaces | Bernhard Beckert and Gerd Beuster | 3rd International Workshop on Critical Systems Development with UML |
A JMM-Faithful Non-interference Calculus for Java | Vladimir Klebanov | 4th International Workshop on Scientific Engineering of Distributed Java Applications (FIDJI 2004) |
Title | Author(s) | Source |
---|---|---|
A Program Logic for Handling JAVA CARD's Transaction Mechanism | Bernhard Beckert and Wojciech Mostowski | 6th International Conference on Fundamental Approaches to Software Engineering (FASE 2003), held as part of ETAPS 2003: the Joint European Conferences on Theory and Practice of Software |
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 | Department of Computing Science, Chalmers University and Göteborg University, Göteborg, Sweden No. 2003-5 |
Depth-first Proof Search without Backtracking for Free-variable Clausal Tableaux | Bernhard Beckert | Journal of Symbolic Computation 36(1-2) |
Program Verification Using Change Information | Bernhard Beckert and Peter H. Schmitt | 1st International Conference on Software Engineering and Formal Methods (SEFM 2003) |
Title | Author(s) | Source |
---|---|---|
The KeY System: Integrating Object-Oriented Design and Formal Methods | Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, and Peter H. Schmitt | 5th International Conference on Fundamental Approaches to Software Engineering (FASE 2002) held as part of ETAPS 2002: the Joint European Conferences on Theory and Practice of Software |
Integer Arithmetic in the Specification and Verification of Java Programs | Bernhard Beckert and Steffen Schlager | Workshop on Tools for System Design and Verification (FM-TOOLS 2002) |
Translating the Object Constraint Language into First-order Predicate Logic | Bernhard Beckert, Uwe Keller, and Peter H. Schmitt | VERIFY Workshop (VERIFY 2002) at FLoC 2002: Federated Logic Conferences |
Title | Author(s) | Source |
---|---|---|
A Sequent Calculus for First-order Dynamic Logic with Trace Modalities | Bernhard Beckert and Steffen Schlager | First International Joint Conference on Automated Reasoning (IJCAR 2001) |
Handling Java's Abrupt Termination in a Sequent Calculus for Dynamic Logic | Bernhard Beckert and Bettina Sasse | IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development (PMD '01) |
Free-variable Tableaux for Propositional Modal Logics | Bernhard Beckert and Rajeev Goré | Studia Logica 69(1) |
A Dynamic Logic for the Formal Verification of Java Card Programs | Bernhard Beckert | International Workshop on Java on Smart Cards: Programming and Security (Java Card 2000), Revised Papers |
IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development (PMD '01) | Bernhard Beckert, Robert France, Reiner Hähnle, and Bart Jacobs | Technical Report DII 07/01, Dipartimento di Ingegneria dell'Informazione, Università degli Studi di Siena 2001 |
An Extension of Dynamic Logic for Modelling OCL's @pre Operator | Thomas Baar, Bernhard Beckert, and Peter H. Schmitt | Fourth Andrei Ershov International Conference on Perspectives of System Informatics |