Publications
Refereed Publications
Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, and Marko Kleine Büning. Combining Graph-Based and Deduction-Based Information-Flow Analysis. In 5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017) affiliated with ETAPS 2017: European Joint Conferences on Theory and Practice of Software, April 2017. [ bib | .pdf ]
Felix Dörre and Vladimir Klebanov. Practical Detection of Entropy Loss in Pseudo-Random Number Generators. In Proceedings, ACM Conference on Computer and Communications Security (CCS), 2016. [ bib ]
Vladimir Klebanov, Alexander Weigl, and Jörg Weisbarth. Sound Probabilistic #SAT with Projection. In Proceedings, Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL), 2016. [ bib ]
Alexander Weigl. Efficient SAT-based Pre-image Enumeration for Quantitative Information Flow in Programs. In 5th International Workshop on Quantitative Aspects of Security Assurance (QASA 2016), 2016. [ bib ]
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 ]
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, May 18 2015. [ bib ]
Felix Dörre and Vladimir Klebanov. Pseudo-Random Number Generator Verification: A Case Study. In Arie Gurfinkel and Sanjit A. Seshia, editors, Proceedings, Verified Software: Theories, Tools, and Experiments (VSTTE), Lecture Notes in Computer Science. Springer, 2015. [ bib ]
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 and Michael Hicks, editors, 28th IEEE Computer Security Foundations Symposium, 2015. [ bib ]
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 ]
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 ]
Christoph Scheben and Peter H. Schmitt. Efficient Self-Composition for Weakest Precondition Calculi. In Cliff Jones, Pekka Pihlajasaari, and Jun Sun, editors, Proceedings, 19th International Symposium on Formal Methods (FM), volume 8442 of LNCS, pages 579-594. Springer International Publishing, 2014. [ bib | DOI ]
Vladimir Klebanov. Precise Quantitative Information Flow Analysis - A Symbolic Approach. Theoretical Computer Science, 538(0):124-139, 2014. [ bib | DOI ]
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 ]
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 ]
Vladimir Klebanov, Norbert Manthey, and Christian Muise. SAT-based Analysis and Quantification of Information Flow in Programs. In Proceedings, International Conference on Quantitative Evaluation of Systems (QEST), volume 8054 of LNCS, pages 156-171. Springer, 2013. [ bib | DOI | .pdf ]
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, Edinburgh, United Kingdom, 2012. EasyChair. Discussion paper. [ bib | http ]
Christoph Scheben and Peter H. Schmitt. Verification of Information Flow Properties of Java Programs without Approximations. In Formal Verification of Object-Oriented Software, volume 7421 of LNCS, pages 232-249. Springer, 2012. [ bib ]
Vladimir Klebanov. Precise Quantitative Information Flow Analysis Using Symbolic Model Counting. In Fabio Martinelli and Flemming Nielson, editors, Proceedings, International Workshop on Quantitative Aspects in Security Assurance (QASA), 2012. [ bib | .pdf ]
Non-Refereed Publications
Felix Dörre and Vladimir Klebanov. Entropy Loss and Output Predictability in the Libgcrypt PRNG (CVE-2016-6313), 2016. [ bib | .pdf ]
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 | http ]
Daniel Bruns. Deductive Verification of Concurrent Programs. Technical Report 2015-3, Department of Informatics, Karlsruhe Institute of Technology, 2015. [ bib | http ]
Christoph Scheben. Program-level Specification and Deductive Verification of Security Properties. PhD thesis, Karlsruhe Institute of Technology, 2014. [ bib | http ]
Pavel Nikolov. Combining theorem proving and type systems for precise and efficient information flow verification. Studienarbeit, Karlsruhe Institute of Technology, 2014. [ bib ]
Kai Wallisch. Maps in Java Dynamic Logic. Studienarbeit, Karlsruhe Institute of Technology, 2014. [ bib ]
Daniel Bruns. Formal Verification of an Electronic Voting System. Technical Report 2014-11, Department of Informatics, Karlsruhe Institute of Technology, 2014. [ bib | http ]
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, 2014. [ bib | http ]
Andreas Wagner. Trace Based Reasoning with KeY and JML. Studienarbeit, Karlsruhe Institute of Technology, 2013. [ bib | .pdf ]
Fabian Ruch. Efficient Logic-Based Information Flow Analysis Of Object-Oriented Programs. Bachelor thesis, Karlsruhe Institute of Technology, 2013. [ bib | http ]
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 | http ]
Bernhard Beckert and Daniel Bruns. Dynamic Trace Logic: Definition and Proofs. Technical Report 2012-10, Department of Informatics, Karlsruhe Institute of Technology, 2012. [ bib | http ]
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 | http ]
This file was generated by bibtex2html 1.97.