Veröffentlichungen

Lieber nach Kategorien gruppieren.

2024
Titel Autor(en) Quelle
Formally Verifying an Efficient Sorter, extended versionBernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler und Sascha Witt
2023
Titel Autor(en) Quelle
Scalable and Precise Refinement Types for Imperative LanguagesFlorian Lanzinger, Joshua Bachmeier, Mattias Ulbrich und Werner DietliFM 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 MachinesAnnika Vielsack, Miriam Klein, Thomas Niesenhaus und Mattias UlbrichProceedings of the 18th WiPSCE Conference on Primary and Secondary Computing Education Research
Transformations de graphes décorésPascale Le Gall und Romain PascualInformatique Mathématique Une photographie en 2023
A SAT-Benchmark Set from the Approximation of Trigonometric Functions for SAT-based VerificationKai Hiller und Alexander WeiglProceedings of SAT Competition 2023 : Solver, Benchmark and Proof Checker Descriptions
2022
Titel Autor(en) Quelle
Inference of graph transformation rules for the design of geometric modeling operationsRomain PascualUniversité Paris-Saclay
A Refactoring for Data Minimisation Using Formal VerificationFlorian Lanzinger, Mattias Ulbrich und Alexander Weigl11th 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 und Bernhard BeckertFirst 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 VerificationPhilipp Kern, Marko Kleine Büning und Carsten Sinz1st Workshop on Formal Verification of Machine Learning (WFVML 2022) colocated with ICML 2022: International Conference on Machine Learning
The Karlsruhe Java Verification SuiteJonas Klamroth, Florian Lanzinger, Wolfram Pfeifer und Mattias UlbrichThe 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 und Michael SchefczykEuropean Workshop on Algorithmic Fairness (EWAF '22), Lightning round track
Formal Specification and Verification of JDK’s Identity Hash Map ImplementationMartin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich und Alexander Weigl17th International Conference on integrated Formal Methods (iFM 2022)
Certified Verification of Relational PropertiesLionel Blatter, Nikolai Kosmatov, Virgile Prevosto und Pascale Le Gall17th International Conference on integrated Formal Methods (iFM 2022)
Inferring topological operations on generalized maps: Application to subdivision schemesRomain Pascual, Hakim Belhaouari, Agnès Arnould und Pascale Le GallGraphics 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 und Alexander WeiglKarlsruhe Institute of Technology (KIT) 1000145727
Inferring Interval-Valued Floating-Point PreconditionsJonas Krämer, Lionel Blatter, Eva Darulova und Mattias Ulbrich28th 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, Teil I
Preserving consistency in geometric modeling with graph transformationsAgnès Arnould, Hakim Belhaouari, Thomas Bellet, Pascale Le Gall und Romain PascualMathematical Structures in Computer Science 32(3)
Topological consistency preservation with graph transformation schemesRomain Pascual, Pascale Le Gall, Agnès Arnould und Hakim BelhaouariScience of Computer Programming 214
The counterSharp Model Counting BenchmarkSamuel Teuber und Alexander WeiglKarlsruhe Institute of Technology 2022-02
Formal Methods for Trustworthy Voting SystemsMichael KirstenKarlsruhe Institute of Technology (KIT) (Januar 2022)
Towards a Formal Approach for Data Minimization in ProgramsFlorian Lanzinger und Alexander WeiglData Privacy Management, Cryptocurrencies and Blockchain Technology
2021
Titel Autor(en) Quelle
Upper Bound Computation of Information Leakages for Unbounded RecursionJohannes Bechberger und Alexander Weigl19th International Conference on Software Engineering and Formal Methods (SEFM 2021)
Formal Specification and Verification for Automated Production SystemsAlexander Sebastian WeiglKarlsruhe Institute of Technology (KIT) (Dezember 2021)
Geometric Path Enumeration for Equivalence Verification of Neural NetworksSamuel Teuber, Marko Kleine Büning, Philipp Kern und Carsten Sinz33rd IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2021)
Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationFlorian Lanzinger, Alexander Weigl, Mattias Ulbrich und Werner DietlProceedings of the ACM on programming languages 5(OOPSLA)
Quantifying Software Reliability via Model-CountingSamuel Teuber und Alexander Weigl18th International Conference on Quantitative Evaluation of Systems (QEST 2021)
Towards Correct Smart Contracts: A Case Study on Formal Verification of Access ControlJonas Schiffl, Matthias Grundmann, Marc Leinweber, Oliver Stengele, Sebastian Friebe und Bernhard BeckertSACMAT '21: Proceedings of the 26th ACM Symposium on Access Control Models and Technologies
Runtime Verification of Generalized Test TablesAlexander Weigl, Mattias Ulbrich, Shmuel S. Tyszberowicz und Jonas KlamrothNASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings
Table-based formal specification approaches for control engineers—empirical studies of usabilitySuhyun Cha, Birgit Vogel‑Heuser, Alexander Weigl, Mattias Ulbrich und Bernhard BeckertIET Cyber-Physical Systems: Theory and Applications
Card-Based Cryptography Meets Formal VerificationAlexander Koch, Michael Schrempp und Michael KirstenNew Generation Computing 39(1)
Deductive Verification of Floating-Point Java Programs in KeYRosa Abbasi, Jonas Schiffl, Eva Darulova, Mattias Ulbrich und Wolfgang Ahrendt27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), held as part of ETAPS 2021: European Joint Conferences on Theory and Practice of Software, Teil II
Property Types in Java: Combining Type Systems and Deductive VerificationFlorian LanzingerKarlsruher Institut für Technologie (Februar 2021)
Modeling and Verifying Access Control for Ethereum Smart ContractsFrederik Reiche, Jonas Schiffl, Bernhard Beckert, Robert Heinrich und Ralf ReussnerKarlsruher Institut für Technologie (KIT) 1000129607
Reconstructing Z3 proofs in KeY: There and back againWolfram Pfeifer, Jonas Schiffl und Mattias UlbrichProceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2021), co-located with ECOOP/ISSTA 2021, Online, 13 July 2021
Reconstructing Z3 Proofs With KeYWolfram PfeiferKarlsruhe Institute of Technology (Januar 2021)
2020
Titel Autor(en) Quelle
Integration of Static and Dynamic Analysis Techniques for Checking NoninterferenceBernhard Beckert, Mihai Herda, Michael Kirsten und Shmuel TyszberowiczDeductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Teil V: Integration of Verification Techniques
Usability Recommendations for User Guidance in Deductive Program VerificationSarah Grebing und Mattias UlbrichDeductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Teil IV: Feasibility and Usability
Formal Analysis of Smart Contracts: Applying the KeY SystemJonas Schiffl, Wolfgang Ahrendt, Bernhard Beckert und Richard BubelDeductive Software Verification: Future Perspectives
Deductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeYWolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle und Mattias UlbrichLecture Notes in Computer Science 12345 (Springer 2020)
The VerifyThis Collaborative Long Term ChallengeMarieke Huisman, Raúl Monti, Mattias Ulbrich und Alexander WeiglDeductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY, Teil IV: Feasibility and Usability
Design- and Evaluation-Concept for Teaching and Learning Laboratories in Informatics Teacher EducationBernhard Standl, Anette Bentz, Mattias Ulbrich, Annika Vielsack und Ingo WagnerInformatics in Schools. Engaging Learners in Computational Thinking - 13th International Conference, ISSEP 2020, Tallinn, Estonia, November 16-18, 2020, Proceedings
Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der InformatikMichael Kirsten, Robert Bauer, Andreas Fried, Bernhard Beckert, Michael Beigl, Gregor Snelting und Martina ZitterbartCampustage 2020 „Lehre^Forschung-PLUS“
Modular Verification of JML Contracts Using Bounded Model CheckingBernhard Beckert, Michael Kirsten, Jonas Klamroth und Mattias Ulbrich9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Teil I: Verification Principles
Modular Regression Verification for Reactive SystemsAlexander Weigl, Mattias Ulbrich und Daniel Lentzsch9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Teil II: Engineering Principles
Specifying Framing Conditions for Smart ContractsBernhard Beckert und Jonas SchifflISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation
Verifying Equivalence Properties of Neural Networks with ReLU Activation FunctionsMarko Kleine Büning, Philipp Kern und Carsten Sinz26th International Conference on Principles and Practice of Constraint Programming (CP 2020)
An Incremental Abstraction Scheme for Solving Hard SMT-Instances over Bit-VectorsSamuel Teuber, Marko Kleine Büning und Carsten SinzCoRR abs/2008.10061
VerifyThis Long-term Challenge 2020: Proceedings of the Online-EventMarieke Huisman, Raúl E. Monti, Mattias Ulbrich und Alexander WeiglInstitut für Theoretische Informatik (ITI), KIT 2020
Verified Construction of Fair Voting RulesKarsten Diekhoff, Michael Kirsten und Jonas Krämer29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019), Revised Selected Papers
Relational Test Tables: A Practical Specification Language for Evolution and SecurityAlexander Weigl, Mattias Ulbrich, Suhyun Cha, Bernhard Beckert und Birgit Vogel‑HeuserFormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, July 13, 2020
On the Preservation of the Trust by Regression Verification of PLC software for Cyber-Physical Systems of SystemsSuhyun Cha, Mattias Ulbrich, Alexander Weigl, Bernhard Beckert, Kathrin Land und Birgit Vogel‑Heuser17th IEEE International Conference on Industrial Informatics (INDIN 2019)
Combining Static and Dynamic Program Analysis Techniques for Checking Relational PropertiesMihai HerdaKarlsruhe Institute of Technology (KIT) (Januar 2020)
2019
Titel Autor(en) Quelle
Card-Based Cryptography Meets Formal VerificationAlexander Koch, Michael Schrempp und Michael Kirsten25th International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT 2019), Teil I
Card-Based Cryptography Meets Formal VerificationAlexander Koch, Michael Schrempp und Michael KirstenIACR Cryptology ePrint Archive 2019(1037)
Formal Property-Oriented Design of Voting Rules Using Composable ModulesKarsten Diekhoff, Michael Kirsten und Jonas Krämer6th International Conference on Algorithmic Decision Theory (ADT 2019), Teil Short Papers
KASTEL Industry 4.0 Demonstrator: Provably Forgetting Information in PLC softwareAlexander WeiglPresentation in the KASTEL Seminar, Karlsruhe, Germany, October 10
User Interaction in Deductive Interactive Program VerificationSarah Caecilia GrebingKarlsruhe Institute of Technology (Oktober 2019)
Smart Contracts: Application Scenarios for Deductive Program VerificationBernhard Beckert, Jonas Schiffl und Mattias Ulbrich1st 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 ElectionsBernhard 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 und Cornelia WinterFourth International Joint Conference on Electronic Voting (E-Vote-ID 2019)
Relational properties for specification and verification of C programs in Frama-CLionel BlatterUniversité Paris-Saclay (September 2019)
Using Relational Verification for Program SlicingBernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch und Mattias Ulbrich17th International Conference on Software Engineering and Formal Methods (SEFM 2019)
Understanding Counterexamples for Relational Properties with DIbuggerMihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick und Bernhard BeckertSixth 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 ReasoningEmanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos und Mattias Ulbrich abs/1907.03523 2019
Seamless Interactive Program VerificationSarah Grebing, Jonas Klamroth und Mattias Ulbrich11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)
Formal Verification of Evolutionary ChangesBernhard Beckert, Jakob Mund, Mattias Ulbrich und Alexander WeiglManaged Software Evolution
Using Relational Verification for Program SlicingBernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch und Mattias UlbrichDepartment of Informatics, Karlsruhe Institute of Technology 2019,5
VerifyThis – Verification Competition with a Human FactorGidon Ernst, Marieke Huisman, Wojciech Mostowski und Mattias Ulbrich25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019)
Modular Verification of JML Contracts Using Bounded Model CheckingJonas KlamrothKarlsruhe Institute of Technology (März 2019)
Efficient unpacking of required software from CERNVM-FSSamuel TeuberZenodo 2019-02
Verification-based Test Case Generation for Information-Flow PropertiesMihai Herda, Shmuel Tyszberowicz, Joachim Müssig und Bernhard Beckert34rd Annual ACM Symposium on Applied Computing (SAC 2019)
Learning from Evolution for EvolutionStefan 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 und Sandro KochManaged Software Evolution
Addressed ChallengesReiner Jung, Lukas Märtin, Jan Ole Johanssen, Barbara Paech, Malte Lochau, Thomas Thüm, Kurt Schneider, Matthias Tichy und Mattias UlbrichManaged Software Evolution
2018
Titel Autor(en) Quelle
Specification and Verification of Hyperledger Fabric ChaincodeJonas SchifflKarlsruhe Institute of Technology (Dezember 2018)
Formal Specification and Verification of Hyperledger Fabric ChaincodeBernhard Beckert, Mihai Herda, Michael Kirsten und Jonas Schiffl3rd Symposium on Distributed Ledger Technology (SDLT-2018) co-located with ICFEM 2018: the 20th International Conference on Formal Engineering Methods
A Uniform Information-Flow-Security Benchmark Suite for Source Code and BytecodeTobias Hamann, Mihai Herda, Heiko Mantel, Martin Mohr, David Schneider und Markus Tasch23rd Nordic Conference on Secure IT Systems (NordSec 2018)
Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow ControlBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten und Marko Kleine Büning20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018)
Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPUSuhyun Cha, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert und Birgit Vogel‑HeuserAutomatisierungstechnik Special Issue
Trends in Relational Program VerificationBernhard Beckert und Mattias UlbrichPrincipled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday
Towards a Notion of Coverage for Incomplete Program-Correctness ProofsBernhard Beckert, Mihai Herda, Stefan Kobischke und Mattias Ulbrich8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018), Teil II: A Broader View on Verification: From Static to Runtime and Back
Achieving delta description for the system software of an automated production evolution based on partially inferenced modelSuhyun Cha, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert und Birgit Vogel‑Heuser14th IEEE International Conference on Automation Science and Engineering (CASE 2018)
Towards automatic argumentation about voting rulesMichael Kirsten und Olivier Cailloux4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)
Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification – Lessons LearnedSarah Grebing, An Thuy Tien Luong und Alexander Weigl13th International Workshop on User Interfaces for Theorem Provers (UITP 2018)
Efficient Verification of Programs with Complex Data Structures Using SMT SolversTianhai LiuKarlsruhe Institute of Technology (Juli 2018)
Relational Equivalence Proofs Between Imperative and MapReduce AlgorithmsBernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich und Alexander Weigl10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018)
Static and Dynamic Verification of Relational Properties on Self-composed C CodeLionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto und Guillaume Petiot12th International Conference on Tests and Proofs (TAP 2018) held as part of STAF 2018: Software Technologies - Applications and Foundations
Using Dependence Graphs to Assist Verification and Testing of Information-Flow PropertiesMihai Herda, Shmuel Tyszberowicz und Bernhard Beckert12th International Conference on Tests and Proofs (TAP 2018)
Automating Regression Verification of Pointer Programs by Predicate AbstractionVladimir Klebanov, Philipp Rümmer und Mattias UlbrichFormal Methods in System Design 52(3)
Proving Equivalence Between Imperative and MapReduce Implementations Using Program TransformationsBernhard Beckert, Timo Bingmann, Moritz Kiefer, Peter Sanders, Mattias Ulbrich und Alexander WeiglThird Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (MARS/VPT@ETAPS 2018)
Debugging Program Verification Proof Scripts (Tool Paper)Bernhard Beckert, Sarah Grebing und Alexander WeiglCoRR abs/1804.04402
A Framework for Non-Interference in Component-Based SystemsSimon GreinerKarlsruhe Institute of Technology (April 2018)
A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program VerificationFlorian LanzingerKarlsruher Institut für Technologie (April 2018)
Program Equivalence (Dagstuhl Seminar 18151)Shuvendu K. Lahiri, Andrzej Murawski, Ofer Strichman und Mattias UlbrichDagstuhl Reports 8(4)
Experience Report: Formal Methods in Material ScienceBernhard Beckert, Britta Nestler, Moritz Kiefer, Michael Selzer und Mattias UlbrichCoRR abs/1802.02374
Self-composition to Prove Relational Properties in Annotated C ProgramLionel Blatter, Nikolai Kosmatov, Pascale Le Gall und Virgile PrevostoCoRR abs/1801.06876
Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPUSuhyun Cha, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert und Birgit Vogel‑HeuserAutomatisierungstechnik 66(10)
2017
Titel Autor(en) Quelle
Model-Driven Specification and Analysis of Confidentiality in Component-Based SystemsMax E. Kramer, Martin Hecker, Simon Greiner, Kaibin Bao und Kateryna YurchenkoDepartment of Informatics, Karlsruhe Institute of Technology 2017,12
VerifyThis 2017: A Program Verification CompetitionMarieke Huisman, Rosemary Monahan, Wojciech Mostowski, Peter Müller und Mattias UlbrichKarlsruhe Institute of Technology 2017,10
An Interaction Concept for Program Verification Systems with Explicit Proof ObjectBernhard Beckert, Sarah Grebing und Mattias UlbrichHardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017)
An Introduction to Voting Rule VerificationBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Carsten SchürmannTrends in Computational Social Choice, Teil II: Techniques
A novel model-based testing approach for software product linesFerruccio Damiani, David Faitelson, Christoph Gladisch und Shmuel TyszberowiczSoftware and System Modeling 16(4)
SemSlice: Exploiting Relational Verification for Automatic Program SlicingBernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch und Mattias Ulbrich13th International Conference on integrated Formal Methods (iFM 2017)
Modular Verification of Information Flow Security in Component-Based SystemsSimon Greiner, Martin Mohr und Bernhard Beckert15th International Conference on Software Engineering and Formal Methods (SEFM 2017)
Generalised Test Tables: A Practical Specification Language for Reactive SystemsBernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel‑Heuser und Alexander Weigl13th International Conference on integrated Formal Methods (iFM 2017)
Relational Program Reasoning Using Compiler IR – Combining Static Verification and Dynamic AnalysisMoritz Kiefer, Vladimir Klebanov und Mattias UlbrichJournal of Automated Reasoning 60(3)
Formal Fairness Properties in Network Routing Based on a Resource Allocation ModelAlmut Demel und Michael Kirsten9th Workshop on Logical Aspects of Multi-Agent Systems (LAMAS 2017) affiliated with CSL 2017: the 26th EACSL Annual Conference on Computer Science Logic
RIFL 1.1: A Common Specification Language for Information-Flow RequirementsThomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider und Markus TaschTU Darmstadt TUD-CS-2017-0225
A Mechanizable First-Order Theory of OrdinalsPeter H. Schmitt26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017)
Generation of Monitoring Functions in Production Automation Using Test SpecificationsSuhyun Cha, Sebastian Ulewicz, Birgit Vogel‑Heuser, Alexander Weigl, Mattias Ulbrich und Bernhard Beckert15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive SystemsAlexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert und Birgit Vogel‑Heuser15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Modular Verification of Information Flow Security in Component-Based Systems – Proofs and Proof of ConceptSimon Greiner, Martin Mohr und Bernhard BeckertDepartment of Informatics, Karlsruhe Institute of Technology 2017,9
Specifying and Verifying Real-World Java Code with KeY - Case Study java.math.BigIntegerWolfram PfeiferKarlsruhe Institute of Technology (Mai 2017)
Combining Graph-Based and Deduction-Based Information-Flow AnalysisBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten und Marko Kleine Büning5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017) affiliated with ETAPS 2017: European Joint Conferences on Theory and Practice of Software
RPP: Automatic Proof of Relational Properties by Self-compositionLionel Blatter, Nikolai Kosmatov, Pascale Le Gall und Virgile Prevosto23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017) held as part of ETAPS 2017: European Joint Conferences on Theory and Practice of Software, Teil I
CoCoME with SecuritySimon Greiner und Mihai HerdaDepartment of Informatics, Karlsruhe Institute of Technology 2017,2
Natural Language User Interface For Software Engineering TasksAlexander Wachtel, Jonas Klamroth und Walter F. TichyThe Tenth International Conference on Advances in Computer-Human Interactions (ACHI 2016)
Computing Exact Loop Bounds for Bounded Program VerificationTianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert und Mana TaghdiriInternational Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2017)
Proving JDK's Dual Pivot Quicksort CorrectBernhard Beckert, Jonas Schiffl, Peter H. Schmitt und Mattias Ulbrich9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)
Automatic Margin Computation for Risk-Limiting AuditsBernhard Beckert, Michael Kirsten, Vladimir Klebanov und Carsten SchürmannFirst International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
2016
Titel Autor(en) Quelle
Dynamic Logic for JavaBernhard Beckert, Vladimir Klebanov und Benjamin WeißDeductive Software Verification - The KeY Book: From Theory to Practice, Teil I: Foundations
Deductive Software Verification - The KeY Book: From Theory to PracticeWolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt und Mattias UlbrichLecture Notes in Computer Science 10001 (Springer 2016)
Formal Verification with KeY: A TutorialBernhard Beckert, Reiner Hähnle, Martin Hentschel und Peter H. SchmittDeductive Software Verification - The KeY Book: From Theory to Practice, Teil IV: The KeY System in Action
Proof-based Test Case GenerationWolfgang Ahrendt, Christoph Gladisch und Mihai HerdaDeductive Software Verification - The KeY Book: From Theory to Practice, Teil III: From Verification to Analysis
First-Order LogicPeter H. SchmittDeductive Software Verification - The KeY Book: From Theory to Practice, Teil I: Foundations
TheoriesPeter H. Schmitt und Richard BubelDeductive Software Verification - The KeY Book: From Theory to Practice, Teil I: Foundations
Formal Specification with the Java Modeling LanguageMarieke Huisman, Wolfgang Ahrendt, Daniel Grahl und Martin HentschelDeductive Software Verification - The KeY Book: From Theory to Practice, Teil II: Specification and Verification
Functional Verification and Information Flow Analysis of an Electronic Voting SystemDaniel Grahl und Christoph SchebenDeductive Software Verification - The KeY Book: From Theory to Practice, Teil V: Case Studies
Information Flow AnalysisChristoph Scheben und Simon GreinerDeductive Software Verification - The KeY Book: From Theory to Practice, Teil III: From Verification to Analysis
Using the KeY ProverWolfgang Ahrendt und Sarah GrebingDeductive Software Verification - The KeY Book: From Theory to Practice, Teil IV: The KeY System in Action
From Specification to Proof ObligationsDaniel Grahl und Mattias UlbrichDeductive Software Verification - The KeY Book: From Theory to Practice, Teil II: Specification and Verification
Modular Specification and VerificationDaniel Grahl, Richard Bubel, Wojciech Mostowski, Peter H. Schmitt, Mattias Ulbrich und Benjamin WeißDeductive Software Verification - The KeY Book: From Theory to Practice, Teil II: Specification and Verification
Proof Search with TacletsPhilipp Rümmer und Mattias UlbrichDeductive Software Verification - The KeY Book: From Theory to Practice, Teil I: Foundations
Computing Specification-Sensitive Abstractions for Program VerificationTianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl und Mana TaghdiriSecond International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016)
Relational Program Reasoning Using Compiler IRMoritz Kiefer, Vladimir Klebanov und Mattias Ulbrich8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Revised Selected Papers
Deductive Verification of Legacy CodeBernhard Beckert, Thorsten Bormer und Daniel Grahl7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), Band I: Foundational Techniques
Sound Probabilistic #SAT with ProjectionVladimir Klebanov, Alexander Weigl und Jörg Weisbarth14th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2016)
Practical Detection of Entropy Loss in Pseudo-Random Number Generators: Extended VersionFelix Dörre und Vladimir KlebanovDepartment of Informatics, Karlsruhe Institute of Technology 2016,12
Practical Detection of Entropy Loss in Pseudo-Random Number GeneratorsFelix Dörre und Vladimir Klebanov23rd ACM SIGSAC Conference on Computer and Communications Security (CCS 2016)
Efficient SAT-based Pre-image Enumeration for Quantitative Information Flow in ProgramsAlexander Weigl5th International Workshop on Quantitative Aspects of Security Assurance (QASA 2016)
Dynamic Dispatch for Method Contracts through Abstract PredicatesWojciech Mostowski und Mattias UlbrichTransactions on Modularity and Composition 1
A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory AutomationSebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten, Franziska Wiebe, Bernhard Beckert und Birgit Vogel‑HeuserIEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
Automated Verification for Functional and Relational Properties of Voting RulesBernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber und Mattias UlbrichSixth International Workshop on Computational Social Choice (COMSOC 2016)
Deductive Verification with Relational PropertiesLionel Blatter, Nikolai Kosmatov, Pascale Le Gall und Virgile PrevostoCoRR abs/1606.00678
Non-Interference with What-Declassification in Component-Based SystemsSimon Greiner und Daniel Grahl29th IEEE Computer Security Foundations Symposium (CSF 2016)
Dual Pivot Quicksort: Specification and Verification Using KeYJonas SchifflKarlsruhe Institute of Technology (Mai 2016)
A Natural Language Dialog System Based on Active OntologiesAlexander Wachtel, Jonas Klamroth und Walter F. TichyThe 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 KITMatthias Budde, Sarah Grebing, Erik Burger, Max Kramer, Bernhard Beckert, Michael Beigl und Ralf ReussnerNeues Handbuch Hochschullehre 74, Band A: Lehren und Lernen, Teil 3: Neue Lehr- und Lernkonzepte
Security in E-VotingDaniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel und Richard GayPoster at the 25th USENIX Security Symposium
2015
Titel Autor(en) Quelle
A Concept for Multi-Phase Incremental Formal Verification in Robotic Guided SurgeryMattias Ulbrich, Luzie Schreiter, Sarah Grebing, Jörg Raczkowsky, Heinz Wörn und Bernhard Beckert4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2015)
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser und Alexander Weigl17th International Conference on Formal Engineering Methods (ICFEM 2015)
Non-Interference with What-Declassification in Component-Based SystemsDaniel Grahl und Simon GreinerDepartment of Informatics, Karlsruhe Institute of Technology 2015,10
Deductive Verification of Concurrent Programs and its Application to Secure Information Flow for JavaDaniel GrahlKarlsruhe Institute of Technology (Oktober 2015)
Relational Reasoning - Constraint Solving, Deduction, and Program VerificationAboubakr Achraf El GhaziKarlsruhe Institute of Technology (Oktober 2015)
Proving Equivalence between Control Software Variants for Programmable Logic Controllers - Using Regression Verification to Reduce Unneeded Variant DiversitySebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Bernhard Beckert und Birgit Vogel‑Heuser20th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2015)
Privacy Preserving Surveillance: An Interdisciplinary ApproachPascal Birnstill, Sebastian Bretthauer, Simon Greiner und Erik KrempelInternational Data Privacy Law 5(4)
Interactive Theorem Proving - Modelling the User in the Proof ProcessBernhard Beckert und Sarah GrebingWorkshop on Bridging the Gap between Human and Automated Reasoning - A workshop of the 25th International Conference on Automated Deduction (CADE-25)
Selected Challenges of Software Evolution for Automated Production SystemsBirgit Vogel‑Heuser, Stefan Feldmann, Jens Folmer, Matthias Kowal, Ina Schaefer, Jan Ladiges, Alexander Fay, Christopher Haubeck, Winfried Lamersdorf, Sascha Lity, Timo Kehrer, Matthias Tichy, Sinem Getir, Mattias Ulbrich, Vladimir Klebanov und Bernhard Beckert13th IEEE International Conference on Industrial Informatics (INDIN 2015)
Regression Verification for Java Using a Secure Information Flow CalculusBernhard Beckert, Vladimir Klebanov und Mattias Ulbrich17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin Mohr28th IEEE Computer Security Foundations Symposium (CSF 2015)
A Theorem Proving Approach to Secure Information Flow in Concurrent Programs (extended abstract)Daniel BrunsWorkshop on Foundations of Computer Security (FCS 2015)
Pseudo-Random Number Generator Verification: A Case StudyFelix Dörre und Vladimir Klebanov7th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2015)
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser und Alexander WeiglKarlsruhe Institute of Technology, Department of Informatics 2015-06
Poster: Security in E-VotingDaniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel und Richard Gay36th IEEE Symposium on Security and Privacy (S&P 2015), Poster Session
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin MohrIACR Cryptology ePrint Archive 2015(438)
First-Order Transitive Closure Axiomatization via Iterative Invariant InjectionsAboubakr Achraf El Ghazi, Mana Taghdiri und Mihai Herda7th NASA Formal Methods Symposium (NFM 2015)
Automating Regression VerificationDennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer und Mattias UlbrichMultikonferenz Software Engineering und Management 2015: Fachtagung Software Engineering (SE 2015)
Dynamic Dispatch for Method Contracts through Abstract PredicatesWojciech Mostowski und Mattias Ulbrich14th International Conference on Modularity (Modularity'15)
Specifying linked data structures in JML for combining formal verification and testingChristoph Gladisch und Shmuel TyszberowiczScience of Computer Programming 107–108
Deductive Verification of Concurrent ProgramsDaniel BrunsDepartment of Informatics, Karlsruhe Institute of Technology 2015-3
Regression Verification for Programmable Logic Controller SoftwareAlexander Sebastian WeiglKarlsruhe Institute of Technology (Januar 2015)
Axiomatization of Typed First-Order LogicPeter H. Schmitt und Mattias Ulbrich20th International Symposium on Formal Methods (FM 2015)
2014
Titel Autor(en) Quelle
Formal Verification of Voting SchemesMichael KirstenITI Beckert, Karlsruhe Institute of Technology (Dezember 2014)
Generating JML Specifications from Alloy ExpressionsDaniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri und Shmuel Tyszberowicz10th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC 2014)
Advancing Deductive Program-Level Verification for Real-World Application: Lessons Learned from an Industrial Case StudyThorsten BormerKarlsruhe Institute of Technology (Oktober 2014)
The KeY Platform for Verification and Analysis of Java ProgramsWolfgang 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 und Mattias Ulbrich6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014)
Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest SenderFlorian Böhl, Simon Greiner und Patrik Scheidecker13th International Conference on Cryptology and Network Security (CANS 2014)
Bedrohungsanalyse eines Smart-Home-Szenarios zur Visualisierung von Energieverbrauchsdaten im Vorfeld einer SteuerentscheidungAnton Hergenröder, Christian Haas, Roland Bless, Denise Dudek, Martina Zitterbart, Thomas Bräuchle, Oliver Raabe, Simon Greiner, Bernhard Beckert, Kaibin Bao und Hartmut SchmeckInstitute of Telematics, Karlsruhe Institute of Technology TM-2014-1
A Usability Evaluation of Interactive Theorem Provers Using Focus GroupsBernhard Beckert, Sarah Grebing und Florian Böhl12th International Conference on Software Engineering and Formal Methods (SEFM 2014) – Collocated Workshops: Human-Oriented Formal Methods (HOFM 2014)
Automating Regression VerificationDennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer und Mattias Ulbrich29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)
Formal Verification of an Electronic Voting SystemDaniel BrunsDepartment of Informatics, Karlsruhe Institute of Technology 2014-11
Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight MethodsBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Thomas Meumann8th International Verification Workshop (VERIFY 2014) in connection with IJCAR 2014: International Joint Conference on Automated Reasoning
Formal Specification with JMLMarieke Huisman, Wolfgang Ahrendt, Daniel Bruns und Martin HentschelDepartment of Informatics, Karlsruhe Institute of Technology 2014-10
How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem ProversBernhard Beckert, Sarah Grebing und Florian BöhlEleventh Workshop on User Interfaces for Theorem Provers (UITP 2014)
Poster: Specification and Verification of Confidentiality in Component-Based SystemsMax E. Kramer, Anton Hergenröder, Martin Hecker, Simon Greiner und Kaibin Bao35th IEEE Symposium on Security and Privacy, Poster Reception
JKelloy: A Proof Assistant for Relational Specifications of Java ProgramsAboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz und Mana Taghdiri6th NASA Formal Methods Symposium (NFM 2014)
Verifying Voting SchemesBernhard Beckert, Rajeev Goré, Carsten Schürmann, Thorsten Bormer und Jian WangJournal of Information Security and Applications (JISA) 19(2)
A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Jürgen Graf und Christoph SchebenUniversität Trier
Precise Quantitative Information Flow Analysis – A Symbolic ApproachVladimir KlebanovTheoretical Computer Science 538(0)
On Verifying Relational Specifications of Java Programs with JKelloyAboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz und Mana TaghdiriDepartment of Informatics, Karlsruhe Institute of Technology 2014,3
Towards Specification and Verification of Information Flow in Concurrent Java-like ProgramsDaniel BrunsDepartment of Informatics, Karlsruhe Institute of Technology 2014-5
Reasoning and Verification: State of the Art and Current TrendsBernhard Beckert und Reiner HähnleIntelligent Systems, IEEE 29(1)
Generating Bounded Counterexamples for KeY Proof ObligationsMihai HerdaKarlsruhe Institute of Technology (Januar 2014)
A Comparative Study of Incremental Constraint Solving Approaches in Symbolic ExecutionTianhai Liu, Mateus Araújo, Marcelo d'Amorim und Mana Taghdiri10th International Haifa Verification Conference on Hardware and Software: Verification and Testing (HVC 2014)
2013
Titel Autor(en) Quelle
Information Flow in Object-Oriented Software – Extended Version –Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt und Mattias UlbrichDepartment of Informatics, Karlsruhe Institute of Technology 2013-14
Proving Well-Definedness of JML Specifications with KeYMichael KirstenITI Schmitt, Karlsruhe Institute of Technology (November 2013)
Implementation-level verification of algorithms with KeYDaniel Bruns, Wojciech Mostowski und Mattias UlbrichInternational Journal on Software Tools for Technology Transfer (STTT) 17(6)
Specifying a Linked Data Structure in JML for Formal Verification and Runtime CheckingChristoph Gladisch und Shmuel TyszberowiczBrazilian Symposium on Formal Methods (SBMF 2013)
Secure Information Flow for Java – A Dynamic Logic Approach: Extended VersionBernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt und Mattias UlbrichDepartment of Informatics, Karlsruhe Institute of Technology 2013-10
Privacy Preserving Surveillance and the Tracking-ParadoxSimon Greiner, Pascal Birnstill, Erik Krempel, Bernhard Beckert und Jürgen Beyerer8th Security Research Conference on Future Security
Information Flow in Object-Oriented SoftwareBernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt und Mattias Ulbrich23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2013), Revised Selected Papers
Refinement-based Testing of Delta-oriented Product LinesFerruccio Damiani, Christoph Gladisch und Shmuel TyszberowiczInternational Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools (PPPJ 2013)
Heuristically Creating Test Cases for Program Verification SystemsBernhard Beckert, Thorsten Bormer und Markus Wagner10th Metaheuristics International Conference (MIC 2013)
SAT-based Analysis and Quantification of Information Flow in ProgramsVladimir Klebanov, Norbert Manthey und Christian Muise10th International Conference on Quantitative Evaluation of Systems (QEST 2013)
On the Specification and Verification of Voting SchemesBernhard Beckert, Rajeev Goré und Carsten Schürmann4th International Conference on E-Voting and Identity (Vote-ID 2013)
Reducing the Complexity of Quantified Formulas via Variable EliminationAboubakr Achraf El Ghazi, Mattias Ulbrich, Mana Taghdiri und Mihai Herda11th International Workshop on Satisfiability Modulo Theories (SMT 2013)
Analysing Vote Counting Algorithms Via Logic - And its Application to the CADE Election SystemBernhard Beckert, Rajeev Goré und Carsten Schürmann24th International Conference on Automated Deduction (CADE-24)
A Metric for Testing Program Verification SystemsBernhard Beckert, Thorsten Bormer und Markus WagnerSeventh International Conference on Tests and Proofs (TAP 2013)
Dynamic Logic with Trace SemanticsBernhard Beckert und Daniel Bruns24th International Conference on Automated Deduction (CADE-24)
Dynamic Logic for an Intermediate Language: Verification, Interaction and RefinementMattias UlbrichKarlsruhe Institute of Technology (Juni 2013)
A Dynamic Logic for Deductive Verification of Multi-Threaded ProgramsBernhard Beckert und Vladimir KlebanovFormal Aspects of Computing 25(3)
A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Jürgen Graf und Christoph SchebenGrande Region Security and Reliability Day (GRSRD 2013)
VerifyThis Verification Competition 2012 – Organizer's ReportMarieke Huisman, Vladimir Klebanov und Rosemary MonahanDepartment of Informatics, Karlsruhe Institute of Technology 2013-01
2012
Titel Autor(en) Quelle
Wirtschaftlichkeit bei der Verbesserung von Systemspezifikationen durch UML-ModellierungThomas Lauscher und Simon GreinerSignal und Draht 104(12)
Lessons Learned From Microkernel Verification: Specification is the New BottleneckChristoph Baumann, Bernhard Beckert, Holger Blasum und Thorsten BormerSeventh Conference on Systems Software Verification (SSV 2012)
Integration of Bounded Model Checking and Deductive VerificationBernhard Beckert, Thorsten Bormer, Florian Merz und Carsten SinzFormal Verification of Object-Oriented Software International Conference (FoVeOOS 2011), Revised Selected Papers
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Revised Selected PapersBernhard Beckert, Ferruccio Damiani und Dilian GurovLecture Notes in Computer Science 7421 (Springer 2012)
Dynamic Trace Logic: Definition and ProofsBernhard Beckert und Daniel BrunsDepartment of Informatics, Karlsruhe Institute of Technology 2012-10
Lessons Learned From Microkernel VerificationBernhard Beckert und Thorsten Bormer12th International Workshop on Automated Verification of Critical Systems (AVOCS 2012)
Formal Semantics of Model Fields in Annotation-based SpecificationsBernhard Beckert und Daniel BrunsKI 2012: Advances in Artificial Intelligence
Precise Quantitative Information Flow Analysis Using Symbolic Model CountingVladimir KlebanovInternational Workshop on Quantitative Aspects in Security Assurance (QASA 2012)
The KeY Approach for the Cryptographic Verification of Java Programs: A Case StudyBernhard Beckert, Daniel Bruns, Ralf Küsters, Christoph Scheben, Peter H. Schmitt und Tomasz TruderungDepartment of Informatics, Karlsruhe Institute of Technology 2012-8
Evaluating and Improving the Usability of Interactive Verification SystemsSarah GrebingUniversität Koblenz-Landau (August 2012)
Mind the Gap: Formal Verification and the Common CriteriaBernhard Beckert, Daniel Bruns und Sarah Grebing6th International Verification Workshop (VERIFY-2010)
1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012)Vladimir Klebanov, Bernhard Beckert, Armin Biere und Geoff SutcliffeCEUR Workshop Proceedings 873 (CEUR-WS.org 2012)
Evaluating the Usability of Interactive Verification SystemsBernhard Beckert und Sarah Grebing1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012)
On the Organisation of Program Verification CompetitionsMarieke Huisman, Vladimir Klebanov und Rosemary Monahan1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE 2012)
Model generation for quantified formulas with application to test data generationChristoph GladischInternational Journal on Software Tools for Technology Transfer (STTT) 14(4)
Eine formale Semantik für die Java Modeling LanguageDaniel BrunsInformatik-Spektrum 35(1)
A Proof Assistant for Alloy SpecificationsMattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi und Mana Taghdiri18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)
10th International Symposium on Formal Methods for Components and Objects (FMCO 2011), State-of-the-Art SurveyBernhard Beckert, Ferruccio Damiani, Frank de Boer und Marcello BonsangueLecture Notes in Computer Science 7542 (Springer 2012)
Bounded Program Verification Using an SMT Solver: A Case StudyTianhai Liu, Michael Nagel und Mana TaghdiriFifth IEEE International Conference on Software Testing, Verification and Validation (ICST 2012)
2011
Titel Autor(en) Quelle
On Proving Alloy Specifications using KeYMattias Ulbrich, Ulrich Geilmann, Aboubakr Achraf El Ghazi und Mana TaghdiriDepartment of Informatics, Karlsruhe Institute of Technology 2011,37
Papers Presented at the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2011)Bernhard Beckert, Ferruccio Damiani und Dilian GurovKarlsruhe Institute of Technology, Department of Informatics 2011-26
Verlässliche Software fur kritische Infrastrukturen - PrefaceBernhard Beckert und Gregor SneltingINFORMATIK 2011 Informatik schafft Communities – Beiträge der 41. Jahrestagung der Gesellschaft für Informatik e.V. (GI), Band P-192
KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit TestingBernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz und Amiram YehudaiInternational Journal of Systems Assurance Engineering and Management 2(2)
Specification of Red-black Trees: Showcasing Dynamic Frames, Model Fields and SequencesDaniel Bruns10th KeY Symposium
Formal Semantics of Model Fields Inspired by a Generalization of Hilbert's ε TermsBernhard Beckert und Daniel Bruns10th KeY Symposium
A Dual-Engine for Early Analysis of Critical SystemsAboubakr Achraf El Ghazi, Ulrich Geilmann, Mattias Ulbrich und Mana TaghdiriWorkshop on Dependable Software for Critical Infrastructures (DSCI 2011)
The 1st Verified Software Competition: Experience ReportVladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich und Benjamin Weiß17th International Symposium on Formal Methods (FM 2011)
A Dynamic Logic for Unstructured Programs with Embedded AssertionsMattias UlbrichInternational Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers
Software Security in Virtualized Infrastructures – The Smart Meter Example (Software-Sicherheit in virtualisierten Infrastrukturen – Das Beispiel der intelligenten Stromzähler)Bernhard Beckert, Dennis Hofheinz, Jörn Müller‑Quade, Alexander Pretschner und Gregor Sneltingit - Information Technology 53(3)
Verification-based software-fault detectionChristoph David GladischKarlsruhe Institute of Technology (Mai 2011)
Dynamic Frames in Java Dynamic LogicPeter H. Schmitt, Mattias Ulbrich und Benjamin WeißInternational Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers
Proving Memory Separation in a Microkernel by Code Level VerificationChristoph Baumann, Holger Blasum, Thorsten Bormer und Sergey Tverdyshev1st International Workshop on Architectures and Applications for Mixed-Criticality Systems (AMICS 2011)
Verification-based Software-fault DetectionChristoph GladischKarlsruhe Institute of Technology (Februar 2011)
International Conference on Formal Verification of Object-Oriented Software International Conference (FoVeOOS 2010), Revised Selected PapersBernhard Beckert und Claude MarchéLecture Notes in Computer Science 6528 (Springer 2011)
Improving the Usability of Specification Languages and Methods for Annotation-based VerificationBernhard Beckert, Thorsten Bormer und Vladimir Klebanov9th International Symposium on Formal Methods for Components and Objects (FMCO 2010), State-of-the-Art Survey
2010
Titel Autor(en) Quelle
Software Security in Virtualized Infrastructures – The Smart Meter ExampleBernhard Beckert, Dennis Hofheinz, Jörn Müller‑Quade, Alexander Pretschner und Gregor SneltingKarlsruhe Institute of Technology 2010-20
Test Data Generation for Programs with Quantified First-Order Logic SpecificationsChristoph Gladisch22nd IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS 2010)
Dynamic Frames in Java Dynamic Logic: Formalisation and ProofsPeter H. Schmitt, Mattias Ulbrich und Benjamin WeißDepartment of Computer Science, Karlsruhe Institute of Technology 2010-11
Towards Testing a Verifying CompilerThorsten Bormer und Markus WagnerFormal Verification of Object-Oriented Software, Papers presented at the International Conference, Band KIT-INFO-TR 2010-13
Deduktion: Von der Theorie zur AnwendungFranz Baader, Bernhard Beckert und Tobias NipkowInformatik-Spektrum 33(5)
Generating Regression Unit Tests using a Combination of Verification and Capture & ReplayBernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz und Amiram YehudaiFourth International Conference on Tests and Proofs (TAP 2010)
Satisfiability Solving and Model Generation for Quantified First-order Logic FormulasChristoph GladischFakultät für Informatik, Institut für Theoretische Informatik, ITI
Verification of Software Product Lines with Delta-Oriented SlicingDaniel Bruns, Vladimir Klebanov und Ina SchaeferFormal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers
Verification of Software Product Lines: Reducing the Effort with Delta-oriented Slicing and Proof ReuseDaniel Bruns, Vladimir Klebanov und Ina SchaeferDepartment of Informatics, Karlsruhe Institute of Technology 2010-13
Special Issue on Tests and ProofsBernhard Beckert und Reiner HähnleJournal of Automated Reasoning 45(4)
Deductive Verification of a Byzantine Agreement ProtocolRoman Krenický und Mattias UlbrichKarlsruhe Institute of Technology, Department of Informatics 2010-7
Ingredients of Operating System CorrectnessChristoph Baumann, Bernhard Beckert, Holger Blasum und Thorsten Bormerembedded world 2010 Conference
Formal Semantics for the Java Modeling LanguageDaniel BrunsInformatiktage 2010, Band S-9
Deductive Verification of System Software in the Verisoft XT ProjectBernhard Beckert und Michal MoskalKI 24(1)
Papers Presented at the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)Bernhard Beckert und Claude MarchéKarlsruhe Institute of Technology, Department of Informatics 2010-13
Practical Aspects of Automated Deduction for Program VerificationWolfgang Ahrendt, Bernhard Beckert, Martin Giese und Philipp RümmerKI 24(1)
Satisfiability Solving and Model Generation for Quantified First-Order Logic FormulasChristoph GladischInternational Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers
Mind the Gap: Formal Verification and the Common CriteriaBernhard Beckert, Daniel Bruns und Sarah Grebing6th International Verification Workshop (VERIFY 2010)
2009
Titel Autor(en) Quelle
On Essential Program Annotations and Completeness of Verifying CompilersBernhard Beckert, Thorsten Bormer und Vladimir Klebanov16th Workshop on Verified Software: Theory, Tools, and Experiments (VSTTE 2009)
Probabilistic Models for the Verification of Human-Computer InteractionBernhard Beckert und Markus WagnerKI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI
Formal Verification of a Microkernel Used in Dependable Software SystemsChristoph Baumann, Bernhard Beckert, Holger Blasum und Thorsten Bormer28th International Conference on Computer Safety, Reliability and Security
Could we have chosen a better Loop Invariant or Method Contract?Christoph GladischThird International Conference on Tests and Proofs (TAP 2009)
Verifying the PikeOS Microkernel: First Results in the Verisoft XT Avionics ProjectChristoph Baumann und Thorsten BormerDoctoral Symposium on Systems Software Verification (DS SSV'09)
Formal Semantics for the Java Modeling LanguageDaniel BrunsUniversität Karlsruhe (Juni 2009)
Extending the Reach and Power of Deductive Program VerificationVladimir KlebanovUniversität Koblenz-Landau (Juni 2009)
Better Avionics Software Reliability by Code VerificationChristoph Baumann, Bernhard Beckert, Holger Blasum und Thorsten Bormerembedded world Conference
2008
Titel Autor(en) Quelle
Verification-based Testing for Full Feasible Branch CoverageChristoph Gladisch6th IEEE International Conference on Software Engineering and Formal Methods (SEFM 08)
Elektronische Wahlen: Theoretisch möglich, praktisch undemokratischDaniel BrunsFIfF-Kommunikation 25(3)
Verification-based Test Case Generation with Loop Invariants and Method SpecificationsChristoph GladischUniversity of Koblenz-Landau
Extending KeY for the Verification of C ProgramsChristoph GladischVDM Verlag 2008
Second International Conference on Tests and Proofs (TAP 2008)Bernhard Beckert und Reiner HähnleLecture Notes in Computer Science 4966 (Springer 2008)
5th International Verification Workshop (VERIFY '08) co-located with IJCAR 2008: the 4th International Joint Conference on Automated ReasoningBernhard Beckert und Gerwin KleinCEUR Workshop Proceedings 372 (CEUR-WS.org 2008)
Editorial: Special Section on Software Engineering and Formal MethodsBernhard K. Aichernig und Bernhard BeckertSoftware and System Modeling 7(3)
Privacy Protection in an Electronic Chronicle SystemSimon Greiner und Jie Yang34th Annual IEEE Northeast Bioengineering Conference (NEBEC 2008)
Integrating Verification and Testing of Object-Oriented SoftwareChristian Engel, Christoph Gladisch, Vladimir Klebanov und Philipp RümmerSecond International Conference on Tests and Proofs (TAP 2008)
2007
Titel Autor(en) Quelle
A Dynamic Logic for Deductive Verification of Concurrent ProgramsBernhard Beckert und Vladimir Klebanov5th 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 und Peter H. Schmitt21st International Conference on Automated Deduction (CADE-21)
How C differs from Java for Symbolic Program ExecutionChristoph GladischC/C++ Verification Workshop
A Fixpoint-based Rule for Loop VerificationDaniel BrunsUniversität Karlsruhe (Juni 2007)
Preface: Special Issue on Automated Reasoning with Analytic Tableaux and Related MethodsBernhard Beckert und Lawrence C. PaulsonJournal of Automated Reasoning 38(1-3)
White-box Testing by Combining Deduction-based Specification Extraction and Black-box TestingBernhard Beckert und Christoph GladischFirst International Conference on Tests and Proofs (TAP 2007), Revised Papers
KeY: A Formal Method for Object-Oriented SystemsWolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle und Peter H. SchmittIFIP 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 DeductionBernhard BeckertCEUR Workshop Proceedings 259 (CEUR-WS.org 2007)
A Dynamic Logic for Deductive Verification of Concurrent Java Programs With Condition VariablesBernhard Beckert und Vladimir Klebanov1st 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 ApproachBernhard Beckert, Reiner Hähnle und Peter H. SchmittLecture Notes in Computer Science 4334 (Springer 2007)
Dynamic LogicBernhard Beckert, Vladimir Klebanov und Steffen SchlagerVerification of Object-Oriented Software: The KeY Approach, Teil I: Foundations
Formal SpecificationAndreas Roth und Peter H. SchmittVerification of Object-Oriented Software: The KeY Approach, Teil II: Expressing and Formalising Requirements
Proof ReuseVladimir KlebanovVerification of Object-Oriented Software: The KeY Approach, Teil III: Using the KeY System
Software Verification for Java 5Mattias UlbrichFakultät für Informatik, Universität Karlsruhe (Januar 2007)
2006
Titel Autor(en) Quelle
Verifying Object-Oriented Programs with KeY: A TutorialWolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer und Peter H. Schmitt5th International Symposium on Formal Methods for Components and Objects (FMCO 2006), Revised Lectures
Integrating Object-oriented Design and Deductive Verification of Software, Tutorial AbstractBernhard Beckert, Reiner Hähnle und Peter H. Schmitt4th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006)
Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program VerificationBernhard Beckert und André PlatzerThird International Joint Conference on Automated Reasoning (IJCAR 2006)
A Method for Formalizing, Analyzing, and Verifying Secure User InterfacesBernhard Beckert und Gerd BeusterEight International Conference on Formal Engineering Methods (ICFEM 2006)
Intelligent Systems and Formal Methods in Software EngineeringBernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball und Sriram K. RajamaniIEEE Intelligent Systems 21(6)
Must Program Verification Systems and Calculi be Verified?Bernhard Beckert und Vladimir Klebanov3rd International Verification Workshop (VERIFY 2006), Workshop at Federated Logic Conferences (FLoC)
Guaranteeing Consistency in Text-Based Human-Computer InteractionBernhard Beckert und Gerd BeusterInternational Workshop on Formal Methods for Interactive Systems (FMIS 2006)
2005
Titel Autor(en) Quelle
14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2005)Bernhard BeckertLecture Notes in Computer Science 3702 (Springer 2005)
Third International Conference on Software Engineering and Formal Methods (SEFM 2005)Bernhard K. Aichernig und Bernhard BeckertIEEE Computer Society 2005
The KeY ToolWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager und Peter H. SchmittSoftware and System Modeling 4(1)
Email Client Verification GoalsBernhard Beckert und Gerd BeusterVerisoft Project #46
An Improved Rule for While Loops in Deductive Program VerificationBernhard Beckert, Steffen Schlager und Peter H. SchmittSeventh International Conference on Formal Engineering Methods (ICFEM 2005)
Second-Order Principles in Specification Languages for Object-Oriented ProgramsBernhard Beckert und Kerry Trentelman12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Refinement and Retrenchment for Programming Language Data TypesBernhard Beckert und Steffen SchlagerFormal Aspects of Computing 17(4)
Reusing Proofs when Program Verification Systems are ModifiedBernhard Beckert, Thorsten Bormer und Vladimir KlebanovSoftware Certificate Management Workshop (SoftCeMent 2005)
TABLEAUX 2005: Position Papers and Tutorial DescriptionsBernhard BeckertUniversität Koblenz-Landau 12–2005
Verification of JCSP ProgramsVladimir Klebanov, Philipp Rümmer, Steffen Schlager und Peter H. Schmitt28th WoTUG Conference on Communicating Process Architectures (CPA 2005)
Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen SyntheseMattias UlbrichFakultät für Informatik, Universität Karlsruhe (Januar 2005)
2004
Titel Autor(en) Quelle
Software Verification with Integrated Data Type Refinement for Integer ArithmeticBernhard Beckert und Steffen Schlager4th International Conference on Integrated Formal Methods (IFM 2004)
Taclets: A New Paradigm for Constructing Interactive Theorem ProversBernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer und Steffen SchlagerDepartment of Computer Science, University of Koblenz 9-2004
Email Client SpecificationBernhard Beckert, Gerd Beuster und Pia BreuerVerisoft Project #6
Taclets: A New Paradigm for Constructing Interactive Theorem ProversBernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer und Steffen SchlagerRevista de la Real Academia de Ciencias Exactas, Físicas y Naturales, Serie A: Matemáticas (RACSAM) 98(1)
Proof Reuse for Deductive Program VerificationBernhard Beckert und Vladimir Klebanov2nd International Conference on Software Engineering and Formal Methods (SEFM 2004)
Formal Specification of Security-relevant Properties of User InterfacesBernhard Beckert und Gerd BeusterDepartment of Computer Science, University of Koblenz 10-2004
Formal Specification of Security-relevant Properties of User InterfacesBernhard Beckert und Gerd Beuster3rd International Workshop on Critical Systems Development with UML
A JMM-Faithful Non-interference Calculus for JavaVladimir Klebanov4th International Workshop on Scientific Engineering of Distributed Java Applications (FIDJI 2004)
2003
Titel Autor(en) Quelle
A Program Logic for Handling JAVA CARD's Transaction MechanismBernhard Beckert und Wojciech Mostowski6th 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 ToolWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager und Peter H. SchmittDepartment 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 TableauxBernhard BeckertJournal of Symbolic Computation 36(1-2)
Program Verification Using Change InformationBernhard Beckert und Peter H. Schmitt1st International Conference on Software Engineering and Formal Methods (SEFM 2003)
2002
Titel Autor(en) Quelle
The KeY System: Integrating Object-Oriented Design and Formal MethodsWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski und Peter H. Schmitt5th 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 ProgramsBernhard Beckert und Steffen SchlagerWorkshop on Tools for System Design and Verification (FM-TOOLS 2002)
Translating the Object Constraint Language into First-order Predicate LogicBernhard Beckert, Uwe Keller und Peter H. SchmittVERIFY Workshop (VERIFY 2002) at FLoC 2002: Federated Logic Conferences
2001
Titel Autor(en) Quelle
A Sequent Calculus for First-order Dynamic Logic with Trace ModalitiesBernhard Beckert und Steffen SchlagerFirst International Joint Conference on Automated Reasoning (IJCAR 2001)
Handling Java's Abrupt Termination in a Sequent Calculus for Dynamic LogicBernhard Beckert und Bettina SasseIJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development (PMD '01)
Free-variable Tableaux for Propositional Modal LogicsBernhard Beckert und Rajeev GoréStudia Logica 69(1)
A Dynamic Logic for the Formal Verification of Java Card ProgramsBernhard BeckertInternational 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 und Bart JacobsTechnical 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 OperatorThomas Baar, Bernhard Beckert und Peter H. SchmittFourth Andrei Ershov International Conference on Perspectives of System Informatics
2000
Titel Autor(en) Quelle
The KeY Approach: Integrating Object Oriented Design and Formal VerificationWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel und Peter H. SchmittEuropean Workshop on Logics in Artificial Intelligence (JELIA 2000)
The 2-SAT Problem of Regular Signed CNF FormulasBernhard Beckert, Reiner Hähnle und Felip Manyà30th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2000)
The KeY Approach: Integrating Object Oriented Design and Formal VerificationWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel und Peter H. Schmitt4th Workshop on Tools for System Design and Verification (FM-TOOLS 2000)
The SAT Problem of Signed CNF FormulasBernhard Beckert, Reiner Hähnle und Felip ManyaLabelled Deduction
Depth-first Proof Search without Backtracking for Free-variable Clausal TableauxBernhard BeckertThird International Workshop on First-Order Theorem Proving (FTP 2000)
The KeY Approach: Integrating Design and Formal Verification of Java Card ProgramsWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel und Peter H. SchmittJava Card Workshop (JCW 2000)
A Dynamic Logic for Java CardBernhard Beckert2nd ECOOP Workshop on Formal Techniques for Java Programs
The KeY Approach: Integrating Object Oriented Design and Formal VerificationWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel und Peter H. SchmittUniversity of Karlsruhe, Department of Computer Science 2000/4