Publications

Rather group by categories.

2017
Title Author(s) Source
Combining Graph-Based and Deduction-Based Information-Flow AnalysisBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and 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
Automatic Margin Computation for Risk-Limiting AuditsBernhard Beckert, Michael Kirsten, Vladimir Klebanov, and Carsten SchürmannFirst International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
2016
Title Author(s) Source
From Specification to Proof ObligationsDaniel Grahl and Mattias UlbrichDeductive Software Verification - The KeY Book: From Theory to Practice
Deductive Software Verification - The KeY Book: From Theory to PracticeWolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias UlbrichLecture Notes in Computer Science 10001 (Springer 2016)
Formal Specification with the Java Modeling LanguageMarieke Huisman, Wolfgang Ahrendt, Daniel Grahl, and Martin HentschelDeductive Software Verification - The KeY Book: From Theory to Practice
Functional Verification and Information Flow Analysis of an Electronic Voting SystemDaniel Grahl and Christoph SchebenDeductive Software Verification - The KeY Book: From Theory to Practice
Proof-based Test Case GenerationWolfgang Ahrendt, Christoph Gladisch, and Mihai HerdaDeductive Software Verification - The KeY Book: From Theory to Practice
Modular Specification and VerificationDaniel Grahl, Richard Bubel, Wojciech Mostowski, Peter H. Schmitt, Mattias Ulbrich, and Benjamin WeißDeductive Software Verification - The KeY Book: From Theory to Practice
Formal Verification with KeY: A TutorialBernhard Beckert, Reiner Hähnle, Martin Hentschel, and Peter H. SchmittDeductive Software Verification - The KeY Book: From Theory to Practice
Dynamic Logic for JavaBernhard Beckert, Vladimir Klebanov, and Benjamin WeißDeductive Software Verification - The KeY Book: From Theory to Practice
Using the KeY ProverWolfgang Ahrendt and Sarah GrebingDeductive Software Verification - The KeY Book: From Theory to Practice
Proof Search with TacletsPhilipp Rümmer and Mattias UlbrichDeductive Software Verification - The KeY Book: From Theory to Practice
Information Flow AnalysisChristoph Scheben and Simon GreinerDeductive Software Verification - The KeY Book: From Theory to Practice
Relational Program Reasoning Using Compiler IRMoritz Kiefer, Vladimir Klebanov, and Mattias UlbrichVerified Software. Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Revised Selected Papers
Sound Probabilistic #SAT with ProjectionVladimir Klebanov, Alexander Weigl, and Jörg Weisbarth14th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2016)
Practical Detection of Entropy Loss in Pseudo-Random Number GeneratorsFelix Dörre and Vladimir KlebanovProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security
Computing Specification-Sensitive Abstractions for Program VerificationTianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl, and Mana TaghdiriProceedings, Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016)
Deductive Verification of Legacy CodeBernhard Beckert, Thorsten Bormer, and Daniel GrahlProceedings, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 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 and Mattias UlbrichTransactions on Modularity and Compoisition 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, and Birgit Vogel‑HeuserIEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
Non-Interference with What-Declassification in Component-Based SystemsSimon Greiner and Daniel GrahlProceedings of the Computer Security Foundations Symposium (CSF 2016)
Automated Verification for Functional and Relational Properties of Voting RulesBernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and Mattias UlbrichSixth International Workshop on Computational Social Choice (COMSOC 2016)
A novel model-based testing approach for software product linesFerruccio Damiani, David Faitelson, Christoph Gladisch, and Shmuel TyszberowiczSoftware & Systems Modeling
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, and Ralf ReussnerNeues Handbuch Hochschullehre
2015
Title Author(s) Source
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander Weigl17th International Conference on Formal Engineering Methods (ICFEM 2015)
A Concept for Multi-Phase Incremental Formal Verification in Robotic Guided SurgeryMattias Ulbrich, Luzie Schreiter, Sarah Grebing, Jörg Raczkowsky, Heinz Wörn, and Bernhard Beckert4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)
Non-Interference with What-Declassification in Component-Based SystemsDaniel Grahl and 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 (October 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, and 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, and Erik KrempelInternational Data Privacy Law 5(4)
Interactive Theorem Proving - Modelling the User in the Proof ProcessBernhard Beckert and Sarah GrebingProceedings of the Workshop on Bridging the Gap between Human and Automated Reasoning - A workshop of the 25th International Conference on Automated Deduction (CADE-25)
Pseudo-Random Number Generator Verification: A Case StudyFelix Dörre and Vladimir KlebanovProceedings, Verified Software: Theories, Tools, and Experiments (VSTTE)
Regression Verification for Java Using a Secure Information Flow CalculusBernhard Beckert, Vladimir Klebanov, and Mattias Ulbrich17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)
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, and Bernhard Beckert13th IEEE International Conference on Industrial Informatics (INDIN 2015)
A Theorem Proving Approach to Secure Information Flow in Concurrent Programs (extended abstract)Daniel BrunsWorkshop on Foundations of Computer Security (FCS 2015)
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr28th IEEE Computer Security Foundations Symposium (CSF 2015)
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander WeiglKarlsruhe Institute of Technology, Department of Informatics 2015-06
Axiomatization of Typed First-Order LogicPeter H. Schmitt and Mattias Ulbrich20th International Symposium on Formal Methods (FM 2015)
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin MohrIACR Cryptology ePrint Archive 2015(438)
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, and Richard Gay36th IEEE Symposium on Security and Privacy, Poster Session
First-Order Transitive Closure Axiomatization via Iterative Invariant InjectionsAboubakr Achraf El Ghazi, Mana Taghdiri, and Mihai Herda7th NASA Formal Methods Symposium (NFM 2015)
Dynamic Dispatch for Method Contracts through Abstract PredicatesWojciech Mostowski and Mattias Ulbrich14th International Conference on MODULARITY (MODULARITY15)
Automating Regression VerificationDennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias UlbrichMultikonferenz Software Engineering und Management 2015
Specifying linked data structures in JML for combining formal verification and testingChristoph Gladisch and 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 (January 2015)
2014
Title Author(s) Source
Information Flow in Object-Oriented SoftwareBernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias UlbrichLogic-Based Program Synthesis and Transformation, LOPSTR 2013, Revised Selected Papers
Formal Verification of Voting SchemesMichael KirstenITI Beckert, Karlsruhe Institute of Technology (December 2014)
Generating JML Specifications from Alloy ExpressionsDaniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, and Shmuel TyszberowiczHardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014. Proceedings
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, and 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, and Patrik Scheidecker13th International Conference on Cryptology and Network Security (CANS 2014)
Automating Regression VerificationDennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)
A Usability Evaluation of Interactive Theorem Provers Using Focus GroupsBernhard Beckert, Sarah Grebing, and Florian BöhlSoftware Engineering and Formal Methods – SEFM 2014 Collocated Workshops
Formal Verification of an Electronic Voting SystemDaniel BrunsDepartment of Informatics, Karlsruhe Institute of Technology 2014-11
How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem ProversBernhard Beckert, Sarah Grebing, and Florian BöhlProceedings, Workshop on User Interfaces for Theorem Provers (UITP), Vienna, July 2014
Formal Specification with JMLMarieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin HentschelDepartment of Informatics, Karlsruhe Institute of Technology 2014-10
Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight MethodsBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Thomas Meumann8th International Verification Workshop (VERIFY 2014) in connection with IJCAR 2014: International Joint Conference on Automated Reasoning
JKelloy: A Proof Assistant for Relational Specifications of Java ProgramsAboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, and Mana Taghdiri6th NASA Formal Methods Symposium (NFM 2014)
Verifying Voting SchemesBernhard Beckert, Rajeev Goré, Carsten Schürmann, Thorsten Bormer, and 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, and Christoph SchebenUniversität Trier
Precise Quantitative Information Flow Analysis – A Symbolic ApproachVladimir KlebanovTheoretical Computer Science 538(0)
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 and Reiner HähnleIntelligent Systems, IEEE 29(1)
Generating Bounded Counterexamples for KeY Proof ObligationsMihai HerdaKarlsruhe Institute of Technology (January 2014)
2013
Title Author(s) Source
Information Flow in Object-Oriented Software – Extended Version –Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and 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, and 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 and Shmuel TyszberowiczBrazilian Symposium on Formal Methods (SBMF 2013)
Secure Information Flow for Java – A Dynamic Logic ApproachBernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias UlbrichDepartment of Informatics, Karlsruhe Institute of Technology 2013-10
Information Flow in Object-Oriented SoftwareBernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich23rd International Symposium on Logic-Based Program Synthesis and Transformation, (LOPSTR 2013)
Refinement-based Testing of Delta-oriented Product LinesFerruccio Damiani, Christoph Gladisch, and Shmuel TyszberowiczInternational Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools (PPPJ 2013)
Privacy Preserving Surveillance and the Tracking ParadoxSimon Greiner, Pascal Birnstill, Erik Krempel, Bernhard Beckert, and Jürgen BeyererProceedings, Future Security Conference 2013, 15–19 September 2013, Berlin
Heuristically Creating Test Cases for Program Verification SystemsBernhard Beckert, Thorsten Bormer, and Markus WagnerProceedings, 10th Metaheuristics International Conference, 5–8 August 2013, Singapore
SAT-based Analysis and Quantification of Information Flow in ProgramsVladimir Klebanov, Norbert Manthey, and Christian MuiseProceedings, International Conference on Quantitative Evaluation of Systems
Reducing the Complexity of Quantified Formulas via Variable EliminationAboubakr Achraf El Ghazi, Mattias Ulbrich, Mana Taghdiri, and Mihai Herda11th International Workshop on Satisfiability Modulo Theories (SMT)
On the Specification and Verification of Voting SchemesBernhard Beckert, Rajeev Goré, and Carsten Schürmann4th International Conference on E-Voting and Identity (Vote-ID 2013)
Analysing Vote Counting Algorithms Via Logic - And its Application to the CADE Election SystemBernhard Beckert, Rajeev Goré, and Carsten Schürmann24th International Conference on Automated Deduction (CADE-24)
Dynamic Logic with Trace SemanticsBernhard Beckert and Daniel Bruns24th International Conference on Automated Deduction (CADE-24)
A Metric for Testing Program Verification SystemsBernhard Beckert, Thorsten Bormer, and Markus WagnerTests and Proofs. Seventh International Conference, TAP 2013, Budapest, Hungary
Dynamic Logic for an Intermediate Language: Verification, Interaction and RefinementMattias UlbrichKarlsruhe Institute of Technology (June 2013)
A Dynamic Logic for Deductive Verification of Multi-Threaded ProgramsBernhard Beckert and 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, and Christoph SchebenGrande Region Security and Reliability Day (GRSRD 2013)
VerifyThis Verification Competition 2012 – Organizer's ReportMarieke Huisman, Vladimir Klebanov, and Rosemary MonahanDepartment of Informatics, Karlsruhe Institute of Technology 2013-01
2012
Title Author(s) Source
Wirtschaftlichkeit bei der Verbesserung von Systemspezifikationen durch UML-ModellierungThomas Lauscher and Simon GreinerSignal und Draht 104(12)
Lessons Learned From Microkernel Verification: Specification is the New BottleneckChristoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten BormerProceedings, Seventh Conference on Systems Software Verification. SSV 2012, Sydney, Australia)
Formal Verification of Object-Oriented Software International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011, Revised Selected PapersBernhard Beckert, Ferruccio Damiani, and Dilian GurovLNCS 7421 (Springer 2012)
Integration of Bounded Model Checking and Deductive VerificationBernhard Beckert, Thorsten Bormer, Florian Merz, and Carsten SinzFormal Verification of Object-Oriented Software International Conference, FoVeOOS 2011, Turin, Italy, October 5-7, 2011, Revised Selected Papers
Dynamic Trace Logic: Definition and ProofsBernhard Beckert and Daniel BrunsDepartment of Informatics, Karlsruhe Institute of Technology 2012-10
Precise Quantitative Information Flow Analysis Using Symbolic Model CountingVladimir KlebanovProceedings, International Workshop on Quantitative Aspects in Security Assurance (QASA)
Formal Semantics of Model Fields in Annotation-based SpecificationsBernhard Beckert and Daniel BrunsKI 2012: Advances in Artificial Intelligence
Lessons Learned From Microkernel VerificationBernhard Beckert and Thorsten BormerProceedings, AVOCS 2012: International Workshop on Automated Verification of Critical Systems
Evaluating and Improving the Usability of Interactive Verification SystemsSarah GrebingUniversität Koblenz-Landau (August 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, and Tomasz TruderungDepartment of Informatics, Karlsruhe Institute of Technology 2012-8
Mind the Gap: Formal Verification and the Common CriteriaBernhard Beckert, Daniel Bruns, and Sarah Grebing6th International Verification Workshop, VERIFY 2010
Evaluating the Usability of Interactive Verification SystemsBernhard Beckert and Sarah GrebingProceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE), Manchester, UK, June 30, 2012
On the Organisation of Program Verification CompetitionsMarieke Huisman, Vladimir Klebanov, and Rosemary MonahanProceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE), Manchester, UK, June 30, 2012
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, and Mana Taghdiri18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Model generation for quantified formulas with application to test data generationChristoph GladischInternational Journal on Software Tools for Technology Transfer (STTT) 14(4)
Proceedings of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems (COMPARE), Manchester, UK, June 30, 2012Vladimir Klebanov, Bernhard Beckert, Armin Biere, and Geoff SutcliffeCEUR Workshop Proceedings 873 (CEUR-WS.org 2012)
Formal Methods for Components and Objects, 10th International Symposium FMCO 2011. State-of-the-Art SurveyBernhard Beckert, Ferruccio Damiani, Frank de Boer, and Marcello BonsangueLNCS 7542 (Springer 2012)
2011
Title Author(s) Source
Formal Verification of Object-Oriented Software. Papers Presented at the 2nd International Conference, October 5-7, 2011, Turin, ItalyBernhard Beckert, Ferruccio Damiani, and Dilian GurovKarlsruhe Institute of Technology, Department of Informatics 2011-26
Verlässliche Software fur kritische Infrastrukturen - PrefaceBernhard Beckert and Gregor SneltingINFORMATIK 2011 Informatik schafft Communities – Beiträge der 41. Jahrestagung der Gesellschaft für Informatik e.V. (GI)
KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit TestingBernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz, and 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
A Dual-Engine for Early Analysis of Critical SystemsAboubakr Achraf El Ghazi, Ulrich Geilmann, Mattias Ulbrich, and Mana TaghdiriWorkshop on Dependable Software for Critical Infrastructures (DSCI)
Formal Semantics of Model Fields Inspired by a Generalization of Hilbert's ε TermsBernhard Beckert and Daniel Bruns10th KeY Symposium
A Dynamic Logic for Unstructured Programs with Embedded AssertionsMattias UlbrichRevised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)
Verification of Software Product Lines with Delta-Oriented SlicingDaniel Bruns, Vladimir Klebanov, and Ina SchaeferFormal Verification of Object-Oriented Software (FoVeOOS 2010)
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, and Benjamin WeißProceedings, 17th International Symposium on Formal Methods (FM 2011)
Dynamic Frames in Java Dynamic LogicPeter H. Schmitt, Mattias Ulbrich, and Benjamin WeißRevised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010)
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, and Gregor Sneltingit - Information Technology 53(3)
Proving Memory Separation in a Microkernel by Code Level VerificationChristoph Baumann, Holger Blasum, Thorsten Bormer, and Sergey Tverdyshev1st International Workshop on Architectures and Applications for Mixed-Criticality Systems (AMICS 2011)
Verification-based Software-fault DetectionChristoph GladischKarlsruhe Institute of Technology (KIT) (February 2011)
Improving the Usability of Specification Languages and Methods for Annotation-based VerificationBernhard Beckert, Thorsten Bormer, and Vladimir KlebanovFormal Methods for Components and Objects, 9th International Symposium FMCO 2010. State-of-the-Art Survey
Improving the Usability of Specification Languages and Methods for Annotation-based VerificationBernhard Beckert, Thorsten Bormer, and Vladimir KlebanovProceedings, 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010)
Formal Verification of Object-Oriented Software. International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010. Revised Selected PapersBernhard Beckert and Claude MarchéLNCS 6528 (Springer 2011)
2010
Title Author(s) Source
Software Security in Virtualized Infrastructures – The Smart Meter ExampleBernhard Beckert, Dennis Hofheinz, Jörn Müller‑Quade, Alexander Pretschner, and Gregor SneltingKarlsruhe Institute of Technology 2010-20
Dynamic Frames in Java Dynamic Logic: Formalisation and ProofsPeter H. Schmitt, Mattias Ulbrich, and Benjamin WeißDepartment of Computer Science, Karlsruhe Institute of Technology 2010-11
Towards Testing a Verifying CompilerThorsten Bormer and Markus WagnerFormal Verification of Object-Oriented Software, Papers presented at the International Conference
Deduktion: Von der Theorie zur AnwendungFranz Baader, Bernhard Beckert, and Tobias NipkowInformatik-Spektrum 33(5)
Generating Regression Unit Tests using a Combination of Verification and Capture & ReplayBernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz, and Amiram YehudaiTests and Proofs. Fourth International Conference, TAP 2010, Malaga, Spain
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: Reducing the Effort with Delta-oriented Slicing and Proof ReuseDaniel Bruns, Vladimir Klebanov, and Ina SchaeferPapers Presented at the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS)
Verification of Software Product Lines with Delta-oriented SlicingDaniel Bruns, Vladimir Klebanov, and Ina SchaeferRevised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS)
Special Issue on Tests and ProofsBernhard Beckert and Reiner HähnleJournal of Automated Reasoning 45(4)
Deductive Verification of a Byzantine Agreement ProtocolRoman Krenický and Mattias UlbrichKarlsruhe Institute of Technology, Department of Informatics 2010-7
Formal Semantics for the Java Modeling LanguageDaniel BrunsInformatiktage 2010
Ingredients of Operating System CorrectnessChristoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten BormerProceedings, embedded world 2010 Conference, Nuremberg, Germany
Deductive Verification of System Software in the Verisoft XT ProjectBernhard Beckert and Michal MoskalKI 24(1)
Satisfiability Solving and Model Generation for Quantified First-Order Logic FormulasChristoph GladischFormal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Revised Selected Papers
Test Data Generation for Programs with Quantified First-Order Logic SpecificationsChristoph GladischTesting Software and Systems - 22nd IFIP WG 6.1 International Conference, ICTSS 2010. Proceedings
Formal Verification of Object-Oriented Software. Papers Presented at the International Conference, June 28-30, 2010, Paris, FranceBernhard Beckert and Claude MarchéKarlsruhe Institute of Technology, Department of Informatics 2010-13
Practical Aspects of Automated Deduction for Program VerificationWolfgang Ahrendt, Bernhard Beckert, Martin Giese, and Philipp RümmerKI 24(1)
2009
Title Author(s) Source
On Essential Program Annotations and Completeness of Verifying CompilersBernhard Beckert, Thorsten Bormer, and Vladimir KlebanovProceedings, Workshop on Verified Software: Theory, Tools, and Experiments (VSTTE)
Probabilistic Models for the Verification of Human-Computer InteractionBernhard Beckert and Markus WagnerKI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, KI 2009, Paderborn, Germany, September 15-18, 2009. Proceedings
Formal Verification of a Microkernel Used in Dependable Software SystemsChristoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten BormerProceedings, 28th International Conference on Computer Safety, Reliability and Security, Hamburg, Germany
Could we have chosen a better Loop Invariant or Method Contract?Christoph GladischTests and Proofs. Third International Conference, TAP 2009, Zürich, Switzerland
Extending the Reach and Power of Deductive Program VerificationVladimir KlebanovUniversität Koblenz-Landau (June 2009)
Formal Semantics for the Java Modeling LanguageDaniel BrunsUniversität Karlsruhe (June 2009)
Verifying the PikeOS Microkernel: First Results in the Verisoft XT Avionics ProjectChristoph Baumann and Thorsten BormerDoctoral Symposium on Systems Software Verification (DS SSV'09)
Better Avionics Software Reliability by Code VerificationChristoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten BormerProceedings, embedded world Conference, Nuremberg, Germany
2008
Title Author(s) Source
Verification-based Testing for Full Feasible Branch CoverageChristoph GladischProc. 6th IEEE Int. Conf. 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
Editorial. Special Section on Software Engineering and Formal MethodsBernhard K. Aichernig and Bernhard BeckertSoftware and System Modeling 7(3)
Integrating Verification and Testing of Object-Oriented SoftwareChristian Engel, Christoph Gladisch, Vladimir Klebanov, and Philipp RümmerTests and Proofs, Second International Conference, TAP 2008, Prato, Italy
Tests and Proofs. Second International Conference, TAP 2008, Prato, ItalyBernhard Beckert and Reiner HähnleLNCS 4966 (Springer 2008)
5th International Verification Workshop (VERIFY'08). Co-located with the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, AustraliaBernhard Beckert and Gerwin KleinCEUR Workshop Proceedings 372 (CEUR-WS.org 2008)
2007
Title Author(s) Source
How C differs from Java for Symbolic Program ExecutionChristoph GladischProceedings, C/C++ Verification Workshop, Oxford, United Kingdom
A Fixpoint-based Rule for Loop VerificationDaniel BrunsUniversität Karlsruhe (June 2007)
KeY: A Formal Method for Object-Oriented SystemsWolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, and Peter H. SchmittProceedings, IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), Paphos, Cyprus
4th International Verification Workshop (VERIFY'07). Co-located with the 21st Conference on Automated Deduction (CADE-21), Bremen, GermanyBernhard BeckertCEUR Workshop Proceedings 259 (CEUR-WS.org 2007)
Proof ReuseVladimir KlebanovVerification of Object-Oriented Software: The KeY Approach
Software Verification for Java 5Mattias UlbrichFakultät für Informatik, Universität Karlsruhe (January 2007)
Dynamic LogicBernhard Beckert, Vladimir Klebanov, and Steffen SchlagerVerification of Object-Oriented Software: The KeY Approach
Verifying Object-Oriented Programs with KeY: A TutorialWolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, and Peter H. SchmittRevised Lectures, 5th International Symposium on Formal Methods for Components and Objects (FMCO 2006), Amsterdam, The Netherlands
A Dynamic Logic for Deductive Verification of Concurrent Java Programs With Condition VariablesBernhard Beckert and Vladimir KlebanovProceedings, 1st International Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP), Satellite Workshop CONCUR 2007, Lisbon, Portugal
A Dynamic Logic for Deductive Verification of Concurrent ProgramsBernhard Beckert and Vladimir KlebanovProceedings, 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM), London, UK
Verification of Object-Oriented Software: The KeY ApproachBernhard Beckert, Reiner Hähnle, and Peter H. SchmittLecture Notes in Computer Science 4334 (Springer 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. SchmittProceedings, International Conference on Automated Deduction, Bremen, Germany
White-box Testing by Combining Deduction-based Specification Extraction and Black-box TestingBernhard Beckert and Christoph GladischProceedings, International Conference on Tests and Proofs (TAP), Zurich, Switzerland
Preface. Special Issue on Automated Reasoning with Analytic Tableaux and Related MethodsBernhard Beckert and Lawrence PaulsonJournal of Automated Reasoning 38(1–3)
2006
Title Author(s) Source
Integrating Object-oriented Design and Deductive Verification of Software. Tutorial AbstractBernhard Beckert, Reiner Hähnle, and Peter H. SchmittSoftware Engineering and Formal Methods. 4th IEEE International Conference, SEFM 2006, Pune, India, Proceedings
Guaranteeing Consistency in Text-Based Human-Computer InteractionBernhard Beckert and Gerd BeusterProceedings, International Workshop on Formal Methods for Interactive Systems (FMIS), Macao SAR China
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, and Sriram K. RajamaniIEEE Intelligent Systems 21(6)
Must Program Verification Systems and Calculi be Verified?Bernhard Beckert and Vladimir KlebanovProceedings, 3rd International Verification Workshop (VERIFY), Workshop at Federated Logic Conferences (FLoC), Seattle, USA
Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program VerificationBernhard Beckert and André PlatzerProceedings, International Joint Conference on Automated Reasoning, Seattle, USA
A Method for Formalizing, Analyzing, and Verifying Secure User InterfacesBernhard Beckert and Gerd BeusterProceedings, Eighth International Conference on Formal Engineering Methods
2005
Title Author(s) Source
Refinement and Retrenchment for Programming Language Data TypesBernhard Beckert and Steffen SchlagerFormal Aspects of Computing 17(4)
An Improved Rule for While Loops in Deductive Program VerificationBernhard Beckert, Steffen Schlager, and Peter H. SchmittProceedings, Seventh International Conference on Formal Engineering Methods (ICFEM), Manchester, UK
Verification of JCSP ProgramsVladimir Klebanov, Philipp Rümmer, Steffen Schlager, and Peter H. SchmittCommunicating Process Architectures (CPA), Proceedings
Reusing Proofs when Program Verification Systems are ModifiedBernhard Beckert, Thorsten Bormer, and Vladimir KlebanovProceedings, Software Certificate Management Workshop (SoftCeMent), Long Beach, California, USA
Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen SyntheseMattias UlbrichFakultät für Informatik, Universität Karlsruhe (January 2005)
Second-Order Principles in Specification Languages for Object-Oriented ProgramsBernhard Beckert and Kerry TrentelmanProceedings, 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Montego Bay, Jamaica
The KeY ToolWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. SchmittSoftware and System Modeling 4(1)
Email Client Verification GoalsBernhard Beckert and Gerd BeusterVerisoft Project #46
Automated Reasoning with Analytic Tableaux and Related MethodsBernhard BeckertLNCS 3702 (Springer 2005)
TABLEAUX 2005: Position Papers and Tutorial DescriptionsBernhard BeckertUniversität Koblenz-Landau 12–2005
Third International Conference on Software Engineering and Formal Methods (SEFM 2005)Bernhard K. Aichernig and Bernhard BeckertIEEE Computer Society 2005
2004
Title Author(s) Source
Formal Specification of Security-relevant Properties of User InterfacesBernhard Beckert and Gerd BeusterProceedings, 3rd International Workshop on Critical Systems Development with UML, Lisbon, Portugal
Proof Reuse for Deductive Program VerificationBernhard Beckert and Vladimir KlebanovProceedings, Software Engineering and Formal Methods (SEFM), Beijing, China
A JMM-Faithful Non-interference Calculus for Java.Vladimir KlebanovScientific Engineering of Distributed Java Applications, 4th International Workshop, FIDJI 2004, Luxembourg-Kirchberg
Email Client SpecificationBernhard Beckert, Gerd Beuster, and 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, and Steffen SchlagerDepartment of Computer Science, University of Koblenz 9-2004
Software Verification with Integrated Data Type Refinement for Integer ArithmeticBernhard Beckert and Steffen SchlagerProceedings, International Conference on Integrated Formal Methods, Canterbury, UK
Taclets: A New Paradigm for Constructing Interactive Theorem ProversBernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen SchlagerRevista de la Real Academia de Ciencias Exactas, F'isicas y Naturales, Serie A: Matemáticas (RACSAM) 98(1)
Formal Specification of Security-relevant Properties of User InterfacesBernhard Beckert and Gerd BeusterDepartment of Computer Science, University of Koblenz 10-2004
2003
Title Author(s) Source
The KeY ToolWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. SchmittDepartment of Computing Science, Chalmers University and Göteborg University, Göteborg, Sweden No. 2003-5
Program Verification Using Change InformationBernhard Beckert and Peter H. SchmittProceedings, Software Engineering and Formal Methods (SEFM), Brisbane, Australia
A Program Logic for Handling Java Card's Transaction MechanismBernhard Beckert and Wojciech MostowskiProceedings, Fundamental Approaches to Software Engineering (FASE), Warsaw, Poland
Depth-first Proof Search without Backtracking for Free-variable Clausal TableauxBernhard BeckertJournal of Symbolic Computation 36(1-2)
2002
Title Author(s) Source
Integer Arithmetic in the Specification and Verification of Java ProgramsBernhard Beckert and Steffen SchlagerProceedings, Workshop on Tools for System Design and Verification (FM-TOOLS), Reisensburg, Germany
The KeY System: Integrating Object-Oriented Design and Formal MethodsWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, and Peter H. SchmittFundamental Approaches to Software Engineering. 5th International Conference, FASE 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 2002, Proceedings
Translating the Object Constraint Language into First-order Predicate LogicBernhard Beckert, Uwe Keller, and Peter H. SchmittProceedings, VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen, Denmark
2001
Title Author(s) Source
A Dynamic Logic for the Formal Verification of Java Card ProgramsBernhard BeckertJava on Smart Cards: Programming and Security. Revised Papers, Java Card 2000, International Workshop, Cannes, France
An Extension of Dynamic Logic for Modelling OCL's @pre OperatorThomas Baar, Bernhard Beckert, and Peter H. SchmittProceedings, Fourth Andrei Ershov International Conference, Perspectives of System Informatics, Novosibirsk, Russia
A Sequent Calculus for First-order Dynamic Logic with Trace ModalitiesBernhard Beckert and Steffen SchlagerProceedings, International Joint Conference on Automated Reasoning, Siena, Italy
Proceedings, IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development, Siena, ItalyBernhard Beckert, Robert France, Reiner Hähnle, and Bart JacobsTechnical Report DII 07/01, Dipartimento di Ingegneria dell'Informazione, Università degli Studi di Siena 2001
Free-variable Tableaux for Propositional Modal LogicsBernhard Beckert and Rajeev GoréStudia Logica 69(1)
Handling Java's Abrupt Termination in a Sequent Calculus for Dynamic LogicBernhard Beckert and Bettina SasseProceedings, IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development, Siena, Italy
2000
Title Author(s) Source
The 2-SAT Problem of Regular Signed CNF FormulasBernhard Beckert, Reiner Hähnle, and Felip ManyàProceedings, International Symposium on Multiple-valued Logic (ISMVL), Portland, USA
The KeY Approach: Integrating Object Oriented Design and Formal VerificationWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. SchmittProceedings, 4th Workshop on Tools for System Design and Verification (FM-TOOLS), Reisensburg, Germany
The KeY Approach: Integrating Object Oriented Design and Formal VerificationWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. SchmittUniversity of Karlsruhe, Department of Computer Science 2000/4
The KeY Approach: Integrating Object Oriented Design and Formal VerificationWolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, and Peter H. SchmittProceedings, Logics in Artificial Intelligence (JELIA), Malaga, Spain
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, and Peter H. SchmittProceedings, Java Card Workshop (JCW), Cannes, France
Depth-first Proof Search without Backtracking for Free-variable Clausal TableauxBernhard BeckertThird International Workshop on First-Order Theorem Proving (FTP), St.~Andrews, Scotland
A Dynamic Logic for Java CardBernhard BeckertProceedings, 2nd ECOOP Workshop on Formal Techniques for Java Programs, Cannes, France
The SAT Problem of Signed CNF FormulasBernhard Beckert, Reiner Hähnle, and Felip ManyaLabelled Deduction