[GG15]	Daniel Grahl and Simon Greiner. Non-interference with what-declassification in component-based systems. Technical Report 2015,10, Department of Informatics, Karlsruhe Institute of Technology, November 2015. [ bib | license | urn | http | Abstract ]
[BMU15]	Daniel Bruns, Wojciech Mostowski, and Mattias Ulbrich. Implementation-level verification of algorithms with KeY. Software Tools for Technology Transfer, 17(6):729–744, November 2015. [ bib | DOI | http | Abstract ]
[Gra15]	Daniel Grahl. Deductive Verification of Concurrent Programs and its Application to Secure Information Flow for Java. PhD thesis, Karlsruhe Institute of Technology, 29 October 2015. [ bib | DOI | license | urn | http | Abstract ]
[Bru15b]	Daniel Bruns. A theorem proving approach to secure information flow in concurrent programs (extended abstract). In Deepak Garg and Boris Köpf, editors, Workshop on Foundations of Computer Security (FCS 2015), July 2015. [ bib | .pdf ]
[BDG+15]	Daniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel, and Richard Gay. Poster: Security in e-voting. In Sophie Engle, editor, 36th IEEE Symposium on Security and Privacy, Poster Session, 18 May 2015. [ bib ]
[Bru15a]	Daniel Bruns. Deductive verification of concurrent programs. Technical Report 2015,3, Department of Informatics, Karlsruhe Institute of Technology, February 2015. [ bib | license | urn | http | Abstract ]
[KTB+15]	Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr. A hybrid approach for proving noninterference of Java programs. In Cédric Fournet, Michael Hicks, and Luca Viganò, editors, 28th IEEE Computer Security Foundations Symposium (CSF), pages 305–319, 2015. [ bib | DOI | http | Abstract ]
[Bru14a]	Daniel Bruns. Formal verification of an electronic voting system. Technical Report 2014,11, Department of Informatics, Karlsruhe Institute of Technology, August 2014. [ bib | license | urn | http | Abstract ]
[Bru14b]	Daniel Bruns. Towards specification and verification of information flow in concurrent Java-like programs. Technical Report 2014,5, Department of Informatics, Karlsruhe Institute of Technology, March 2014. [ bib | license | urn | http | Abstract ]
[BBK+14]	Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. Information flow in object-oriented software. In Gopal Gupta and Ricardo Peña, editors, Logic-Based Program Synthesis and Transformation, LOPSTR 2013, number 8901 in Lecture Notes in Computer Science, pages 19–37. Springer, 2014. [ bib | DOI | Abstract ]
[HABH14]	Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. Formal specification with JML. Technical Report 2014,10, Department of Informatics, Karlsruhe Institute of Technology, 2014. [ bib | license | urn | http | Abstract ]
[ABB+14]	Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. The KeY platform for verification and analysis of Java programs. In Dimitra Giannakopoulou and Daniel Kroening, editors, Verified Software: Theories, Tools, and Experiments (VSTTE 2014), number 8471 in Lecture Notes in Computer Science, pages 1–17. Springer-Verlag, 2014. [ bib | DOI | http | Abstract ]
[BBK+13a]	Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. Information flow in object-oriented software – extended version –. Technical Report 2013,14, Department of Informatics, Karlsruhe Institute of Technology, 2013. [ bib | license | urn | http ]
[BBK+13b]	Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. Secure information flow for Java – a dynamic logic approach. Technical Report 2013,10, Department of Informatics, Karlsruhe Institute of Technology, 2013. [ bib | license | http ]
[BB13]	Bernhard Beckert and Daniel Bruns. Dynamic logic with trace semantics. In Maria Paola Bonacina, editor, 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Computer Science, pages 315–329. Springer-Verlag, 2013. [ bib | DOI | http | Abstract ]
[KTB+13]	Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Jürgen Graf, and Christoph Scheben. A hybrid approach for proving noninterference and applications to the cryptographic verification of Java programs. In Christian Hammer and Sjouke Mauw, editors, Grande Region Security and Reliability Day 2013, Luxembourg, 2013. Extended Abstract. [ bib | .pdf ]
[BBG12]	Bernhard Beckert, Daniel Bruns, and Sarah Grebing. Mind the gap: Formal verification and the Common Criteria. In Markus Aderhold, Serge Autexier, and Heiko Mantel, editors, 6th International Verification Workshop, VERIFY-2010, volume 3 of EPiC Series, pages 4–12. EasyChair, 2012. [ bib | http | Abstract ]
[BB12b]	Bernhard Beckert and Daniel Bruns. Formal semantics of model fields in annotation-based specifications. In Birte Glimm and Antonio Krüger, editors, KI 2012: Advances in Artificial Intelligence, volume 7526 of Lecture Notes in Computer Science, pages 13–24. Springer-Verlag, 2012. [ bib | http | Abstract ]
[BB12a]	Bernhard Beckert and Daniel Bruns. Dynamic trace logic: Definition and proofs. Technical Report 2012,10, Department of Informatics, Karlsruhe Institute of Technology, 2012. A revised version replacing an unsound rule is available at https://formal.kastel.kit.edu/~grahl/papers/trace-tr.pdf. [ bib | license | urn | http | Abstract ]
[Bru12]	Daniel Bruns. Eine formale Semantik für die Java Modeling Language. Informatik-Spektrum, 35(1):45–49, 2012. [ bib | DOI | http ]
[BBK+12]	Bernhard Beckert, Daniel Bruns, Ralf Küsters, Christoph Scheben, Peter H. Schmitt, and Tomasz Truderung. The KeY approach for the cryptographic verification of Java programs: A case study. Technical Report 2012,8, Department of Informatics, Karlsruhe Institute of Technology, 2012. [ bib | license | urn | http | Abstract ]
[Bru11]	Daniel Bruns. Specification of red-black trees: Showcasing dynamic frames, model fields and sequences. In Wolfgang Ahrendt and Richard Bubel, editors, 10th KeY Symposium, Nijmegen, the Netherlands, 26–27 August 2011. Extended Abstract. [ bib | urn | http | Abstract ]
[BB11]	Bernhard Beckert and Daniel Bruns. Formal semantics of model fields inspired by a generalization of Hilbert's ε terms. In Wolfgang Ahrendt and Richard Bubel, editors, 10th KeY Symposium, Nijmegen, the Netherlands, 26–27 August 2011. Extended Abstract. [ bib | urn | http | Abstract ]
[BKS11]	Daniel Bruns, Vladimir Klebanov, and Ina Schaefer. Verification of software product lines with delta-oriented slicing. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software (FoVeOOS 2010), volume 6528 of Lecture Notes in Computer Science, pages 61–75. Springer-Verlag, 2011. [ bib | DOI | http | Abstract ]
[BKS10]	Daniel Bruns, Vladimir Klebanov, and Ina Schaefer. Verification of software product lines: Reducing the effort with delta-oriented slicing and proof reuse. In Bernhard Beckert and Claude Marché, editors, Papers Presented at the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), number 2010,13 in Karlsruhe Reports in Informatics, pages 345–358, Paris, France, 28–30 June 2010. Technical Report, Department of Informatics, Karlsruhe Institute of Technology, 2010-13. [ bib | urn | http | Abstract ]
[Bru10]	Daniel Bruns. Formal semantics for the Java Modeling Language. In Informatiktage 2010, volume S-9 of Lecture Notes in Informatics, pages 15–18, Bonn, Germany, 19–20 March 2010. Gesellschaft für Informatik. Best Paper Award. [ bib | .pdf | Abstract ]
[Bru09]	Daniel Bruns. Formal semantics for the Java Modeling Language. Diplomarbeit, Universität Karlsruhe, June 2009. [ bib | license | urn | http | Abstract ]
[Bru08]	Daniel Bruns. Elektronische Wahlen: Theoretisch möglich, praktisch undemokratisch. FIfF-Kommunikation, 25(3):33–35, September 2008. [ bib ]
[Bru07]	Daniel Bruns. A fixpoint-based rule for loop verification. Studienarbeit, Universität Karlsruhe, June 2007. [ bib ]