Publications

[1]	Eyad Alkassar, Mark A. Hillebrand, Wolfgang Paul, and Elena Petrova. Automated verification of a small hypervisor. In Peter O'Hearn, Gary T. Leavens, and Sriram Rajamani, editors, Verified Software: Theories, Tools, Experiments (VSTTE 2010), Lecture Notes in Computer Science, Edinburgh, UK, 2010. Springer. To appear. [ bib \| sources (.tar.gz) ]
[2]	Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer. Better avionics software reliability by code verification - A glance at code verification methodology in the Verisoft XT project. In Embedded World 2009 Conference, Nuremberg, Germany, March 2009. Franzis Verlag. To appear. [ bib \| .pdf ]
[3]	Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer. Formal verification of a microkernel used in dependable software systems. In Bettina Buth, Gerd Rabe, and Till Seyfarth, editors, Computer Safety, Reliability, and Security (SAFECOMP 2009), volume 5775 of Lecture Notes in Computer Science, pages 187-200, Hamburg, Germany, 2009. Springer. [ bib \| http \| .pdf ]
[4]	Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer. Ingredients of operating system correctness. In Embedded World 2010 Conference, Nuremberg, Germany, March 2010. To appear. [ bib \| .pdf ]
[5]	Christoph Baumann and Thorsten Bormer. Verifying the PikeOS microkernel: First results in the Verisoft XT Avionics project. In Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, Doctoral Symposium on Systems Software Verification (DS SSV 2009), number AIB-2009-14 in Aachener Informatik Berichte, pages 20-22. Department of Computer Science, RWTH Aachen, June 2009. [ bib \| .pdf ]
[6]	Bernhard Beckert and Michal Moskal. Deductive verification of system software in the Verisoft XT project. KI, 2010. To appear. [ bib \| http ]
[7]	Stefan Berghofer, Lukas Bulwahn, and Florian Haftmann. Turning inductive into equational specifications. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Markus Wenzel, editors, Theorem Proving in Higher Order Logics (TPHOLs 2009), volume 5674 of Lecture Notes in Computer Science, pages 131-146, Munich, Germany, 2009. Springer. [ bib \| http ]
[8]	Stefan Berghofer and Markus Reiter. Formalizing the logic-automaton connection. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Markus Wenzel, editors, Theorem Proving in Higher Order Logics (TPHOLs 2009), volume 5674 of Lecture Notes in Computer Science, pages 147-163, Munich, Germany, 2009. Springer. [ bib \| http ]
[9]	Stefan Berghofer and Makarius Wenzel. Logic-free reasoning in Isabelle/Isar. In Mathematical Knowledge Management (MKM 2008), volume 5144 of Lecture Notes in Computer Science, pages 355-369, Birmingham, UK, July 2008. Springer. [ bib \| http \| .pdf ]
[10]	Sven Beyer. Advanced CPU verification using automatic detection of verification and specification gaps. In Magdy S. Abadir, Jayanta Bhadra, and Li-C. Wang, editors, Workshop on Microprocessor Test and Verification (MTV 2009), Austin, Texas, USA, December 2009. IEEE. [ bib ]
[11]	Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Matt Kaufmann, Lawrence Paulson, and Michael Norrish, editors, Interactive Theorem Proving (ITP 2010), Lecture Notes in Computer Science, Edinburgh, UK, 2010. Springer. To appear. [ bib ]
[12]	Sascha Böhme. Proof reconstruction for Z3 in Isabelle/HOL. In Workshop on Satisfiability Modulo Theories (SMT 2009), 2009. [ bib \| http \| .pdf ]
[13]	Sascha Böhme, Rustan Leino, and Burkhart Wolff. HOL-Boogie - An interactive prover for the Boogie program verifier. In Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of Lecture Notes in Computer Science, pages 150-166, Montréal, Québec, Canada, 2008. Springer. [ bib \| http \| .pdf ]
[14]	Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff. HOL-Boogie: An interactive prover-backend for the Verifiying C Compiler. Journal of Automated Reasoning, 44(1-2):111-144, 2010. [ bib \| http ]
[15]	Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement day. In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning (IJCAR 2010), Lecture Notes in Computer Science, Edinburgh, UK, 2010. Springer. To appear. [ bib ]
[16]	Sascha Böhme and Tjark Weber. Fast LCF-style proof reconstruction for Z3. In Matt Kaufmann, Lawrence Paulson, and Michael Norrish, editors, Interactive Theorem Proving (ITP 2010), Lecture Notes in Computer Science, Edinburgh, UK, 2010. Springer. To appear. [ bib ]
[17]	Jörg Bormann. Vollständige Formale Verifikation. PhD thesis, Universität Kaiserslautern, June 2009. [ bib \| http \| .pdf ]
[18]	Ernie Cohen, Eyad Alkassar, Vladimir Boyarinov, Markus Dahlweid, Ulan Degenbaev, Mark Hillebrand, Bruno Langenstein, Dirk Leinenbach, Michal Moskal, Steven Obua, Wolfgang Paul, Hristo Pentchev, Elena Petrova, Thomas Santen, Norbert Schirmer, Sabine Schmaltz, Wolfram Schulte, Andrey Shadrin, Stephan Tobies, Alexandra Tsyban, and Sergey Tverdyshev. Invariants, modularity, and rights. In Amir Pnueli, Irina Virbitskaite, and Andrei Voronkov, editors, Perspectives of Systems Informatics (PSI 2009), volume 5947 of Lecture Notes in Computer Science, pages 43-55, Novosibirsk, Russia, 2009. Springer. Invited paper. [ bib \| http ]
[19]	Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. VCC: A practical system for verifying concurrent C. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Markus Wenzel, editors, Theorem Proving in Higher Order Logics (TPHOLs 2009), volume 5674 of Lecture Notes in Computer Science, pages 23-42, Munich, Germany, 2009. Springer. Invited paper. [ bib \| http ]
[20]	Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies. A practical verification methodology for concurrent programs. Technical Report MSR-TR-2009-15, Microsoft Research, February 2009. [ bib \| http ]
[21]	Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies. A precise yet efficient memory model for C. In Workshop on Systems Software Verification (SSV 2009), volume 254 of Electronic Notes in Theoretical Computer Science, pages 85-103. Elsevier Science B.V., 2009. [ bib \| http ]
[22]	Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies. Local verification of global invariants in concurrent programs. In Byron Cook, Paul Jackson, and Tayssir Touili, editors, Computer Aided Verification (CAV 2010), Lecture Notes in Computer Science, Edinburgh, UK, July 2010. Springer. To appear. [ bib ]
[23]	Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies. Local verification of global invariants in concurrent programs. Technical Report MSR-TR-2010-9, Microsoft Research, January 2010. [ bib \| http ]
[24]	Ernie Cohen and Bert Schirmer. From total store order to sequential consistency: A practical reduction theorem. In Matt Kaufmann, Lawrence Paulson, and Michael Norrish, editors, Interactive Theorem Proving (ITP 2010), Lecture Notes in Computer Science, Edinburgh, UK, 2010. Springer. To appear. [ bib ]
[25]	Ernie Cohen and Norbert Schirmer. A better reduction theorem for store buffers. Technical Report arXiv:0909.4637, arXiv, September 2009. [ bib \| http \| .pdf ]
[26]	Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, and Wolfram Schulte. VCC: Contract-based modular verification of concurrent C. In ICSE Companion 2009: 31st International Conference on Software Engineering, pages 429-430. IEEE, May 2009. [ bib \| http ]
[27]	Ulan Degenbaev, Wolfgang J. Paul, and Norbert Schirmer. Pervasive theory of memory. In Susanne Albers, Helmut Alt, and Stefan Näher, editors, Efficient Algorithms - Essays Dedicated to Kurt Mehlhorn on the Occasion of His 60th Birthday, volume 5760 of Lecture Notes in Computer Science, pages 74-98. Springer, 2009. [ bib \| http ]
[28]	Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In Matthias Blume, Naoki Kobayashi, and Germán Vidal, editors, Functional and Logic Programming (FLOPS 2010), volume 6009 of Lecture Notes in Computer Science, pages 103-117, Sendai, Japan, 2010. Springer. [ bib \| http ]
[29]	Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Nested interpolants. In Manuel V. Hermenegildo and Jens Palsberg, editors, Principles of Programming Languages (POPL 2010), pages 471-482, Madrid, Spain, January 2010. ACM. [ bib \| http ]
[30]	Mark A. Hillebrand and Dirk C. Leinenbach. Formal verification of a reader-writer lock implementation in C. In Workshop on Systems Software Verification (SSV 2009), volume 254 of Electronic Notes in Theoretical Computer Science, pages 123-141. Elsevier Science B.V., 2009. [ bib \| http \| sources (.tar.gz) ]
[31]	Ulrich Kühne. Advanced Automation in Formal Verification of Processors. PhD thesis, University of Bremen, September 2009. [ bib \| http ]
[32]	Ulrich Kühne, Daniel Große, and Rolf Drechsler. Property analysis and design understanding in a quality-driven bounded model checking flow. In Magdy S. Abadir, Li-C. Wang, and Jayanta Bhadra, editors, Workshop on Microprocessor Test and Verification (MTV 2008), pages 88-93, Austin, Texas, USA, December 2008. IEEE. [ bib \| http \| .pdf ]
[33]	Ulrich Kühne, Daniel Große, and Rolf Drechsler. Property analysis and design understanding. In Design, Automation, and Test in Europe (DATE 2009), pages 1246-1249, Nice, France, April 2009. European Design and Automation Association (EDAA). [ bib \| http \| .pdf ]
[34]	Dirk Leinenbach and Thomas Santen. Verifying the Microsoft Hyper-V Hypervisor with VCC. In Formal Methods (FM 2009), volume 5850 of Lecture Notes in Computer Science, pages 806-809, Eindhoven, the Netherlands, 2009. Springer. Invited paper. [ bib \| http ]
[35]	Dirk Leinenbach and Thomas Santen. Verifying the Microsoft Hyper-V Hypervisor with VCC. In Jean-Raymond Abrial, Michael Butler, Rajeev Joshi, Elena Troubitsyna, and Jim C. P. Woodcock, editors, 09381 Extended Abstracts Collection - Refinement Based Methods for the Construction of Dependable Systems, number 09381 in Dagstuhl Seminar Proceedings, pages 104-108, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany. [ bib \| http ]
[36]	Sacha Loitz, Markus Wedler, Christian Brehm, Timo Vogt, Norbert Wehn, and Wolfgang Kunz. Proving functional correctness of weakly programmable IPs - A case study with formal property checking. In Symposium on Application Specific Processors (SASP 2008), pages 48-54, Anaheim, CA, USA, June 2008. IEEE. [ bib \| http ]
[37]	David C. J. Matthews and Makarius Wenzel. Efficient parallel programming in Poly/ML and Isabelle/ML. In Workshop on Declarative Aspects of Multicore Programming (DAMP 2010), pages 53-62, Madrid, Spain, 2010. ACM. [ bib \| http \| .pdf ]
[38]	Stefan Maus, Michal Moskal, and Wolfram Schulte. Vx86: x86 assembler simulated in C powered by automated theorem proving. In José Meseguer and Grigore Rosu, editors, Algebraic Methodology and Software Technology (AMAST 2008), volume 5140 of Lecture Notes in Computer Science, pages 284-298, Urbana, IL, USA, July 2008. Springer. [ bib \| http ]
[39]	Michal Moskal. Programming with triggers. In Workshop on Satisfiability Modulo Theories (SMT 2009), volume 375 of ACM International Conference Proceeding Series, pages 20-29. ACM, August 2009. [ bib \| http ]
[40]	Michal Moskal. Satisfiability Modulo Software. PhD thesis, University of Wroclaw, December 2009. [ bib \| .pdf ]
[41]	Minh Duc Nguyen, Max Thalmaier, Markus Wedler, Jörg Bormann, Dominik Stoffel, and Wolfgang Kunz. Unbounded protocol compliance verification using interval property checking with invariants. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(11):2068-2082, November 2008. [ bib \| http ]
[42]	Minh Duc Nguyen, Max Thalmaier, Markus Wedler, Dominik Stoffel, and Wolfgang Kunz. A re-use methodology for formal SoC protocol compliance. In Forum on Specification & Design Languages (FDL 2009), Sophia Antipolis, France, September 2009. To appear. [ bib ]
[43]	Evgeny Pavlenko, Markus Wedler, Dominik Stoffel, Oliver Wienand, Evgenij Karibaev, and Wolfgang Kunz. Modeling of custom-designed arithmetic components in ABL normalization. In Forum on Specification & Design Languages (FDL 2008), Stuttgart, Germany, September 2008. [ bib ]
[44]	Frank Rogin, Thomas Klotz, Görschwin Fey, Rolf Drechsler, and Steffen Rülke. Automatic generation of complex properties for hardware designs. In Design, Automation, and Test in Europe (DATE 2008), pages 545-548, Munich, Germany, March 2008. ACM. [ bib \| http ]
[45]	Mohamed Nassim Seghir, Andreas Podelski, and Thomas Wies. Abstraction refinement for quantified array assertions. In Jens Palsberg and Zhendong Su, editors, Static Analysis (SAS 2009), volume 5673 of Lecture Notes in Computer Science, pages 3-18, Los Angeles, CA, USA, August 2009. Springer. [ bib \| http ]
[46]	Maria Spichkova. Refinement-based specification and verification. In Jean-Raymond Abrial, Michael Butler, Rajeev Joshi, Elena Troubitsyna, and Jim C. P. Woodcock, editors, 09381 Extended Abstracts Collection - Refinement Based Methods for the Construction of Dependable Systems, number 09381 in Dagstuhl Seminar Proceedings, page 18, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany. [ bib \| http ]
[47]	David Trachtenherz. Ausführungssemantik von AutoFocus-Modellen: Isabelle/HOL-Formalisierung und Äquivalenzbeweis. Technical report, Institut für Informatik, Technische Universität München, January 2009. [ bib \| .pdf ]
[48]	David Trachtenherz. Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter Systeme. PhD thesis, Institut für Informatik, Technische Universität München, 2009. [ bib \| http \| .pdf ]
[49]	Makarius Wenzel. Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit. In Claudio Sacerdoti Coen and David Aspinall, editors, Workshop on User Interfaces for Theorem Provers (UITP 2010), Electronic Notes in Theoretical Computer Science, Edinburgh, UK, 2010. Elsevier Science B.V. To appear. [ bib ]
[50]	Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of Lecture Notes in Computer Science, pages 33-38, Montréal, Québec, Canada, 2008. Springer. Invited paper. [ bib \| http \| .pdf ]
[51]	Makarius Wenzel and Burkhart Wolff. Building formal method tools in the Isabelle/Isar framework. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of Lecture Notes in Computer Science, pages 352-267, Kaiserslautern, Germany, 2007. Springer. [ bib \| http \| .pdf ]
[52]	Markus Wenzel. Parallel proof checking in Isabelle / Isar. In R. Dos Reis and L. Théry, editors, The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). ACM, August 2009. To appear. [ bib ]
[53]	Oliver Wienand, Markus Wedler, Gert-Martin Greuel, Dominik Stoffel, and Wolfgang Kunz. An algebraic approach for proving data correctness in arithmetic data paths. In Computer Aided Verification (CAV 2008), volume 5123 of Lecture Notes in Computer Science, pages 473-486, Princeton, NJ, USA, July 2008. Springer. [ bib \| http ]

This file was generated by bibtex2html 1.95.

Revision 16 Jun 2010	Copyright © 2007—2010 Verisoft XT Consortium.