@inbook{KlamrothEtAl2022,
title = {The Karlsruhe Java Verification Suite},
author = {Jonas Klamroth and Florian Lanzinger and Wolfram Pfeifer and Mattias Ulbrich},
editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Einar Broch Johnsen},
url = {https://doi.org/10.1007/978-3-031-08166-8_14},
doi = {10.1007/978-3-031-08166-8_14},
isbn = {978-3-031-08166-8},
year  = {2022},
date = {2022-07-01},
booktitle = {The Logic of Software. A Tasting Menu of Formal Methods: 
 Essays Dedicated to Reiner H\"{a}hnle on the Occasion of 
 His 60th Birthday},
pages = {290--312},
publisher = {Springer International Publishing},
keywords = {},
pubstate = {published},
tppubtype = {inbook}
}
@inproceedings{BoerGouwKlamroth2022_1000148092,
title = {Formal Specification and Verification of JDK’s Identity Hash Map Implementation},
author = {Martin Boer and Stijn Gouw and Jonas Klamroth and Christian Jung and Mattias Ulbrich and Alexander Weigl},
editor = {Maurice H. Beek and Rosemary Monahan},
doi = {10.1007/978-3-031-07727-2_4},
isbn = {978-3-031-07727-2},
year  = {2022},
date = {2022-06-01},
booktitle = {17th International Conference on integrated Formal Methods (iFM 2022)},
volume = {13274},
pages = {45--62},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{KramerBDDUlbrich22,
title = {Inferring Interval-Valued Floating-Point Preconditions},
author = {Jonas Kr\"{a}mer and Lionel Blatter and Eva Darulova and Mattias Ulbrich},
editor = {Dana Fisman and Grigore Rosu},
url = {https://doi.org/10.1007/978-3-030-99524-9_16},
doi = {10.1007/978-3-030-99524-9_16},
year  = {2022},
date = {2022-04-01},
booktitle = {28th International Conference on Tools and Algorithms for 
 the Construction and Analysis of Systems (TACAS 2022), 
 held as part of ETAPS 2022: European Joint Conferences 
 on Theory and Practice of Software},
volume = {13243},
pages = {303--321},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/fase/GratzHB22,
title = {Finding Semantic Bugs Fast},
author = {Lukas Gr\"{a}tz and Reiner H\"{a}hnle and Richard Bubel},
editor = {Einar Broch Johnsen and Manuel Wimmer},
url = {https://doi.org/10.1007/978-3-030-99429-7_8},
doi = {10.1007/978-3-030-99429-7_8},
year  = {2022},
date = {2022-01-01},
booktitle = {Fundamental Approaches to Software Engineering - 25th International 
 Conference, FASE 2022, Held as Part of the European Joint Conferences 
 on Theory and Practice of Software, ETAPS 2022, Munich, Germany, 
 April 2-7, 2022, Proceedings},
volume = {13241},
pages = {145--154},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/icse-formalise/TabarBH22,
title = {Automatic Loop Invariant Generation for Data Dependence Analysis},
author = {Asmae Heydari Tabar and Richard Bubel and Reiner H\"{a}hnle},
url = {https://doi.org/10.1145/3524482.3527649},
doi = {10.1145/3524482.3527649},
year  = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
booktitle = {10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2022, Pittsburgh, PA, USA, May 22-23, 
 2022},
pages = {34--45},
publisher = {ACM},
keywords = {Abstract Predicates, deductive verification, Invariant generation},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/isola/BeckertBHU22,
title = {Towards a Usable and Sustainable Deductive Verification Tool},
author = {Bernhard Beckert and Richard Bubel and Reiner H\"{a}hnle and Mattias Ulbrich},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://doi.org/10.1007/978-3-031-19756-7_16},
doi = {10.1007/978-3-031-19756-7_16},
year  = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. 
 Software Engineering - 11th International Symposium, ISoLA 2022, Rhodes, 
 Greece, October 22-30, 2022, Proceedings, Part II},
volume = {13702},
pages = {281--300},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {deductive verification, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@incollection{DBLP:books/mc/22/Hahnle22,
title = {Dijkstra's Legacy on Program Verification},
author = {Reiner H\"{a}hnle},
editor = {Krzysztof R. Apt and Tony Hoare},
url = {https://doi.org/10.1145/3544585.3544593},
doi = {10.1145/3544585.3544593},
year  = {2022},
date = {2022-01-01},
urldate = {2022-01-01},
booktitle = {Edsger Wybe Dijkstra: His Life, Work, and Legacy},
pages = {105--140},
publisher = {ACM / Morgan \& Claypool},
keywords = {Verification},
pubstate = {published},
tppubtype = {incollection}
}
@article{LanzingerWeiglUlbrich2021_1000139256,
title = {Scalability and Precision by Combining Expressive Type Systems and Deductive Verification},
author = {Florian Lanzinger and Alexander Weigl and Mattias Ulbrich and Werner Dietl},
doi = {10.1145/3485520},
issn = {2475-1421},
year  = {2021},
date = {2021-10-01},
journal = {Proceedings of the ACM on programming languages},
volume = {5},
number = {OOPSLA},
pages = {Article no: 143},
publisher = {Association for Computing Machinery (ACM)},
note = {46.23.01; LK 01},
keywords = {deductive verification, Pluggable type systems, Refinement types},
pubstate = {published},
tppubtype = {article}
}
@inproceedings{AbbasiSchifflEtAl2021,
title = {Deductive Verification of Floating-Point Java Programs in KeY},
author = {Rosa Abbasi and Jonas Schiffl and Eva Darulova and Mattias Ulbrich and Wolfgang Ahrendt},
editor = {Jan Friso Groote and Kim Guldstrand Larsen},
doi = {10.1007/978-3-030-72013-1_13},
year  = {2021},
date = {2021-03-01},
booktitle = {27th 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},
volume = {12652},
pages = {242--261},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
abstract = {Deductive verification has been successful in verifying interesting 
 properties of real-world programs. One notable gap is the limited support 
 for floating-point reasoning. This is unfortunate, as floating-point 
 arithmetic is particularly unintuitive to reason about due to rounding as 
 well as the presence of the special values infinity and `Not a Number' (NaN). 
 In this paper, we present the first floating-point support in a deductive 
 verification tool for the Java programming language. Our support in the KeY verifier handles 
 arithmetic via floating-point decision procedures inside SMT solvers 
 and transcendental functions via axiomatization. 
 We evaluate this integration on new benchmarks, and show that this approach 
 is powerful enough to prove the absence of floating-point special 
 values---often a prerequisite for further reasoning about numerical 
 computations---as well as certain functional properties for realistic benchmarks.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{PfeiferSchifflUlbrich2021,
title = {Reconstructing Z3 proofs in KeY: There and back again},
author = {Wolfram Pfeifer and 
Jonas Schiffl and
Mattias Ulbrich},
doi = {10.1145/3464971.3468421},
isbn = {978-1-4503-8543-5},
year  = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs : 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021, Online, 13 July 2021 - null},
pages = {24--31},
publisher = {Association for Computing Machinery (ACM)},
series = {ACM Conferences},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/gpce/ScalettaHSB21,
title = {Delta-based verification of software product families},
author = {Marco Scaletta and Reiner H\"{a}hnle and Dominic Steinh\"{o}fel and Richard Bubel},
editor = {Eli Tilevich and Coen De Roover},
url = {https://doi.org/10.1145/3486609.3487200},
doi = {10.1145/3486609.3487200},
year  = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17 
 - 18, 2021},
pages = {69--82},
publisher = {ACM},
keywords = {deductive verification, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/fase/AlbertHMS21,
title = {Certified Abstract Cost Analysis},
author = {Elvira Albert and Reiner H\"{a}hnle and Alicia Merayo and Dominic Steinh\"{o}fel},
editor = {Esther Guerra and Mari\"{e}lle Stoelinga},
url = {https://doi.org/10.1007/978-3-030-71500-7_2},
doi = {10.1007/978-3-030-71500-7_2},
year  = {2021},
date = {2021-01-01},
urldate = {2021-01-01},
booktitle = {Fundamental Approaches to Software Engineering - 24th International 
 Conference, FASE 2021, Held as Part of the European Joint Conferences 
 on Theory and Practice of Software, ETAPS 2021, Luxembourg City, 
 Luxembourg, March 27 - April 1, 2021, Proceedings},
volume = {12649},
pages = {24--45},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {deductive verification, Resource Analysis},
pubstate = {published},
tppubtype = {inproceedings}
}
@phdthesis{DBLP:phd/dnb/Steinhofel20,
title = {Abstract Execution: Automatically Proving Infinitely Many Programs},
author = {Dominic Steinh\"{o}fel},
url = {http://tuprints.ulb.tu-darmstadt.de/8540/},
year  = {2020},
date = {2020-01-01},
school = {Darmstadt University of Technology, Germany},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
@inproceedings{DBLP:conf/isola/HahnleTMNS020,
title = {Safer Parallelization},
author = {Reiner H\"{a}hnle and Asmae Heydari Tabar and Arya Mazaheri and Mohammad Norouzi and Dominic Steinh\"{o}fel and Felix Wolf},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://doi.org/10.1007/978-3-030-61470-6_8},
doi = {10.1007/978-3-030-61470-6_8},
year  = {2020},
date = {2020-01-01},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: 
 Engineering Principles - 9th International Symposium on Leveraging 
 Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 
 20-30, 2020, Proceedings, Part II},
volume = {12477},
pages = {117--137},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/isola/AhrendtB20,
title = {Functional Verification of Smart Contracts via Strong Data Integrity},
author = {Wolfgang Ahrendt and Richard Bubel},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://doi.org/10.1007/978-3-030-61467-6_2},
doi = {10.1007/978-3-030-61467-6_2},
year  = {2020},
date = {2020-01-01},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: 
 Applications - 9th International Symposium on Leveraging Applications 
 of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, 
 Proceedings, Part III},
volume = {12478},
pages = {9--24},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@article{Hentschel2018,
title = {The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more},
author = {Martin Hentschel and Richard Bubel and Reiner H\"{a}hnle},
url = {https://doi.org/10.1007/s10009-018-0490-9},
doi = {10.1007/s10009-018-0490-9},
issn = {1433-2787},
year  = {2019},
date = {2019-09-01},
journal = {International Journal on Software Tools for Technology Transfer},
abstract = {The Symbolic Execution Debugger (SED), is an extension of the debug platform for interactive debuggers based on symbolic execution. The SED comes with a static symbolic execution engine for sequential programs, but any third-party symbolic execution engine can be integrated into the SED. An interactive debugger based on symbolic execution allows one like a traditional debugger to locate defects in the source code. The difference is that all feasible execution paths are explored at once, and thus there is no need to know input values resulting in an execution that exhibits the failure. In addition, such a debugger can be used in code reviews and to guide and present results of an analysis based on symbolic execution such as, in our case, correctness proofs. Experimental evaluations proved that the SED increases the effectiveness of code reviews and proof understanding tasks.},
keywords = {Debugging, Symbolic Execution},
pubstate = {published},
tppubtype = {article}
}
@inproceedings{DBLP:conf/fsen/AhrendtBEPPRS19,
title = {Verification of Smart Contract Business Logic - Exploiting a Java 
 Source Code Verifier},
author = {Wolfgang Ahrendt and Richard Bubel and Joshua Ellul and Gordon J Pace and Raul Pardo and Vincent Rebiscoul and Gerardo Schneider},
editor = {Hossein Hojjat and Mieke Massink},
url = {https://doi.org/10.1007/978-3-030-31517-7_16},
doi = {10.1007/978-3-030-31517-7_16},
year  = {2019},
date = {2019-01-01},
booktitle = {Fundamentals of Software Engineering - 8th International Conference, 
 FSEN 2019, Tehran, Iran, May 1-3, 2019, Revised Selected Papers},
volume = {11761},
pages = {228--243},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/fm/SteinhofelH19,
title = {Abstract Execution},
author = {Dominic Steinh\"{o}fel and Reiner H\"{a}hnle},
editor = {Maurice H ter Beek and Annabelle McIver and Jos \'{e}},
url = {https://doi.org/10.1007/978-3-030-30942-8_20},
doi = {10.1007/978-3-030-30942-8_20},
year  = {2019},
date = {2019-01-01},
booktitle = {Formal Methods - The Next 30 Years - Third World Congress, FM 2019, 
 Porto, Portugal, October 7-11, 2019, Proceedings},
volume = {11800},
pages = {319--336},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{dali2019,
title = {The Trace Modality},
author = {Dominic Steinh\"{o}fel and Reiner H\"{a}hnle},
editor = {Alexandru Baltag and Luis S Barbosa},
year  = {2019},
date = {2019-01-01},
booktitle = {2nd Workshop on Dynamic Logic: New Trends and Applications},
publisher = {Springer},
address = {Porto, Portugal},
series = {Lecture Notes in Computer Science},
note = {Accepted, in print.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{BHT19,
title = {A Program Logic For Dependence Analysis},
author = {Richard Bubel and Reiner H\"{a}hnle and Asmae Heydari Tabar},
editor = {Wolfgang Ahrendt and Silvia Lizeth Tapia Tarifa},
year  = {2019},
date = {2019-01-01},
booktitle = {Integrated Formal Methods, 15th International Conference, 
 iFM, Bergen, Norway},
publisher = {Springer},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@phdthesis{Grebing19,
title = {User Interaction in Deductive Interactive Program Verification},
author = {Sarah Caecilia Grebing},
doi = {10.5445/IR/1000099121},
year  = {2019},
date = {2019-01-01},
school = {Karlsruhe Institute of Technology},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
@inproceedings{GrebingKlamrothUlbrich19,
title = {Seamless Interactive Program Verification},
author = {Sarah Grebing and Jonas Klamroth and Mattias Ulbrich},
year  = {2019},
date = {2019-01-01},
booktitle = {11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019)},
publisher = {Springer Publishing},
address = {New York City, USA},
series = {LNCS},
note = {To appear},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{BeckertHerdaEtAl18,
title = {Towards a Notion of Coverage for Incomplete Program-Correctness Proofs},
author = {Bernhard Beckert and Mihai Herda and Stefan Kobischke and Mattias Ulbrich},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://doi.org/10.1007/978-3-030-03421-4_4},
doi = {10.1007/978-3-030-03421-4_4},
year  = {2018},
date = {2018-11-01},
booktitle = {8th International Symposium on Leveraging Applications of Formal Methods, 
 Verification and Validation (ISoLA 2018)},
volume = {11245},
pages = {53--63},
publisher = {Springer},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{steinhoefel-haehnle-2018,
title = {Modular, Correct Compilation with Automatic Soundness Proofs},
author = {Dominic Steinh\"{o}fel and Reiner H\"{a}hnle},
editor = {Tiziana Margaria and Bernhard Steffen},
url = {https://link.springer.com/chapter/10.1007%2F978-3-030-03418-4_25},
doi = {10.1007/978-3-030-03418-4_25},
issn = {0302-9743},
year  = {2018},
date = {2018-01-01},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Modeling},
volume = {11244},
pages = {424--447},
publisher = {Springer International Publishing},
address = {Cham},
series = {Lecture Notes in Computer Science},
abstract = {Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort. We propose a framework for automatically proving the correctness of compilation rules based on simultaneous symbolic execution for the source and target language. The correctness of the whole system follows from the correctness of each compilation rule. To support a new source or target language it is sufficient to formalize that language in terms of symbolic execution, while the corresponding formalization of its counterpart can be re-used. The correctness of translation rules can be checked automatically. Our approach is based on a reduction of correctness assertions to formulas in a program logic capable of symbolic execution of abstract programs. We instantiate the framework for compilation from Java to LLVM IR and provide a symbolic execution system for a subset of LLVM IR.},
keywords = {Compilation, Integration of Formal Methods into Software Engineering Practice, LLVM, Symbolic Execution, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@mastersthesis{SchifflMSc2018,
title = {Specification and Verification of Hyperledger Fabric Chaincode},
author = {Jonas Schiffl},
year  = {2018},
date = {2018-01-01},
address = {Karlsruhe, Germany},
school = {Karlsruhe Institute of Technology},
keywords = {},
pubstate = {published},
tppubtype = {mastersthesis}
}
@inproceedings{BeckertBischofEA2018,
title = {Using Theorem Provers to Increase the Precision of  Dependence Analysis for Information Flow Control},
author = {Bernhard Beckert and Simon Bischof and Mihai Herda and Michael Kirsten and Marko Kleine B\"{u}ning},
editor = {Jing Sun and Meng Sun},
doi = {10.1007/978-3-030-02450-5_17},
year  = {2018},
date = {2018-01-01},
booktitle = {20th International Conference on Formal Engineering 
 Methods - Formal Methods and Software Engineering 
 (ICFEM 2018)},
volume = {11232},
pages = {284--300},
publisher = {Springer},
address = {Gold Coast, QLD, Australia},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@phdthesis{Greiner2018PhD,
title = {A Framework for Non-Interference in Component-Based 
Systems},
author = {Simon Greiner},
doi = {10.5445/IR/1000082042},
year  = {2018},
date = {2018-01-01},
school = {Karlsruhe Institute of Technology},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}
@inproceedings{uitp2018,
title = {Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons 
 Learned},
author = {Sarah Grebing and An Thuy Tien Luong and Alexander Weigl},
editor = {Mateja Jamnik and Christoph L\"{u}th},
year  = {2018},
date = {2018-01-01},
booktitle = {13th International Workshop on User Interfaces for Theorem Provers (UITP 2018)},
note = {To appear, %snip pdf=https://formal.iti.kit.edu/~grebing/pub/uitp2018.pdf},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@techreport{Kramer2017,
title = {Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems},
author = {Max E. and Martin Hecker and Simon Greiner and Kaibin Bao and Kateryna Yurchenko},
doi = {10.5445/IR/1000076957},
issn = {2190-4782},
year  = {2017},
date = {2017-12-01},
number = {2017,12},
address = {Karlsruhe},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
@inproceedings{Schmitt2017,
title = {A Mechanizable First-Order Theory of Ordinals},
author = {Peter H. Schmitt},
editor = {Renate A. Schmidt and Claudia Nalon},
url = {https://www.key-project.org/papers/ordinal-numbers},
doi = {10.1007/978-3-319-66902-1_20},
isbn = {978-3-319-66901-4},
year  = {2017},
date = {2017-09-06},
urldate = {2017-09-06},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 26th
International Conference, {TABLEAUX} 2017, Brasilia, Brazil,
September 25-28, 2017, Proceedings},
volume = {10501},
pages = {331--346},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
abstract = {We present a first-order theory of ordinals without resorting to set theory. The theory is implemented in the
 KeY program verification system which is in turn used to prove termination of a Java program computing 
the Goodstein sequences.},
keywords = {theorem proving},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{BeckertEtAl2017a,
title = {Proving JDK's Dual Pivot Quicksort Correct},
author = {Bernhard Beckert and Jonas Schiffl and Peter H. Schmitt and Mattias Ulbrich},
url = {https://formal.iti.kit.edu/biblio/?lang=en\&key=BeckertEtAl2017a},
year  = {2017},
date = {2017-07-22},
booktitle = {9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017)},
note = {To appear },
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@article{deGouw2017,
title = {Verifying OpenJDK's Sort Method for Generic Collections},
author = {Stijn de Gouw and Frank S de Boer and Richard Bubel and Reiner H\"{a}hnle and Jurriaan Rot and Dominic Steinh\"{o}fel},
url = {https://doi.org/10.1007/s10817-017-9426-4},
doi = {10.1007/s10817-017-9426-4},
issn = {1573-0670},
year  = {2017},
date = {2017-01-01},
journal = {Journal of Automated Reasoning},
abstract = {TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered a bug which causes the implementation to crash by an uncaught exception. In this paper, we identify conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise performance. We formally specify the new version and verify termination and the absence of exceptions including the bug. This verification is carried out mechanically with KeY, a state-of-the-art interactive verification tool for Java. We provide a detailed description and analysis of the proofs. The complexity of the proofs required extensions and new capabilities in KeY, including symbolic state merging.},
keywords = {Java Runtime Library, Real-World Code, Sorting, State Merging, Verification},
pubstate = {published},
tppubtype = {article}
}
@inproceedings{Do2017,
title = {Inferring Secrets by Guided Experiments},
author = {Quoc Huy Do and Richard Bubel and Reiner H\"{a}hnle},
editor = {Dang Van Hung and Deepak Kapur},
url = {https://doi.org/10.1007/978-3-319-67729-3_16},
doi = {10.1007/978-3-319-67729-3_16},
year  = {2017},
date = {2017-01-01},
booktitle = {Theoretical Aspects of Computing -- ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings},
pages = {269--287},
publisher = {Springer International Publishing},
address = {Cham},
keywords = {secure information flow, Test Case Generation},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/ifm/SteinhofelW17,
title = {A New Invariant Rule for the Analysis of Loops with Non-standard Control  Flows},
author = {Dominic Steinh\"{o}fel and Nathan Wasser},
editor = {Nadia Polikarpova and Steve Schneider},
url = {https://doi.org/10.1007/978-3-319-66845-1_18},
doi = {10.1007/978-3-319-66845-1_18},
year  = {2017},
date = {2017-01-01},
booktitle = {Integrated Formal Methods - 13th International Conference, IFM 2017, 
 Turin, Italy, September 20-22, 2017, Proceedings},
volume = {10510},
pages = {279--294},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{BeckertGrebingUlbrich2017,
title = {An Interaction Concept for Program Verification 
 Systems with Explicit Proof Object},
author = {Bernhard Beckert and Sarah Grebing and Mattias Ulbrich},
doi = {10.1007/978-3-319-70389-3_11},
isbn = {978-3-319-70389-3},
year  = {2017},
date = {2017-01-01},
booktitle = {Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017)},
volume = {10629},
pages = {163--178},
publisher = {Springer International Publishing},
address = {Cham},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@book{KeYBook2016,
title = {Deductive Software Verification - The KeY Book - From Theory to Practice},
editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Reiner H\"{a}hnle and Peter H. Schmitt and Mattias Ulbrich},
url = {http://dx.doi.org/10.1007/978-3-319-49812-6},
doi = {10.1007/978-3-319-49812-6},
isbn = {978-3-319-49811-9},
year  = {2016},
date = {2016-12-16},
volume = {10001},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {},
pubstate = {published},
tppubtype = {book}
}
@inproceedings{HentschelHB16ASE16a,
title = {An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier},
author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel},
isbn = {978-1-4503-3845-5},
year  = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
pages = {403-413},
publisher = {ACM},
address = {Singapore, Singapore},
series = {ASE 2016},
abstract = {Theorem provers have highly complex interfaces, but there are not many systematic studies of their usability and effectiveness. Specifically, for interactive theorem provers the ability to quickly comprehend intermediate proof situations is of pivotal importance. In this paper we present the (as far as we know) first empirical study that systematically compares the effectiveness of different user interfaces of an interactive theorem prover. We juxtapose two different user interfaces of the interactive verifier KeY: the traditional one which focuses on proof objects and a more recent one that provides a view akin to an interactive debugger. We carefully designed a controlled experiment where users were given various proof understanding tasks that had to be solved with alternating interfaces. We provide statistical evidence that the conjectured higher effectivity of the debugger-like interface is not just a hunch.},
keywords = {Empirical Evaluation, Proof Understanding, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{	HentschelHB16ASE16b,
title = {The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts},
author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel},
isbn = {978-1-4503-3845-5},
year  = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
pages = {846--851},
publisher = {ACM},
address = {Singapore, Singapore},
series = {ASE 2016},
abstract = {The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w.},
keywords = {Debugging, Program Execution Visualization, Proof Understanding, Symbolic Execution, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@phdthesis{	TUD-CS-2016-0099,
title = {Integrating Symbolic Execution, Debugging and Verification},
author = {Martin Hentschel},
year  = {2016},
date = {2016-01-01},
school = {Technische Universit\"{a}t Darmstadt},
abstract = {In modern software development, almost all activities are centered around an integrated development environment (IDE). Besides the main use cases to write, execute and debug source code, an IDE serves also as front-end for other tools involved in the development process such as a version control system or an application lifecycle management. Independent from the applied development process, the techniques to ensure correct software are always the same. The general goal is to find defects as soon as possible, because the sooner a defect is found, the easier and cheaper it is to fix. In the first place, the programming language helps to prevent some kinds of defects. Once something is written, it is effective to review it not only to find defects, but also to increase its quality. Also tools which statically analyze the source code help to find defects automatically. In addition, testing is used to ensure that selected usage scenarios behave as expected. However, a test can only show the presence of a failure and not its absence. To ensure that a program is correct, it needs to be proven that the program complies to a formal specification describing the desired behavior. This is done by formal verification tools. Finally, whenever a failure is observed, debugging takes place to locate the defect. This thesis extends the software development tool suite by an interactive debugger based on symbolic execution, a technique to explore all feasible execution paths up to a given depth simultaneously. Such a tool can not only be used for classical debugging activities, but also during code reviews or in order to present results of an analysis based on symbolic execution. The contribution is an extension of symbolic execution to explore the full program behavior even in presence of loops and recursive method calls. This is achieved by integrating specifications in form of loop invariants and methods contracts into a symbolic execution engine. How such a symbolic execution engine based on verification proofs can be realized is presented as well. In addition, the presented Symbolic Execution Debugger (SED) makes the Eclipse platform ready for debuggers based on symbolic execution. Its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all program execution paths are explored simultaneously. To support program comprehension, program execution paths as well as intermediate states are visualized. By default, the SED comes with a symbolic execution engine implemented on top of the KeY verification system. Statistical evidence that the SED increases effectiveness of code reviews is gained from a controlled experiment. Another novelty of the SED is that arbitrary verification proofs can be inspected. Whereas traditional user interfaces of verification tools present proof states in a mathematical fashion, the SED analyzes the full proof and presents different aspects of it using specialized views. A controlled experiment gives statistical evidence that proof understanding tasks are more effective using the SED by comparing its user interface with the original one of KeY. The SED allows one to interact with the underlying prover by adapting code and specifications in an auto-active flavor, which creates the need to manage proofs directly within an IDE. A presented concept achieves this, by integrating a semi-automatic verification tool into an IDE. It includes several optimizations to reduce the overall proof time and can be realized without changing the verification tool. An optimal user experience is achieved only if all aspects of verification are directly supported within the IDE. Thus a thorough integration of KeY into Eclipse is presented, which for instance includes in addition to the proof management capabilities to edit JML specifications and to setup the needed infrastructure for verification with KeY. Altogether, a platform for tools based on symbolic execution and related to verification is presented, which offers a seamless integration into an IDE and furthers a usage in combination. Furthermore, many aspects, like the way the SED presents proof attempts to users, help to reduce the barrier of using formal methods.},
keywords = {Code Review, Debugging, Empirical Evaluation, Integration of Formal Methods into Software Engineering Practice, Program Execution Visualization, Proof Understanding, Symbolic Execution, Verification},
pubstate = {published},
tppubtype = {phdthesis}
}
@inproceedings{ThumWSHK16,
title = {Variability Hiding in Contracts for Dependent Software Product Lines},
author = {Thomas Th\"{u}m and Tim Winkelmann and Reimar Schr\"{o}ter and Martin Hentschel and Stefan Kr\"{u}ger},
isbn = {978-1-4503-4019-9},
year  = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the Tenth International Workshop on Variability Modelling of Software-intensive Systems},
pages = {97--104},
publisher = {ACM},
address = {Salvador, Brazil},
series = {VaMoS '16},
abstract = {Software product lines are used to efficiently develop and verify similar software products. While they focus on reuse of artifacts between products, a product line may also be reused itself in other product lines. A challenge with such dependent product lines is evolution; every change in a product line may influence all dependent product lines. With variability hiding, we aim to hide certain features and their artifacts in dependent product lines. In prior work, we focused on feature models and implementation artifacts. We build on this by discussing how variability hiding can be extended to specifications in terms of method contracts. We illustrate variability hiding in contracts by means of a running example and share our insights with preliminary experiments on the benefits for formal verification. In particular, we find that not every change in a certain product line requires a re-verification of other dependent product lines.},
keywords = {deductive verification, method contracts, Multi product line},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DorreK15,
title = {Pseudo-Random Number Generator Verification: A Case Study},
author = {Felix D\"{o}rre and Vladimir Klebanov},
url = {http://dx.doi.org/10.1007/978-3-319-29613-5_4},
doi = {10.1007/978-3-319-29613-5_4},
isbn = {978-3-319-29612-8},
year  = {2016},
date = {2016-01-01},
booktitle = {Revised Selected Papers of the 7th International Conference on Verified Software: Theories, Tools, and Experiments},
volume = {9593},
pages = {61--72},
publisher = {Springer-Verlag New York, Inc.},
address = {San Francisco, CA, USA},
series = {VSTTE 2015},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{scheurer.hahnle.ea_general-lattice-model_16,
title = {A General Lattice Model for Merging Symbolic Execution Branches},
author = {Dominic Scheurer and Reiner H\"{a}hnle and Richard Bubel},
editor = {Kazuhiro Ogata and Mark Lawford and Shaoying Liu},
url = {http://link.springer.com/chapter/10.1007/978-3-319-47846-3_5
/wp-content/uploads/2016/12/SHB-General_Lattice_Model-2016.pdf},
doi = {10.1007/978-3-319-47846-3_5},
year  = {2016},
date = {2016-01-01},
booktitle = {Formal Methods and Software Engineering - 18th International Conference 
 on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 
 14-18, 2016, Proceedings},
volume = {10009},
pages = {57--73},
publisher = {Springer International Publishing},
series = {LNCS},
abstract = {Symbolic execution is a software analysis technique that has been used with success in the past years in program testing and verification. A main bottleneck of symbolic execution is the path explosion problem: the number of paths in a symbolic execution tree is exponential in the number of static branches of the executed program. Here we put forward an abstraction-based framework for state merging in symbolic execution. We show that it subsumes existing approaches and prove soundness. The method was implemented in the verification system KeY. Our empirical evaluation shows that reductions in proof size of up to 80 % are possible by state merging when applied to complex verification problems; new proofs become feasible that were out of reach so far.},
keywords = {Path Explosion, Predicate Abstraction, State Merging, Symbolic Execution, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DoKW16,
title = {Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study},
author = {Quoc Huy Do and Eduard Kamburjan and Nathan Wasser},
url = {http://dx.doi.org/10.1007/978-3-662-49635-0_6},
doi = {10.1007/978-3-662-49635-0_6},
isbn = {978-3-662-49634-3},
year  = {2016},
date = {2016-01-01},
booktitle = {Proceedings of the 5th International Conference on Principles of Security and Trust - Volume 9635},
pages = {97--115},
publisher = {Springer-Verlag New York, Inc.},
address = {New York, NY, USA},
keywords = {Invariant generation, secure information flow, Test Case Generation},
pubstate = {published},
tppubtype = {inproceedings}
}
@article{MostowskiU16,
title = {Dynamic Dispatch for Method Contracts Through Abstract Predicates},
author = {Wojciech Mostowski and Mattias Ulbrich},
url = {http://dx.doi.org/10.1007/978-3-319-46969-0_7},
doi = {10.1007/978-3-319-46969-0_7},
year  = {2016},
date = {2016-01-01},
journal = {Trans. Modularity and Composition},
volume = {1},
pages = {238--267},
crossref = {DBLP:journals/taosd/2016-1},
keywords = {Verification},
pubstate = {published},
tppubtype = {article}
}
@inproceedings{HentschelHB16iFM,
title = {Can Formal Methods Improve the Efficiency of Code Reviews?},
author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel},
url = {http://dx.doi.org/10.1007/978-3-319-33693-0_1},
doi = {10.1007/978-3-319-33693-0_1},
year  = {2016},
date = {2016-01-01},
booktitle = {Integrated Formal Methods - 12th International Conference, IFM 2016, 
 Reykjavik, Iceland, June 1-5, 2016, Proceedings},
pages = {3--19},
keywords = {Code Review, Debugging},
pubstate = {published},
tppubtype = {inproceedings}
}
@phdthesis{DBLP:phd/dnb/Wasser16,
title = {Automatic generation of specifications using verification tools =  Automatische Spezifikationserzeugung mit Hilfe von Verifikationswerkzeugen},
author = {Nathan Wasser},
url = {http://tuprints.ulb.tu-darmstadt.de/5910/},
year  = {2016},
date = {2016-01-01},
school = {Darmstadt University of Technology, Germany},
keywords = {Verification},
pubstate = {published},
tppubtype = {phdthesis}
}
@inproceedings{beckert.klebanov.ea:regression,
title = {Regression Verification for Java Using a Secure Information Flow Calculus},
author = {Bernhard Beckert and Vladimir Klebanov and Mattias Ulbrich},
isbn = {978-1-4503-3656-7},
year  = {2015},
date = {2015-01-01},
booktitle = {Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs},
pages = {6:1--6:6},
publisher = {ACM},
address = {Prague, Czech Republic},
series = {FTfJP '15},
keywords = {formal methods, program equivalence, regression verification, secure information flow},
pubstate = {published},
tppubtype = {inproceedings}
}
@article{bruns.mostowski.ea:implementation-level,
title = {Implementation-level Verification of Algorithms with KeY},
author = {Daniel Bruns and Wojciech Mostowski and Mattias Ulbrich},
url = {http://link.springer.com/article/10.1007/s10009-013-0293-y},
doi = {10.1007/s10009-013-0293-y},
issn = {1433-2779},
year  = {2015},
date = {2015-01-01},
journal = {Software Tools for Technology Transfer},
volume = {17},
number = {6},
pages = {729--744},
publisher = {Springer},
abstract = {We give an account on the authors' experience and results from the software verification competition held at the Formal Methods~2012 conference. Competitions like this are meant to provide a benchmark for verification systems. It consisted of three algorithms which the authors have implemented in Java, specified with the Java Modeling Language, and verified using the KeY system. Building on our solutions, we argue that verification systems which target implementations in real-world programming languages are required to have powerful capabilities for abstraction. Regarding the KeY tool, we explain features which, driven by the competition, have been freshly implemented to accommodate for these demands.},
keywords = {Verification},
pubstate = {published},
tppubtype = {article}
}
@inproceedings{MostowskiU15,
title = {Dynamic Dispatch for Method Contracts through Abstract Predicates},
author = {Wojciech Mostowski and Mattias Ulbrich},
url = {http://doi.acm.org/10.1145/2724525.2724574},
doi = {10.1145/2724525.2724574},
year  = {2015},
date = {2015-01-01},
booktitle = {Proceedings of the 14th International Conference on Modularity, MODULARITY 
 2015, Fort Collins, CO, USA, March 16 - 19, 2015},
pages = {109--116},
publisher = {ACM},
keywords = {Abstract Predicates, Design by Contract, Dynamic Dispatch, JML, Modular Specification, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DoBH15,
title = {Exploit Generation for Information Flow Leaks in Object-Oriented Programs},
author = {Quoc Huy Do and Richard Bubel and Reiner H\"{a}hnle},
url = {http://dx.doi.org/10.1007/978-3-319-18467-8_27},
doi = {10.1007/978-3-319-18467-8_27},
year  = {2015},
date = {2015-01-01},
booktitle = {ICT Systems Security and Privacy Protection - 30th IFIP TC 11 
 International Conference, SEC 2015, Hamburg, Germany, May 26-28, 
 2015, Proceedings},
pages = {401--415},
keywords = {secure information flow, Test Case Generation},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{KuestersTruderungBeckertEA2015,
title = {A Hybrid Approach for Proving Noninterference of Java Programs},
author = {Ralf K\"{u}sters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and Michael Kirsten and Martin Mohr},
editor = {C\'{e}dric Fournet and Michael Hicks},
doi = {10.1109/CSF.2015.28},
year  = {2015},
date = {2015-01-01},
booktitle = {28th IEEE Computer Security Foundations Symposium (CSF 2015)},
pages = {305-319},
abstract = {Several tools and approaches for proving noninterference properties for Java and other languages exist. 
 Some of them have a high degree of automation or are even fully automatic, but overapproximate 
 the actual information flow, and hence, may produce false positives. 
 Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence, 
 analysis is time-consuming. 
 
 
 In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches: 
 We want to use fully automatic analysis as much as possible and only at places in a program where, 
 due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive 
 analysis, where the latter involves only the verification of specific functional properties in certain 
 parts of the program, rather than checking more intricate noninterference properties for the whole 
 program. 
 
 
 To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully 
 automatic tool Joana for checking noninterference properties for Java programs and the theorem prover 
 KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung, 
 and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an 
 e-voting system. 
 The CVJ framework allows one to establish cryptographic indistinguishability properties for Java 
 programs by checking (standard) noninterference properties for such programs.},
keywords = {secure information flow, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@article{KuestersTruderungBeckertEA2015b,
title = {A Hybrid Approach for Proving Noninterference of Java Programs},
author = {Ralf K\"{u}sters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and Michael Kirsten and Martin Mohr},
url = {http://eprint.iacr.org/2015/438},
year  = {2015},
date = {2015-01-01},
journal = {IACR Cryptology ePrint Archive},
volume = {2015},
pages = {438},
abstract = {Several tools and approaches for proving noninterference properties for Java and other languages exist. 
 Some of them have a high degree of automation or are even fully automatic, but overapproximate 
 the actual information flow, and hence, may produce false positives. 
 Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence, 
 analysis is time-consuming. 
 
 
 In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches: 
 We want to use fully automatic analysis as much as possible and only at places in a program where, 
 due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive 
 analysis, where the latter involves only the verification of specific functional properties in certain 
 parts of the program, rather than checking more intricate noninterference properties for the whole 
 program. 
 
 
 To illustrate the hybrid approach, in a case study we use the hybrid approach---along with the fully 
 automatic tool Joana for checking noninterference properties for Java programs and the theorem prover 
 KeY for the verification of Java programs---and the CVJ framework proposed by K"usters, Truderung, 
 and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an 
 e-voting system. 
 The CVJ framework allows one to establish cryptographic indistinguishability properties for Java 
 programs by checking (standard) noninterference properties for such programs.},
keywords = {secure information flow, Verification},
pubstate = {published},
tppubtype = {article}
}
@inproceedings{SchmittUlbrich2015,
title = {Axiomatization of Typed First-Order Logic},
author = {Peter H. Schmitt and Mattias Ulbrich},
doi = {10.1007/978-3-319-19249-9_29},
year  = {2015},
date = {2015-01-01},
booktitle = {20th International Symposium on Formal Methods (FM 2015)},
volume = {9109},
pages = {470--486},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/setta/Wasser15,
title = {Generating Specifications for Recursive Methods by Abstracting Program  States},
author = {Nathan Wasser},
year  = {2015},
date = {2015-01-01},
booktitle = {SETTA},
volume = {9409},
pages = {243--257},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
keywords = {Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{hentschel.kasdorf.ea:interactive,
title = {An interactive verification tool meets an IDE},
author = {Martin Hentschel and Stefan K\"{a}sdorf and Reiner H\"{a}hnle and Richard Bubel},
editor = {Elvira Albert and Emil Sekerinski and Gianluigi Zavattaro},
year  = {2014},
date = {2014-09-01},
booktitle = {Proceedings of the 11th International Conference on Integrated Formal Methods},
pages = {55--70},
publisher = {Springer},
series = {LNCS},
abstract = {We present a general approach on how to integrate a semi-automatic verification tool into a state-of-the-art integrated development environment (IDE). The objective and challenge is to keep implementation, specification and proofs in sync. Following a change in one of the specifications or implementations, all proofs that could possibly be affected by that change are rescheduled. To improve performance we look at several optimizations. User feedback about proof results is provided within the IDE using standard markers and views. The approach has been implemented and realizes an integration of the interactive verification system KeY into the Eclipse IDE.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{hentschel.bubel.ea:symbolic,
title = {Symbolic Execution Debugger (SED)},
author = {Martin Hentschel and Richard Bubel and Reiner H\"{a}hnle},
editor = {Borzoo Bonakdarpour and Scott A. Smolka},
year  = {2014},
date = {2014-01-01},
booktitle = {Proceedings of Runtime Verification 2014},
pages = {255--262},
publisher = {Springer},
series = {LNCS},
abstract = {We present the Symbolic Execution Debugger for sequential Java programs. Based on symbolic execution, its functionality goes beyond that of traditional interactive debuggers. For instance, debugging can start directly at any method or statement and all possible program execution paths are explored simultaneously. To support program comprehension execution paths as well as intermediate states are visualized.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{	TUD-CS-2014-0930,
title = {Potential Synergies of Theorem Proving and Model Checking for Software Product Lines},
author = {Thomas Th\"{u}m and Jens Meinicke and Fabian Benduhn and Martin Hentschel and Alexander von Rhein and Gunter Saake},
year  = {2014},
date = {2014-01-01},
booktitle = {Proceedings of the International Software Product Line Conference (SPLC)},
publisher = {ACM},
address = {New York, NY, USA},
series = {SPLC},
abstract = {The verification of software product lines is an active research area. A challenge is to efficiently verify similar products without the need to generate and verify them individually. As solution, researchers suggest family-based verification approaches, which either transform compile-time into runtime variability or make verification tools variabilityaware. Existing approaches either focus on theorem proving, model checking, or other verification techniques. For the first time, we combine theorem proving and model checking to evaluate their synergies for product-line verification. We provide tool support by connecting five existing tools, namely FeatureIDE and FeatureHouse for product-line development, as well as KeY, JPF, and OpenJML for verification of Java programs. In an experiment, we found the synergy of improved effectiveness and efficiency, especially for product lines with few defects. Further, we experienced that model checking and theorem proving are more efficient and effective if the product line contains more defects.},
keywords = {Design by Contract, family-based verification, feature-based specification, feature-oriented contracts, model checking, Software product lines, theorem proving, variability encoding},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{AhrendtBeckertBrunsEtAl14,
title = {The KeY Platform for Verification and Analysis of Java Programs},
author = {Wolfgang Ahrendt and Bernhard Beckert and Daniel Bruns and Richard Bubel and 
Christoph Gladisch and Sarah Grebing and Reiner H\"{a}hnle and Martin Hentschel and 
Mihai Herda and Vladimir Klebanov and Wojciech Mostowski and Christoph Scheben and 
Peter H. Schmitt and Mattias Ulbrich},
editor = {Dimitra Giannakopoulou and Daniel Kroening},
url = {http://link.springer.com/chapter/10.1007/978-3-319-12154-3_4},
doi = {10.1007/978-3-319-12154-3_4},
isbn = {978-3-642-54107-0},
year  = {2014},
date = {2014-01-01},
booktitle = {Verified Software: Theories, Tools, and Experiments (VSTTE 2014)},
number = {8471},
pages = {1--17},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
abstract = {The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.},
keywords = {Debugging, secure information flow, Symbolic Execution, Test Case Generation, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{	TUD-CS-2014-0831,
title = {Visualizing Unbounded Symbolic Execution},
author = {Martin Hentschel and Reiner H\"{a}hnle and Richard Bubel},
editor = {Martina Seidl and Nikolai Tillmann},
year  = {2014},
date = {2014-01-01},
booktitle = {Proceedings of Testing and Proofs (TAP) 2014},
pages = {82--98},
publisher = {Springer},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{nfm2014JKelloy,
title = {JKelloy: A Proof Assistant for Relational Specifications of Java Programs},
author = {Aboubakr Achraf El Ghazi and Mattias Ulbrich and Christoph Gladisch and Shmuel Tyszberowicz and Mana Taghdiri},
url = {http://dx.doi.org/10.1007/978-3-319-06200-6_13},
doi = {10.1007/978-3-319-06200-6_13},
year  = {2014},
date = {2014-01-01},
booktitle = {NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings},
pages = {173--187},
crossref = {DBLP:conf/nfm/2014},
keywords = {Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@techreport{Bruns14,
title = {Formal Verification of an Electronic Voting System},
author = {Daniel Bruns},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000042284},
issn = {2190-4782},
year  = {2014},
date = {2014-01-01},
number = {2014,11},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {Electronic voting (e-voting) systems that are used in public elections need to fulfil a broad range of strong requirements concerning both safety and security. Among these requirements are reliability, robustness, privacy of votes, coercion resistance and universal verifiability. Bugs in or manipulations of an e-voting system may have considerable influence on the life of the humans living in a country where such a system is used. Hence, e-voting systems are an obvious target for software verification. In this paper, we report on an implementation of such a system in Java and the formal verification of functional properties thereof in the KeY verification system. Even though the actual components are clearly modularized, the challenge lies in the fact that we need to prove a highly nonlocal property: After all voters have cast their votes, the server calculates the correct votes for each candidate w.r.t. the original ballots. This kind of trace property is difficult to prove with static techniques like verification and typically yields a large specification overhead.},
keywords = {secure information flow},
pubstate = {published},
tppubtype = {techreport}
}
@techreport{Bruns14a,
title = {Towards Specification and Verification of Information Flow in Concurrent Java-like Programs},
author = {Daniel Bruns},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000039446},
issn = {2190-4782},
year  = {2014},
date = {2014-01-01},
number = {2014,5},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {Today, nearly all personal computer systems are multiprocessor systems, allowing multiple programs to be executed in parallel while accessing a shared memory. At the same time, computers are increasingly handling more and more data. Ensuring that no confidential data is leaked to untrusted sinks remains a major quest in software engineering. Formal verification, based on theorem proving, is a powerful technique to prove both functional correctness and security properties such as absence of information flow. Present verification systems are sound and complete, but often lack efficiency and are only applicable to sequential programs. Concurrent programs are notorious for all possible environment actions have to be taken into account. In this paper, we point out steps towards a formal verification methodology for information flow in concurrent programs. We consider passive attackers who are able to observe public parts of the memory at any time during execution and to compare program traces between different executions. Our approach consists of two main elements: (i) formalizing properties on whether two executions are indistinguishable to such an attacker in a decidable logic, and (ii) defining a technique to reason about executions of concurrent programs by regarding a single thread in isolation. The latter is based on the rely/guarantee approach.},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
@inproceedings{kusters.truderung.ea:hybrid,
title = {A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java Programs},
author = {Ralf K\"{u}sters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and J\"{u}rgen Graf and Christoph Scheben},
editor = {Christian Hammer and Sjouke Mauw},
url = {http://grsrd.uni.lu/papers/grsrd2013_submission_2.pdf},
year  = {2013},
date = {2013-01-01},
booktitle = {Grande Region Security and Reliability Day 2013},
address = {Luxembourg},
note = {Extended Abstract},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@techreport{BeckertBrunsKlebanovEtAl13,
title = {Information Flow in Object-Oriented Software - Extended Version},
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov and Christoph Scheben and Peter H. Schmitt and Mattias Ulbrich},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000037606},
issn = {2190-4782},
year  = {2013},
date = {2013-01-01},
number = {2013,14},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
@techreport{BeckertBrunsKlebanovEtAl13a,
title = {Secure Information Flow for Java - A Dynamic Logic Approach},
author = {Bernhard Beckert and Daniel Bruns and Vladimir Klebanov and Christoph Scheben and Peter H. Schmitt and Mattias Ulbrich},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000036786},
issn = {2190-4782},
year  = {2013},
date = {2013-01-01},
number = {2013,10},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
keywords = {},
pubstate = {published},
tppubtype = {techreport}
}
@inproceedings{BeckertBruns13,
title = {Dynamic Logic with Trace Semantics},
author = {Bernhard Beckert and Daniel Bruns},
editor = {Maria Paola Bonacina},
url = {http://link.springer.com/chapter/10.1007/978-3-642-38574-2_22},
doi = {10.1007/978-3-642-38574-2_22},
isbn = {978-3-642-38573-5},
year  = {2013},
date = {2013-01-01},
booktitle = {24th International Conference on Automated Deduction (CADE-24)},
volume = {7898},
pages = {315--329},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
abstract = {Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic~(DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for proving functional and information-flow properties in concurrent programs, among other applications.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{gladischTyszberowicz2013,
title = {Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking},
author = {Christoph Gladisch and Shmuel Tyszberowicz},
editor = {Leonardo de Moura and Juliano Iyoda},
year  = {2013},
date = {2013-01-01},
booktitle = {Brazilian Symposium on Formal Methods (SBMF)},
volume = {8195},
publisher = {Springer},
series = {LNCS},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@mastersthesis{KirstenStA2013,
title = {Proving Well-Definedness of JML Specifications with KeY},
author = {Michael Kirsten},
year  = {2013},
date = {2013-01-01},
school = {ITI Schmitt, Karlsruhe Institute of Technology},
abstract = {Specification methods in formal program verification enable the enhancement of source 
 code with formal annotations as to formally specify the behaviour of a program. This is 
 a popular way in order to subsequently prove software to be reliable and meet certain 
 requirements, which is crucial for many applications and gains even more importance in 
 modern society. The annotations can be taken as a contract, which then can be verified 
 guaranteeing the specified program element \textendash as a receiver \textendash to fulfil this contract with 
 its caller. However, these functional contracts can be problematic for partial functions, 
 e.g. a division, as certain cases may be undefined, as in this example a division by zero. 
 Modern programming languages such as Java handle undefined behaviour by casting an exception. 
 
 
 There are several approaches to handle a potential undefinedness of specifications. In 
 this thesis, we chose one which automatically generates formal proof obligations ensuring 
 that undefined specification expressions will not be evaluated. 
 
 
 Within this work, we elaborate on so-called Well-Definedness Checks dealing with undefinedness 
 occurring in specifications of the modelling language JML/JML* in the 
 KeY System, which is a formal software development tool providing mechanisms to 
 deductively prove the before mentioned contracts. Advantages and delimitations are 
 discussed and, furthermore, precise definitions as well as a fully functional implementation 
 within KeY are given. Our work covers the major part of the specification elements 
 currently supported by KeY, on the higher level including class invariants, model fields, 
 method contracts, loop statements and block contracts. The process of checking the 
 well-definedness of a specification forms a preliminary step before the actual proof and 
 rejects undefined specifications. We further contribute by giving a choice between two 
 different semantics, both bearing different advantages and disadvantages. The thesis also 
 includes an extensive case study analysing many examples and measuring the performance 
 of the implemented Well-Definedness Checks.},
type = {Studienarbeit},
keywords = {Verification},
pubstate = {published},
tppubtype = {mastersthesis}
}
@inproceedings{ulbrich-geilmann-elghazi-taghdiri-tacas2012,
title = {A Proof Assistant for Alloy Specifications},
author = {Mattias Ulbrich and Ulrich Geilmann and Aboubakr Achraf El Ghazi and Mana Taghdiri},
year  = {2012},
date = {2012-03-01},
booktitle = {18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
pages = {422-436},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{BeckertBruns12,
title = {Formal Semantics of Model Fields in Annotation-based Specifications},
author = {Bernhard Beckert and Daniel Bruns},
editor = {Birte Glimm and Antonio Kr\"{u}ger},
url = {http://link.springer.com/chapter/10.1007/978-3-642-33347-7_2},
isbn = {978-3-642-33346-0},
year  = {2012},
date = {2012-01-01},
booktitle = {KI 2012: Advances in Artificial Intelligence},
volume = {7526},
pages = {13--24},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
abstract = {It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional. In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert's $varepsilon$~terms.},
keywords = {Modular Specification, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@techreport{BeckertBruns12a,
title = {Dynamic Trace Logic: Definition and Proofs},
author = {Bernhard Beckert and Daniel Bruns},
url = {http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf, 
http://digbib.ubka.uni-karlsruhe.de/volltexte/1000028184},
issn = {2190-4782},
year  = {2012},
date = {2012-01-01},
number = {2012,10},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic~(DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for functional verification of concurrent programs and for proving information-flow properties among other applications.},
note = {A revised version replacing an unsound rule is available at 
http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf},
keywords = {Verification},
pubstate = {published},
tppubtype = {techreport}
}
@article{Bruns12,
title = {Eine formale Semantik f\"{u}r die Java Modeling Language},
author = {Daniel Bruns},
url = {http://www.springerlink.com/content/b503j663353x482w/},
doi = {10.1007/s00287-011-0532-0},
year  = {2012},
date = {2012-01-01},
journal = {Informatik-Spektrum},
volume = {35},
number = {1},
pages = {45--49},
publisher = {Springer-Verlag},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
@techreport{BeckertBrunsKuestersEtAl12,
title = {The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study},
author = {Bernhard Beckert and Daniel Bruns and Ralf K\"{u}sters and Christoph Scheben and Peter H. Schmitt and Tomasz Truderung},
url = {http://digbib.ubka.uni-karlsruhe.de/volltexte/1000027497},
year  = {2012},
date = {2012-01-01},
number = {2012,8},
institution = {Department of Informatics, Karlsruhe Institute of Technology},
series = {Karlsruhe Reports in Informatics},
abstract = {In this paper, we report on an ongoing case study in which we use the KeY tool, a theorem prover for checking functional correctness and noninterference properties of Java programs, to establish computational indistinguishability for a simple Java program that involves clients sending encrypted messages over an untrusted network to a server. The analysis uses a general framework, recently proposed by K"usters et al., which enables program analysis tools, such as KeY, that can check (standard) noninterference properties for Java programs to establish computational indistinguishability properties.},
keywords = {secure information flow},
pubstate = {published},
tppubtype = {techreport}
}
@article{springerlink:10.1007/s10009-012-0227-0,
title = {Model generation for quantified formulas with application to test data generation},
author = {Christoph Gladisch},
url = {http://dx.doi.org/10.1007/s10009-012-0227-0},
issn = {1433-2779},
year  = {2012},
date = {2012-01-01},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
pages = {1-21},
publisher = {Springer Berlin / Heidelberg},
note = {10.1007/s10009-012-0227-0},
keywords = {Test Case Generation},
pubstate = {published},
tppubtype = {article}
}
@inproceedings{	TUD-CS-2012-0355,
title = {Family-Based Deductive Verification of Software Product Lines},
author = {Thomas Th\"{u}m and Ina Schaefer and Sven Apel and Martin Hentschel},
isbn = {978-1-4503-1129-8},
year  = {2012},
date = {2012-01-01},
booktitle = {Proceedings of the 11th International Conference on Generative Programming and Component Engineering},
pages = {11-20},
publisher = {ACM},
address = {Dresden, Germany},
series = {GPCE '12},
abstract = {A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used of-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85 %.},
keywords = {deductive verification, product-line analysis, program families, Software product lines, theorem proving},
pubstate = {published},
tppubtype = {inproceedings}
}
@techreport{ulbrich-geilmann-elghazi-taghdiri-techrep2011,
title = {On Proving Alloy Specifications using KeY},
author = {Mattias Ulbrich and Ulrich Geilmann and Aboubakr Achraf El Ghazi and Mana Taghdiri},
year  = {2011},
date = {2011-01-01},
number = {2011-37},
institution = {Karlsruhe Institute of Technology},
keywords = {Verification},
pubstate = {published},
tppubtype = {techreport}
}
@article{Beckert2011,
title = {KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit Testing},
author = { Bernhard Beckert and Christoph Gladisch and Shmuel Tyszberowicz and Amiram Yehudai},
url = {http://dx.doi.org/10.1007/s13198-011-0068-3},
doi = {10.1007/s13198-011-0068-3},
issn = {0976-4348},
year  = {2011},
date = {2011-01-01},
journal = {International Journal of System Assurance Engineering and Management},
volume = {2},
number = {2},
pages = {97--113},
abstract = {Unit testing plays a major role in the software development process. Two essential criteria to achieve effective unit testing are: (1) testing each unit in isolation from other parts of the program and (2) achieving high code coverage. The former requires a lot of extra work such as writing drivers and stubs, whereas the latter is difficult to achieve when manually writing the tests. When changing existing code it is advocated to run the unit tests to avoid regression bugs. However, in many cases legacy software has no unit tests. Writing those tests from scratch is a hard and tedious process, which might not be cost-effective. This paper presents a tool chain approach that combines verification-based testing (VBT) and capture and replay (CaR) test generation methods. We have built a concrete tool chain, KeYGenU, which consists of two existing tools---KeY and GenUTest. The KeY system is a deductive verification and test-generation tool. GenUTest automatically generates JUnit tests for a correctly working software. This combination provides isolated unit test suites with high code-coverage. The generated tests can also be used for regression testing.},
keywords = {Test Case Generation},
pubstate = {published},
tppubtype = {article}
}
@inproceedings{SchmittEtAl2011,
title = {Dynamic Frames in Java Dynamic Logic},
author = {Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei\ss
},
editor = {Bernhard Beckert and Claude March\'{e}
},
year  = {2011},
date = {2011-01-01},
booktitle = {Revised Selected Papers, International Conference on Formal 
 Verification of Object-Oriented Software (FoVeOOS 2010)},
volume = {6528},
pages = {138--152},
publisher = {Springer},
series = {LNCS},
keywords = {Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DBLP:conf/pts/Gladisch10,
title = {Test Data Generation for Programs with Quantified First-Order 
 Logic Specifications},
author = {Christoph Gladisch},
year  = {2010},
date = {2010-01-01},
booktitle = {ICTSS},
pages = {158-173},
keywords = {Test Case Generation},
pubstate = {published},
tppubtype = {inproceedings}
}
@inbook{Gladisch2010,
title = {Generating Regression Unit Tests Using a Combination of Verification and Capture \& Replay},
author = {Christoph Gladisch and Shmuel Tyszberowicz and Bernhard Beckert and Amiram Yehudai},
editor = {Fraser, Gordon and Gargantini, Angelo},
url = {http://dx.doi.org/10.1007/978-3-642-13977-2_7},
doi = {10.1007/978-3-642-13977-2_7},
isbn = {978-3-642-13977-2},
year  = {2010},
date = {2010-01-01},
booktitle = {Tests and Proofs: 4th International Conference, TAP 2010, M'alaga, Spain, July 1-2, 2010. Proceedings},
pages = {61--76},
publisher = {Springer Berlin Heidelberg},
address = {Berlin, Heidelberg},
keywords = {Test Case Generation},
pubstate = {published},
tppubtype = {inbook}
}
@inproceedings{gladischSEFM2008,
title = {Verification-based Testing for Full Feasible Branch Coverage},
author = {Christoph Gladisch},
editor = {Antonio Cerone},
isbn = {978-0-7695-3437-4},
year  = {2008},
date = {2008-00-00},
booktitle = {Proc. 6th IEEE Int. Conf. Software Engineering and Formal Methods (SEFM'08)},
publisher = {IEEE Computer Society Press},
keywords = {Test Case Generation},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{Beckert:2007:WTC:1776119.1776131,
title = {White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing},
author = {Bernhard Beckert and Christoph Gladisch},
url = {http://dl.acm.org/citation.cfm?id=1776119.1776131},
isbn = {3-540-73769-3, 978-3-540-73769-8},
year  = {2007},
date = {2007-01-01},
booktitle = {Proceedings of the 1st International Conference on Tests and Proofs},
pages = {207--216},
publisher = {Springer-Verlag},
address = {Zurich, Switzerland},
series = {TAP'07},
keywords = {Test Case Generation},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{engelHaehnle07,
title = {Generating Unit Tests from Formal Proofs},
author = {Christian Engel and Reiner H\"{a}hnle},
editor = {Yuri Gurevich and Bertrand Meyer},
year  = {2007},
date = {2007-01-01},
booktitle = {Proceedings, 1st International Conference on Tests And Proofs (TAP), Zurich, Switzerland},
volume = {4454},
publisher = {Springer},
series = {LNCS},
keywords = {Test Case Generation},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DHS05,
title = {A Theorem Proving Approach to Analysis of Secure Information  Flow},
author = {\'{A}d\'{a}m Darvas and Reiner H\"{a}hnle and Dave Sands},
editor = {Dieter Hutter and Markus Ullmann},
url = {http://www.springerlink.com/link.asp?id=rdqa8ejctda3yw64},
year  = {2005},
date = {2005-01-01},
booktitle = {Proc. 2nd International Conference on Security in Pervasive Computing},
volume = {3450},
pages = {193--209},
publisher = {Springer-Verlag},
series = {LNCS},
keywords = {secure information flow, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}
@inproceedings{DHS03,
title = {A Theorem Proving Approach to Analysis of Secure Information  Flow},
author = {\'{A}d\'{a}m Darvas and Reiner H\"{a}hnle and Dave 
Sands},
editor = {Roberto Gorrieri},
year  = {2003},
date = {2003-01-01},
booktitle = {Workshop on Issues in the Theory of Security, WITS},
organization = {IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS},
keywords = {secure information flow, Verification},
pubstate = {published},
tppubtype = {inproceedings}
}