Publications

2017
Title Author(s) Source
Automatic Margin Computation for Risk-Limiting AuditsBernhard Beckert
Michael Kirsten
Vladimir Klebanov
Carsten Schürmann
First International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
2016
Title Author(s) Source
Deductive Software Verification - The KeY Book: From Theory to PracticeWolfgang Ahrendt
Bernhard Beckert
Richard Bubel
Reiner Hähnle
Peter H. Schmitt
Mattias Ulbrich
Formal Specification with the Java Modeling LanguageMarieke Huisman
Wolfgang Ahrendt
Daniel Grahl
Martin Hentschel
Deductive Software Verification - The KeY Book: From Theory to Practice
Functional Verification and Information Flow Analysis of an Electronic Voting SystemDaniel Grahl
Christoph Scheben
Deductive Software Verification – The KeY Book: From Theory to Practice
From Specification to Proof ObligationsDaniel Grahl
Mattias Ulbrich
Deductive Software Verification - The KeY Book: From Theory to Practice
Formal Verification with KeY: A TutorialBernhard Beckert
Reiner Hähnle
Martin Hentschel
Peter H. Schmitt
Deductive Software Verification - The KeY Book: From Theory to Practice
Dynamic Logic for JavaBernhard Beckert
Vladimir Klebanov
Benjamin Weiß
Deductive Software Verification - The KeY Book: From Theory to Practice
Proof Search with TacletsPhilipp Rümmer
Mattias Ulbrich
Deductive Software Verification - The KeY Book: From Theory to Practice
Modular Specification and VerificationDaniel Grahl
Richard Bubel
Wojciech Mostowski
Peter H. Schmitt
Mattias Ulbrich
Benjamin Weiß
Deductive Software Verification - The KeY Book: From Theory to Practice
Relational Program Reasoning Using Compiler IRMoritz Kiefer
Vladimir Klebanov
Mattias Ulbrich
Verified Software. Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Revised Selected Papers
Sound Probabilistic #SAT with ProjectionVladimir Klebanov
Alexander Weigl
Jörg Weisbarth
14th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2016)
Practical Detection of Entropy Loss in Pseudo-Random Number GeneratorsFelix Dörre
Vladimir Klebanov
Proceedings 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
Mana Taghdiri
Proceedings, Second International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016)
Deductive Verification of Legacy CodeBernhard Beckert
Thorsten Bormer
Daniel Grahl
Proceedings, 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
Mattias Ulbrich
Transactions on Modularity and Compoisition
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
Birgit Vogel-Heuser
IEEE 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
Mattias Ulbrich
Sixth International Workshop on Computational Social Choice (COMSOC 2016)
Non-Interference with What-Declassification in Component-Based SystemsSimon Greiner
Daniel Grahl
Proceedings of the Computer Security Foundations Symposium (CSF 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
Ralf Reussner
Neues Handbuch Hochschullehre
A novel model-based testing approach for software product linesFerruccio Damiani
David Faitelson
Christoph Gladisch
Shmuel Tyszberowicz
Software & Systems Modeling
2015
Title Author(s) Source
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert
Mattias Ulbrich
Birgit Vogel-Heuser
Alexander Weigl
17th 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
Bernhard Beckert
4th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)
Non-Interference with What-Declassification in Component-Based SystemsDaniel Grahl
Simon Greiner
Department 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
Birgit Vogel-Heuser
20th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2015)
Privacy-preserving surveillance: an interdisciplinary approachPascal Birnstill
Sebastian Bretthauer
Simon Greiner
Erik Krempel
International Data Privacy Law
Interactive Theorem Proving - Modelling the User in the Proof ProcessBernhard Beckert
Sarah Grebing
Proceedings 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
Vladimir Klebanov
Proceedings, Verified Software: Theories, Tools, and Experiments (VSTTE)
Regression Verification for Java Using a Secure Information Flow CalculusBernhard Beckert
Vladimir Klebanov
Mattias Ulbrich
17th 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
Bernhard Beckert
13th 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
Martin Mohr
28th IEEE Computer Security Foundations Symposium (CSF 2015)
Axiomatization of Typed First-Order LogicPeter H. Schmitt
Mattias Ulbrich
20th International Symposium on Formal Methods (FM 2015)
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert
Mattias Ulbrich
Birgit Vogel-Heuser
Alexander Weigl
Karlsruhe Institute of Technology, Department of Informatics 2015-06
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters
Tomasz Truderung
Bernhard Beckert
Daniel Bruns
Michael Kirsten
Martin Mohr
IACR Cryptology ePrint Archive
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
Richard Gay
36th IEEE Symposium on Security and Privacy, Poster Session
First-Order Transitive Closure Axiomatization via Iterative Invariant InjectionsAboubakr Achraf El Ghazi
Mana Taghdiri
Mihai Herda
7th NASA Formal Methods Symposium (NFM 2015)
Automating Regression VerificationDennis Felsing
Sarah Grebing
Vladimir Klebanov
Philipp Rümmer
Mattias Ulbrich
Multikonferenz Software Engineering und Management 2015
Dynamic Dispatch for Method Contracts through Abstract PredicatesWojciech Mostowski
Mattias Ulbrich
14th International Conference on MODULARITY (MODULARITY15)
Deductive Verification of Concurrent ProgramsDaniel BrunsDepartment of Informatics, Karlsruhe Institute of Technology 2015-3
Specifying linked data structures in JML for combining formal verification and testingChristoph Gladisch
Shmuel Tyszberowicz
Science of Computer Programming
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
Mattias Ulbrich
Logic-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
Shmuel Tyszberowicz
Hardware 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
Mattias Ulbrich
6th 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
Patrik Scheidecker
Cryptology and Network Security (CANS 2014)
Automating Regression VerificationDennis Felsing
Sarah Grebing
Vladimir Klebanov
Philipp Rümmer
Mattias Ulbrich
29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)
A Usability Evaluation of Interactive Theorem Provers Using Focus GroupsBernhard Beckert
Sarah Grebing
Florian Böhl
Software 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
Florian Böhl
Proceedings, Workshop on User Interfaces for Theorem Provers (UITP), Vienna, July 2014
Formal Specification with JMLMarieke Huisman
Wolfgang Ahrendt
Daniel Bruns
Martin Hentschel
Department 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
Thomas Meumann
8th 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
Mana Taghdiri
6th NASA Formal Methods Symposium (NFM 2014)
Verifying Voting SchemesBernhard Beckert
Rajeev Goré
Carsten Schürmann
Thorsten Bormer
Jian Wang
Journal of Information Security and Applications (JISA)
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
Christoph Scheben
Precise Quantitative Information Flow Analysis – A Symbolic ApproachVladimir KlebanovTheoretical Computer Science
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
Reiner Hähnle
Intelligent Systems, IEEE
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
Mattias Ulbrich
Department 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
Mattias Ulbrich
International Journal on Software Tools for Technology Transfer (STTT)
Specifying a Linked Data Structure in JML for Formal Verification and Runtime CheckingChristoph Gladisch
Shmuel Tyszberowicz
Brazilian Symposium on Formal Methods (SBMF)
Secure Information Flow for Java – A Dynamic Logic ApproachBernhard Beckert
Daniel Bruns
Vladimir Klebanov
Christoph Scheben
Peter H. Schmitt
Mattias Ulbrich
Department of Informatics, Karlsruhe Institute of Technology 2013-10
Information Flow in Object-Oriented SoftwareBernhard Beckert
Daniel Bruns
Vladimir Klebanov
Christoph Scheben
Peter H. Schmitt
Mattias Ulbrich
23rd International Symposium on Logic-Based Program Synthesis and Transformation, (LOPSTR 2013)
Refinement-based Testing of Delta-oriented Product LinesFerruccio Damiani
Christoph Gladisch
Shmuel Tyszberowicz
PPPJ'13
Privacy Preserving Surveillance and the Tracking ParadoxSimon Greiner
Pascal Birnstill
Erik Krempel
Bernhard Beckert
Jürgen Beyerer
Proceedings, Future Security Conference 2013, 15–19 September 2013, Berlin
Heuristically Creating Test Cases for Program Verification SystemsBernhard Beckert
Thorsten Bormer
Markus Wagner
Proceedings, 10th Metaheuristics International Conference, 5–8 August 2013, Singapore
SAT-based Analysis and Quantification of Information Flow in ProgramsVladimir Klebanov
Norbert Manthey
Christian Muise
Proceedings, International Conference on Quantitative Evaluation of Systems
Reducing the Complexity of Quantified Formulas via Variable EliminationAboubakr Achraf El Ghazi
Mattias Ulbrich
Mana Taghdiri
Mihai Herda
11th International Workshop on Satisfiability Modulo Theories (SMT)
On the Specification and Verification of Voting SchemesBernhard Beckert
Rajeev Goré
Carsten Schürmann
4th 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é
Carsten Schürmann
24th International Conference on Automated Deduction (CADE-24)
Dynamic Logic with Trace SemanticsBernhard Beckert
Daniel Bruns
24th International Conference on Automated Deduction (CADE-24)
A Metric for Testing Program Verification SystemsBernhard Beckert
Thorsten Bormer
Markus Wagner
Tests 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
Vladimir Klebanov
Formal Aspects of Computing
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
Christoph Scheben
Grande Region Security and Reliability Day 2013
VerifyThis Verification Competition 2012 – Organizer's ReportMarieke Huisman
Vladimir Klebanov
Rosemary Monahan
Department of Informatics, Karlsruhe Institute of Technology 2013-01
2012
Title Author(s) Source
Wirtschaftlichkeit bei der Verbesserung von Systemspezifikationen durch UML-ModellierungThomas Lauscher
Simon Greiner
Signal und Draht
Lessons Learned From Microkernel Verification: Specification is the New BottleneckChristoph Baumann
Bernhard Beckert
Holger Blasum
Thorsten Bormer
Proceedings, Seventh Conference on Systems Software Verification. SSV 2012, Sydney, Australia)
Integration of Bounded Model Checking and Deductive VerificationBernhard Beckert
Thorsten Bormer
Florian Merz
Carsten Sinz
Formal 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
Daniel Bruns
Department 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
Daniel Bruns
KI 2012: Advances in Artificial Intelligence
Lessons Learned From Microkernel VerificationBernhard Beckert
Thorsten Bormer
Proceedings, AVOCS 2012: International Workshop on Automated Verification of Critical Systems
Evaluating and Improving the Usability of Interactive Verification SystemsSarah GrebingUniversität Koblenz-Landau
The KeY Approach for the Cryptographic Verification of Java Programs: A Case StudyBernhard Beckert
Daniel Bruns
Ralf Küsters
Christoph Scheben
Peter H. Schmitt
Tomasz Truderung
Department of Informatics, Karlsruhe Institute of Technology 2012-8
Mind the Gap: Formal Verification and the Common CriteriaBernhard Beckert
Daniel Bruns
Sarah Grebing
6th International Verification Workshop, VERIFY 2010
Evaluating the Usability of Interactive Verification SystemsBernhard Beckert
Sarah Grebing
Proceedings 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
Rosemary Monahan
Proceedings 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
A Proof Assistant for Alloy SpecificationsMattias Ulbrich
Ulrich Geilmann
Aboubakr Achraf El Ghazi
Mana Taghdiri
18th 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)
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
Dilian Gurov
Karlsruhe Institute of Technology
Verlässliche Software fur kritische Infrastrukturen - PrefaceBernhard Beckert
Gregor Snelting
INFORMATIK 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
Amiram Yehudai
International Journal of Systems Assurance Engineering and Management
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
Mana Taghdiri
Workshop on Dependable Software for Critical Infrastructures (DSCI)
Formal Semantics of Model Fields Inspired by a Generalization of Hilbert's ε TermsBernhard Beckert
Daniel Bruns
10th 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
Ina Schaefer
Formal 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
Benjamin Weiß
Proceedings, 17th International Symposium on Formal Methods (FM 2011)
Dynamic Frames in Java Dynamic LogicPeter H. Schmitt
Mattias Ulbrich
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
Gregor Snelting
it - Information Technology
Proving Memory Separation in a Microkernel by Code Level VerificationChristoph Baumann
Holger Blasum
Thorsten Bormer
Sergey Tverdyshev
1st 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
Vladimir Klebanov
Proceedings, 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010)
Improving the Usability of Specification Languages and Methods for Annotation-based VerificationBernhard Beckert
Thorsten Bormer
Vladimir Klebanov
Formal Methods for Components and Objects, 9th International Symposium FMCO 2010. State-of-the-Art Survey
2010
Title Author(s) Source
Software Security in Virtualized Infrastructures – The Smart Meter ExampleBernhard Beckert
Dennis Hofheinz
Jörn Müller-Quade
Alexander Pretschner
Gregor Snelting
Karlsruhe Institute of Technology
Dynamic Frames in Java Dynamic Logic: Formalisation and ProofsPeter H. Schmitt
Mattias Ulbrich
Benjamin Weiß
Department of Computer Science, Karlsruhe Institute of Technology 2010-11
Towards Testing a Verifying CompilerThorsten Bormer
Markus Wagner
Formal Verification of Object-Oriented Software, Papers presented at the International Conference
Deduktion: Von der Theorie zur AnwendungFranz Baader
Bernhard Beckert
Tobias Nipkow
Informatik-Spektrum
Generating Regression Unit Tests using a Combination of Verification and Capture & ReplayBernhard Beckert
Christoph Gladisch
Shmuel Tyszberowicz
Amiram Yehudai
Tests and Proofs. Fourth International Conference, TAP 2010, Malaga, Spain
Satisfiability Solving and Model Generation for Quantified First-order Logic FormulasChristoph Gladisch
Verification of Software Product Lines with Delta-oriented SlicingDaniel Bruns
Vladimir Klebanov
Ina Schaefer
Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS)
Verification of Software Product Lines: Reducing the Effort with Delta-oriented Slicing and Proof ReuseDaniel Bruns
Vladimir Klebanov
Ina Schaefer
Papers Presented at the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS)
Deductive Verification of a Byzantine Agreement ProtocolRoman Krenický
Mattias Ulbrich
Karlsruhe Institute of Technology, Department of Informatics 2010-7
Special Issue on Tests and ProofsBernhard Beckert
Reiner Hähnle
Journal of Automated Reasoning
Formal Semantics for the Java Modeling LanguageDaniel BrunsInformatiktage 2010
Ingredients of Operating System CorrectnessChristoph Baumann
Bernhard Beckert
Holger Blasum
Thorsten Bormer
Proceedings, embedded world 2010 Conference, Nuremberg, Germany
Deductive Verification of System Software in the Verisoft XT ProjectBernhard Beckert
Michal Moskal
KI
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
Practical Aspects of Automated Deduction for Program VerificationWolfgang Ahrendt
Bernhard Beckert
Martin Giese
Philipp Rümmer
KI
2009
Title Author(s) Source
On Essential Program Annotations and Completeness of Verifying CompilersBernhard Beckert
Thorsten Bormer
Vladimir Klebanov
Proceedings, Workshop on Verified Software: Theory, Tools, and Experiments (VSTTE)
Probabilistic Models for the Verification of Human-Computer InteractionBernhard Beckert
Markus Wagner
KI 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
Thorsten Bormer
Proceedings, 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
Thorsten Bormer
Doctoral Symposium on Systems Software Verification (DS SSV'09)
Better Avionics Software Reliability by Code VerificationChristoph Baumann
Bernhard Beckert
Holger Blasum
Thorsten Bormer
Proceedings, 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
Verification-based Test Case Generation with Loop Invariants and Method SpecificationsChristoph GladischUniversity of Koblenz-Landau
Extending KeY for the Verification of C ProgramsChristoph Gladisch
Editorial. Special Section on Software Engineering and Formal MethodsBernhard Aichernig
Bernhard Beckert
Software and System Modeling
Integrating Verification and Testing of Object-Oriented SoftwareChristian Engel
Christoph Gladisch
Vladimir Klebanov
Philipp Rümmer
Tests and Proofs, Second International Conference, TAP 2008, Prato, Italy
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
Peter H. Schmitt
Proceedings, IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), Paphos, Cyprus
Software Verification for Java 5Mattias UlbrichDiplomarbeit, Fakultät für Informatik, Universität Karlsruhe
Dynamic LogicBernhard Beckert
Vladimir Klebanov
Steffen Schlager
Verification of Object-Oriented Software: The KeY Approach
Verifying Object-Oriented Programs with KeY: A TutorialWolfgang Ahrendt
Bernhard Beckert
Reiner Hähnle
Philipp Rümmer
Peter H. Schmitt
Revised 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
Vladimir Klebanov
Proceedings, 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
Vladimir Klebanov
Proceedings, 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
Peter H. Schmitt
The KeY System 1.0 (Deduction Component)Bernhard Beckert
Martin Giese
Reiner Hähnle
Vladimir Klebanov
Philipp Rümmer
Steffen Schlager
Peter H. Schmitt
Proceedings, International Conference on Automated Deduction, Bremen, Germany
White-box Testing by Combining Deduction-based Specification Extraction and Black-box TestingBernhard Beckert
Christoph Gladisch
Proceedings, International Conference on Tests and Proofs (TAP), Zurich, Switzerland
Preface. Special Issue on Automated Reasoning with Analytic Tableaux and Related MethodsBernhard Beckert
Lawrence Paulson
Journal of Automated Reasoning
2006
Title Author(s) Source
Integrating Object-oriented Design and Deductive Verification of Software. Tutorial AbstractBernhard Beckert
Reiner Hähnle
Peter H. Schmitt
Software Engineering and Formal Methods. 4th IEEE International Conference, SEFM 2006, Pune, India, Proceedings
Guaranteeing Consistency in Text-Based Human-Computer InteractionBernhard Beckert
Gerd Beuster
Proceedings, 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
Sriram K. Rajamani
IEEE Intelligent Systems
Must Program Verification Systems and Calculi be Verified?Bernhard Beckert
Vladimir Klebanov
Proceedings, 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
André Platzer
Proceedings, International Joint Conference on Automated Reasoning, Seattle, USA
A Method for Formalizing, Analyzing, and Verifying Secure User InterfacesBernhard Beckert
Gerd Beuster
Proceedings, Eighth International Conference on Formal Engineering Methods
2005
Title Author(s) Source
Refinement and Retrenchment for Programming Language Data TypesBernhard Beckert
Steffen Schlager
Formal Aspects of Computing
An Improved Rule for While Loops in Deductive Program VerificationBernhard Beckert
Steffen Schlager
Peter H. Schmitt
Proceedings, Seventh International Conference on Formal Engineering Methods (ICFEM), Manchester, UK
Verification of JCSP ProgramsVladimir Klebanov
Philipp Rümmer
Steffen Schlager
Peter H. Schmitt
Communicating Process Architectures (CPA), Proceedings
Reusing Proofs when Program Verification Systems are ModifiedBernhard Beckert
Thorsten Bormer
Vladimir Klebanov
Proceedings, Software Certificate Management Workshop (SoftCeMent), Long Beach, California, USA
Bereitstellung und Zuweisung von Ressourcen in der formalen algorithmischen SyntheseMattias UlbrichStudienarbeit, Fakultät für Informatik, Universität Karlsruhe
Second-Order Principles in Specification Languages for Object-Oriented ProgramsBernhard Beckert
Kerry Trentelman
Proceedings, 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
Peter H. Schmitt
Software and System Modeling
Email Client Verification GoalsBernhard Beckert
Gerd Beuster
Verisoft Project
TABLEAUX 2005: Position Papers and Tutorial DescriptionsBernhard BeckertUniversität Koblenz-Landau
2004
Title Author(s) Source
Proof Reuse for Deductive Program VerificationBernhard Beckert
Vladimir Klebanov
Proceedings, 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
Pia Breuer
Verisoft Project
Taclets: A New Paradigm for Constructing Interactive Theorem ProversBernhard Beckert
Martin Giese
Elmar Habermalz
Reiner Hähnle
Andreas Roth
Philipp Rümmer
Steffen Schlager
Department of Computer Science, University of Koblenz
Software Verification with Integrated Data Type Refinement for Integer ArithmeticBernhard Beckert
Steffen Schlager
Proceedings, International Conference on Integrated Formal Methods, Canterbury, UK
Formal Specification of Security-relevant Properties of User InterfacesBernhard Beckert
Gerd Beuster
Proceedings, 3rd International Workshop on Critical Systems Development with UML, Lisbon, Portugal
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
Peter H. Schmitt
Department of Computing Science, Chalmers University and Göteborg University, Göteborg, Sweden
Program Verification Using Change InformationBernhard Beckert
Peter H. Schmitt
Proceedings, Software Engineering and Formal Methods (SEFM), Brisbane, Australia
A Program Logic for Handling Java Card's Transaction MechanismBernhard Beckert
Wojciech Mostowski
Proceedings, Fundamental Approaches to Software Engineering (FASE), Warsaw, Poland
Depth-first Proof Search without Backtracking for Free-variable Clausal TableauxBernhard BeckertJournal of Symbolic Computation
2002
Title Author(s) Source
Integer Arithmetic in the Specification and Verification of Java ProgramsBernhard Beckert
Steffen Schlager
Proceedings, 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
Peter H. Schmitt
Fundamental 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
Peter H. Schmitt
Proceedings, VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen, Denmark
2001
Title Author(s) Source
An Extension of Dynamic Logic for Modelling OCL's @pre OperatorThomas Baar
Bernhard Beckert
Peter H. Schmitt
Proceedings, Fourth Andrei Ershov International Conference, Perspectives of System Informatics, Novosibirsk, Russia
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
A Sequent Calculus for First-order Dynamic Logic with Trace ModalitiesBernhard Beckert
Steffen Schlager
Proceedings, International Joint Conference on Automated Reasoning, Siena, Italy
Handling Java's Abrupt Termination in a Sequent Calculus for Dynamic LogicBernhard Beckert
Bettina Sasse
Proceedings, 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
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
Peter H. Schmitt
Proceedings, 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
Peter H. Schmitt
Proceedings, 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
Peter H. Schmitt
Proceedings, Java Card Workshop (JCW), Cannes, France
A Dynamic Logic for Java CardBernhard BeckertProceedings, 2nd ECOOP Workshop on Formal Techniques for Java Programs, 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