Publications

[1]	Bernhard K. Aichernig and Bernhard Beckert, editors. Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany. IEEE Computer Society, 2005. [ bib ]
[2]	Eyad Alkassar. OS Verication Extended - On the Formal Verication of Device Drivers and the Correctness of Client/Server Software. PhD thesis, Saarland University, Computer Science Department, 2009. [ bib | .pdf ]
[3]	Eyad Alkassar, Sebastian Bogan, and Wolfang Paul. Proving the correctness of client/server software. Sadhana: Academy Proceedings in Engineering Sciences, 34(1):145-191, 2009. [ bib | http | .pdf ]
[4]	Eyad Alkassar, Peter Böhm, and Steffen Knapp. Correctness of a fault-tolerant real-time scheduler algorithm and its hardware implementation. In 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2008), June 5-7 2008, Anaheim, CA, USA, pages 175-186. IEEE, 2008. [ bib | http ]
[5]	Eyad Alkassar, Peter Böhm, and Steffen Knapp. Formal correctness of an automotive bus controller implementation at gate-level. In Bernd Kleinjohann, Lisa Kleinjohann, and Wayne Wolf, editors, 6th IFIP Working Conference on Distributed and Parallel Embedded Systems (DIPES 2008), September 7-10 2008, Milano Italy, volume 271 of International Federation for Information Processing, pages 57-67. Springer, 2008. [ bib | http ]
[6]	Eyad Alkassar, Mark Hillebrand, Steffen Knapp, Rostislav Rusev, and Sergey Tverdyshev. Formal device and programming model for a serial interface. In Bernhard Beckert, editor, Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany, volume 259 of CEUR Workshop Proceedings, pages 4-20. CEUR-WS.org, 2007. [ bib | .pdf ]
[7]	Eyad Alkassar and Mark A. Hillebrand. Formal functional verification of device drivers. In Jim Woodcock and Natarajan Shankar, editors, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, volume 5295 of Lecture Notes in Computer Science, pages 225-239, Toronto, Canada, October 2008. Springer. [ bib | http ]
[8]	Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert W. Schirmer, and Artem Starostin. The Verisoft approach to systems verification. In Natarajan Shankar and Jim Woodcock, editors, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, volume 5295 of Lecture Notes in Computer Science, pages 209-224, Toronto, Canada, October 2008. Springer. [ bib | http ]
[9]	Eyad Alkassar, Mark A. Hillebrand, Dirk C. Leinenbach, Norbert W. Schirmer, Artem Starostin, and Alexandra Tsyban. Balancing the load: Leveraging a semantics stack for systems verification. Journal of Automated Reasoning: Operating System Verification, 42(2-4):389-454, 2009. [ bib | http ]
[10]	Eyad Alkassar, Wolfgang Paul, Artem Starostin, and Alexandra Tsyban. Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices. In Peter O'Hearn, Gary T. Leavens, and Sriram Rajamani, editors, Verified Software: Theories, Tools, Experiments (VSTTE 2010), volume 6217 of Lecture Notes in Computer Science, pages 71-85, Edinburgh, UK, August 2010. Springer. [ bib | http ]
[11]	Eyad Alkassar, Norbert Schirmer, and Artem Starostin. Formal pervasive verification of a paging mechanism. In C. R. Ramakrishnan and Jakob Rehof, editors, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08), volume 4963 of Lecture Notes in Computer Science, pages 109-123. Springer, 2008. [ bib | http ]
[12]	Nathaniel Ayewah, Sven Beyer, Nikhil Kikkeri, and Peter-Michael Seidel. Challenges in the formal verification of complete state-of-the-art processors. In 23rd International Conference on Computer Design (ICCD 2005), 2-5 October 2005, San Jose, CA, USA, pages 603-608. IEEE Computer Society, 2005. [ bib | http ]
[13]	Bernhard Beckert and Gerd Beuster. Formal specification of security-relevant properties of user interfaces. In Proceedings, 3rd International Workshop on Critical Systems Development with UML, pages 139-146, Lisbon, Portugal, 2004. TU Munich Technical Report TUM-I0415. [ bib | .pdf ]
[14]	Bernhard Beckert and Gerd Beuster. A method for formalizing, analyzing, and verifying secure user interfaces. In Zhiming Liu and Jifeng He, editors, Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006, Proceedings, volume 4260 of Lecture Notes in Computer Science, pages 55-73. Springer, 2006. [ bib | http | .pdf ]
[15]	Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, and Steffen Schlager. Taclets: A new paradigm for constructing interactive theorem provers. Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales, Serie A: Matemáticas (RACSAM), 98(1):17-53, 2004. Special Issue on Symbolic Computation in Logic and Artificial Intelligence. [ bib | http | .pdf ]
[16]	Bernhard Beckert and Vladimir Klebanov. Proof reuse for deductive program verification. In 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 28-30 September 2004, Beijing, China, pages 77-86. IEEE Computer Society, 2004. [ bib | http | .pdf ]
[17]	Bernhard Beckert and André Platzer. Dynamic logic with non-rigid functions. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science, pages 266-280. Springer, 2006. [ bib | http | .pdf ]
[18]	Bernhard Beckert and Steffen Schlager. Software verification with integrated data type refinement for integer arithmetic. In Eerke A. Boiten, John Derrick, and Graeme Smith, editors, Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings, volume 2999 of Lecture Notes in Computer Science, pages 207-226. Springer, 2004. [ bib | http | .pdf ]
[19]	Bernhard Beckert and Steffen Schlager. Refinement and retrenchment for programming language data types. Formal Aspects of Computing, 17(4):423-442, 2005. [ bib | http | .pdf ]
[20]	Bernhard Beckert, Steffen Schlager, and Peter H. Schmitt. An improved rule for while loops in deductive program verification. In Kung-Kiu Lau and Richard Banach, editors, Formal Methods and Software Engineering, 7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005, Proceedings, volume 3785 of Lecture Notes in Computer Science, pages 315-329. Springer, 2005. [ bib | http | .pdf ]
[21]	Bernhard Beckert and Kerry Trentelman. Second-order principles in specification languages for object-oriented programs. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, volume 3835 of Lecture Notes in Computer Science, pages 154-168. Springer, 2005. [ bib | http | .pdf ]
[22]	Stefan Berghofer and Tobias Nipkow. Random testing in Isabelle/HOL. In 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 28-30 September 2004, Beijing, China, pages 230-239. IEEE Computer Society, 2004. [ bib | http ]
[23]	Gerd Beuster, Niklas Henrich, and Markus Wagner. Real world verification - Experiences from the Verisoft email client. In Geoff Sutcliffe, Renate Schmidt, and Stephan Schulz, editors, Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning (ESCoR 2006), volume 192 of CEUR Workshop Proceedings, pages 112-125. CEUR-WS.org, August 2006. [ bib | .pdf ]
[24]	Sven Beyer, Peter Böhm, Michael Gerke, Mark Hillebrand, Thomas In der Rieden, Steffen Knapp, Dirk Leinenbach, and Wolfgang J. Paul. Towards the formal verification of lower system layers in automotive systems. In ICCD '05, pages 317-324. IEEE Computer Society, 2005. [ bib | http ]
[25]	Sven Beyer, Christian Jacobi, Daniel Kroening, Dirk Leinenbach, and Wolfgang Paul. Putting it all together: Formal verification of the VAMP. International Journal on Software Tools for Technology Transfer, 8(4-5):411-430, August 2006. [ bib | http ]
[26]	Sebastian Bogan. Formal Specification of a Simple Operating System. PhD thesis, Saarland University, Computer Science Department, August 2008. [ bib | .pdf ]
[27]	Jewgenij Botaschanjan, Alexander Gruler, Alexander Harhurin, Leonid Kof, Maria Spichkova, and David Trachtenherz. Towards modularized verification of distributed time-triggered systems. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings, volume 4085 of Lecture Notes in Computer Science, pages 163-178. Springer, 2006. [ bib | http ]
[28]	Jewgenij Botaschanjan, Leonid Kof, Christian Kühnel, and Maria Spichkova. Towards verified automotive software. In SEAS '05: Proceedings of the Second International Workshop on Software Engineering for Automotive Systems, pages 46-51. ACM, 2005. [ bib | http | .pdf ]
[29]	Amine Chaieb. Verifying mixed real-integer quantifier elimination. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science, pages 528-540. Springer, 2006. [ bib | http ]
[30]	Lassaad Cheikhrouhou, Georg Rock, Werner Stephan, Matthias Schwan, and Gunter Lassmann. Verifying a chipcard-based biometric identification protocol in VSE. In Janusz Górski, editor, Computer Safety, Reliability, and Security, 25th International Conference, SAFECOMP 2006, Gdansk, Poland, September 27-29, 2006, Proceedings, volume 4166 of Lecture Notes in Computer Science, pages 42-56. Springer, 2006. [ bib | http ]
[31]	Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Abstraction refinement for termination. In Chris Hankin and Igor Siveroni, editors, Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings, volume 3672 of Lecture Notes in Computer Science, pages 87-101. Springer, 2005. [ bib | http ]
[32]	Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for systems code. In Michael I. Schwartzbach and Thomas Ball, editors, Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11-14, 2006, pages 415-426. ACM, 2006. [ bib | http ]
[33]	Philipp Correll and Gernot Stenz. Proof output and transformation for disconnection tableaux. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, volume 3702 of Lecture Notes in Computer Science, pages 312-317. Springer, 2005. [ bib | http | .pdf ]
[34]	Iakov Dalinger, Mark Hillebrand, and Wolfgang Paul. On the verification of memory management mechanisms. In Dominique Borrione and Wolfgang Paul, editors, Proceedings of the 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2005), volume 3725 of Lecture Notes in Computer Science, pages 301-316. Springer, 2005. [ bib | http ]
[35]	Ben D'Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, and Zohar Manna. LOLA: Runtime monitoring of synchronous systems. In 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA, pages 166-174. IEEE Computer Society, 2005. [ bib | http | .pdf ]
[36]	Matthias Daum. Reasoning on data-parallel programs in Isabelle/HOL. In Hendrik Tews, editor, Proceedings of the C/C++ Verification Workshop, number R07015 in ICIS Technical Report, pages 17-28. Radboud University Nijmegen, June 2007. [ bib | .pdf ]
[37]	Matthias Daum. Modelling user programs on top of a microkernel. In Elena Troubitsyna, editor, Proceedings of Doctoral Symposium Held in Conjunction with Formal Methods 2008, volume 48 of General Publications. Turku Centre for Computer Science, 2008. [ bib | .pdf ]
[38]	Matthias Daum. Temporal fairness of a microkernel scheduler. In Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, Doctoral Symposium on Systems Software Verification (DS SSV'09), volume AIB-2009-14 of Aachener Informatik Berichte, pages 1-3. Department of Computer Science, RWTH Aachen, June 2009. [ bib | .pdf | .pdf ]
[39]	Matthias Daum. On the Formal Foundation of a Verification Approach for System-Level Concurrent Programs. PhD thesis, Saarland University, Computer Science Department, June 2010. [ bib | .pdf ]
[40]	Matthias Daum, Jan Dörrenbächer, and Sebastian Bogan. Model stack for the pervasive verification of a microkernel-based operating system. In Bernhard Beckert and Gerwin Klein, editors, Proceedings, 5th International Verification Workshop (VERIFY), Sydney, Australia, volume 372 of CEUR Workshop Proceedings, pages 56-70. CEUR-WS.org, August 2008. [ bib | .pdf ]
[41]	Matthias Daum, Jan Dörrenbächer, and Burkhart Wolff. Proving fairness and implementation correctness of a microkernel scheduler. Journal of Automated Reasoning: Operating System Verification, 42(2-4):349-388, 2009. [ bib | http ]
[42]	Matthias Daum, Jan Dörrenbächer, Burkhart Wolff, and Mareike Schmidt. A verification approach for system-level concurrent programs. In Jim Woodcock and Natarajan Shankar, editors, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, volume 5295 of Lecture Notes in Computer Science, pages 161-176, Toronto, Canada, October 2008. Springer. [ bib | http ]
[43]	Matthias Daum, Stefan Maus, Norbert Schirmer, and M. Nassim Seghir. Integration of a software model checker into Isabelle. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, volume 3835 of Lecture Notes in Computer Science, pages 381-395. Springer, 2005. [ bib | http ]
[44]	Matthias Daum, Norbert Walter Schirmer, and Mareike Schmidt. Implementation correctness of a real-time operating system. In Dang Van Hung and Padmanabhan Krishnan, editors, 7th International Conference on Software Engineering and Formal Methods (SEFM 2009), pages 23-32, Hanoi, Vietnam, November 2009. IEEE Computer Society. [ bib | http ]
[45]	Thomas In der Rieden. Verified Linking for Modular Kernel Verification. PhD thesis, Saarland University, Computer Science Department, November 2009. [ bib | .pdf ]
[46]	Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny Sipma. Collecting statistics over runtime executions. Formal Methods in System Design, 27(3):253-274, November 2005. [ bib | http | .pdf ]
[47]	Bernd Finkbeiner and Henny Sipma. Checking finite traces using alternating automata. Formal Methods in System Design, 24(2):101-127, March 2004. [ bib | http | .pdf ]
[48]	Sabine Fischer. Formal verification of a big integer library. In Workshop on Dependable Software Systems at DATE'08, 2008. [ bib | .pdf ]
[49]	Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, and Wolfgang Paul. On the correctness of operating system kernels. In Joe Hurd and Thomas F. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), volume 3603 of Lecture Notes in Computer Science, pages 1-16. Springer, 2005. [ bib | http | .pdf ]
[50]	Mark Hillebrand, Thomas In der Rieden, and Wolfgang Paul. Dealing with I/O devices in the context of pervasive system verification. In ICCD '05, pages 309-316. IEEE Computer Society, 2005. [ bib | http ]
[51]	Mark Hillebrand and Sergey Tverdyshev. Formal verification of gate-level computer systems. In Anna Frid, Andrey Morozov, Andrey Rybalchenko, and Klaus W. Wagner, editors, Computer Science - Theory and Applications, Fourth International Computer Science Symposium in Russia, CSR 2009, Novosibirsk, Russia, August 18-23, 2009, Proceedings, volume 5675 of Lecture Notes in Computer Science, pages 322-333. Springer, 2009. [ bib | http ]
[52]	Mark A. Hillebrand and Wolfgang Paul. On the architecture of system verification environments. In Karen Yorav, editor, Hardware and Software, Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel, October 23-25, 2007, volume 4899 of Lecture Notes in Computer Science, pages 153-168. Springer, 2008. [ bib | http ]
[53]	Dieter Hutter. A management of change. Schloß Dagstuhl Seminar 3451 Applied Deductive Verification, http://www.dagstuhl.de/, November 2003. [ bib ]
[54]	Dieter Hutter. Towards a generic management of change. In Christoph Benzmüller and Wolfgang Windsteiger, editors, Proceedings of the First Workshop on Computer-Supported Mathematical Theory Development Held in the Frame of IJCAR'04 in Cork, Ireland, July 5, 2004, number 04-14 in RISC Report Series, pages 7-18. RISC Institute, University of Linz, July 2004. [ bib | .html | .pdf ]
[55]	Dieter Hutter and Axel Schairer. Possibilistic information flow control in the presence of encrypted communication. In Pierangela Samarati, Peter Y. A. Ryan, Dieter Gollmann, and Refik Molva, editors, Computer Security - ESORICS 2004, 9th European Symposium on Research Computer Security, Sophia Antipolis, France, September 13-15, 2004, Proceedings, volume 3193 of Lecture Notes in Computer Science, pages 209-224. Springer, 2004. [ bib | http ]
[56]	Thomas In der Rieden and Steffen Knapp. An approach to the pervasive formal specification and verification of an automotive system. In FMICS '05, pages 115-124. IEEE Computer Society, 2005. [ bib | http | .pdf ]
[57]	Thomas In der Rieden, Dirk Leinenbach, and Wolfgang Paul. Towards the pervasive verification of automotive systems. In Dominique Borrione and Wolfgang Paul, editors, Proceedings of the 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2005), volume 3725 of Lecture Notes in Computer Science, pages 3-4. Springer, 2005. [ bib | http ]
[58]	Thomas In der Rieden and Wolfgang J. Paul. Beweisen als Ingenieurwissenschaft: Verbundprojekt Verisoft (2003-2007). In Bernd Reuse and Roland Vollmar, editors, Informatikforschung in Deutschland, pages 321-326. Springer, 2008. [ bib ]
[59]	Tom In der Rieden and Alexandra Tsyban. CVM - A verified framework for microkernel programmers. In 3rd International Workshop on Systems Software Verification (SSV 2008), volume 217C of Electronic Notes in Theoretical Computer Science, pages 151-168. Elsevier Science B.V., 2008. [ bib | http ]
[60]	Jan Jürjens. Secure Systems Development with UML. Springer, 2005. [ bib ]
[61]	Jan Jürjens. Sound methods and effective tools for model-based security engineering with UML. In Gruia-Catalin Roman, William G. Griswold, and Bashar Nuseibeh, editors, 27th International Conference on Software Engineering (ICSE 2005), 15-21 May 2005, St. Louis, Missouri, USA, pages 322-331. ACM, 2005. [ bib | http ]
[62]	Jan Jürjens and Pasha Shabalin. Automated verification of UMLsec models for security requirements. In Thomas Baar, Alfred Strohmeier, Ana M. D. Moreira, and Stephen J. Mellor, editors, UML 2004 - The Unified Modelling Language: Modelling Languages and Applications. 7th International Conference, Lisbon, Portugal, October 11-15, 2004. Proceedings, volume 3273 of Lecture Notes in Computer Science, pages 365-379. Springer, 2004. [ bib | http | .pdf ]
[63]	Jan Jürjens and Pasha Shabalin. Tools for critical systems development with UML (tool demo). In Nuno Jardim Nunes, Bran Selic, Alberto Rodrigues da Silva, and José Ambrosio Toval Álvarez, editors, UML Modeling Languages and Applications, UML 2004 Satellite Activities, Lisbon, Portugal, October 11-15, 2004, Revised Selected Papers, volume 3297 of Lecture Notes in Computer Science, pages 250-253. Springer, 2004. [ bib | http ]
[64]	Markus Kaiser and Johannes Buchmann. Computer verification in cryptography. Proceedings of the World Academy of Science, Engineering and Technology, 12:155-160, March 2006. [ bib | .pdf ]
[65]	Gerwin Klein and Tobias Nipkow. A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Transactions on Programming Languages and Systems, 28(4):619-695, 2006. [ bib | http ]
[66]	Steffen Knapp. The Correctness of a Distributed Real-Time System. PhD thesis, Saarland University, Computer Science Department, July 2008. [ bib | .pdf ]
[67]	Steffen Knapp and Wolfgang Paul. Pervasive verification of distributed real-time systems. In Manfred Broy, Johannes Grünbauer, and Tony Hoare, editors, Software System Reliability and Security, volume 9 of IOS Press, NATO Security Through Science Series. Sub-Series D: Information and Communication Security, pages 239-297, 2007. [ bib | .pdf ]
[68]	Steffen Knapp and Wolfgang Paul. Realistic worst case execution time analysis in the context of pervasive system verification. In Thomas Reps, Mooly Sagiv, and Jörg Bauer, editors, Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, volume 4444 of Lecture Notes in Computer Science, pages 53-81. Springer, 2007. [ bib | http | .pdf ]
[69]	Alexander Krauss. Partial recursive functions in higher-order logic. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science, pages 589-603. Springer, 2006. [ bib | http ]
[70]	Christian Kühnel and Maria Spichkova. Upcoming automotive standards for fault-tolerant communication: FlexRay and OSEKtime FTCom. In International Workshop on Engineering of Fault-Tolerant Systems (EFTS 2006), 12-13 June 2006, Luxembourg, pages 68-79, June 2006. [ bib | http | .pdf ]
[71]	Bruno Langenstein, Andreas Nonnengart, Georg Rock, and Werner Stephan. A history-based verification of distributed applications. In Bernhard Beckert, editor, Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany, volume 259 of CEUR Workshop Proceedings, pages 70-84. CEUR-WS.org, 2007. [ bib | .pdf ]
[72]	Bruno Langenstein, Andreas Nonnengart, Georg Rock, and Werner Stephan. Verification of distributed applications. In Francesca Saglietti and Norbert Oster, editors, Computer Safety, Reliability, and Security, 26th International Conference, SAFECOMP 2007, Nuremberg, Germany, September 18-21, 2007, volume 4680 of Lecture Notes in Computer Science, pages 315-328. Springer, 2007. [ bib | http ]
[73]	Gunter Lassmann, Georg Rock, Matthias Schwan, and Lassaad Cheikhrouhou. Verisoft secure biometric identification system. T-Systems International University Conference, Düsseldorf, 10.-11. October 2005. [ bib | .pdf ]
[74]	Dirk Leinenbach, Wolfgang Paul, and Elena Petrova. Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In Bernhard Aichernig and Bernhard Beckert, editors, 3rd International Conference on Software Engineering and Formal Methods (SEFM 2005), 5-9 September 2005, Koblenz, Germany, pages 2-11, 2005. [ bib | http ]
[75]	Dirk Leinenbach and Elena Petrova. Pervasive compiler verification - From verified programs to verified systems. In 3rd International Workshop on Systems Software Verification (SSV 2008), volume 217C of Electronic Notes in Theoretical Computer Science, pages 23-40. Elsevier Science B.V., 2008. [ bib | http ]
[76]	Dirk Carsten Leinenbach. Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University, Computer Science Department, July 2008. [ bib | .pdf ]
[77]	Reinhold Letz and Gernot Stenz. Generalised handling of variables in disconnection tableaux. In David A. Basin and Michaël Rusinowitch, editors, Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, volume 3097 of Lecture Notes in Computer Science, pages 289-306. Springer, 2004. [ bib | http | .pdf ]
[78]	Reinhold Letz and Gernot Stenz. The disconnection tableau calculus. Journal of Automated Reasoning, 38(1-3):79-126, 2007. [ bib | http ]
[79]	Christina Lindenberg, Kai Wirt, and Johannes Buchmann. Formal proof for the correctness of RSA-PSS. Cryptology ePrint Archive, Report 2006/011, 2006. [ bib | http ]
[80]	Farhad Mehta and Tobias Nipkow. Proving pointer programs in higher-order logic. In Franz Baader, editor, Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, volume 2741 of Lecture Notes in Computer Science, pages 121-135. Springer, 2003. [ bib | http ]
[81]	Till Mossakowski, Serge Autexier, and Dieter Hutter. Development graphs - proof management for structured specifications. Journal of Logic and Algebraic Programming, 67(1-2):114-145, 2006. [ bib | http ]
[82]	Till Mossakowski, Piotr Hoffman, Serge Autexier, and Dieter Hutter. Part IV: CASL logic. In Peter D. Mosses, editor, CASL Reference Manual - The Complete Documentation of the Common Algebraic Specification Language, volume 2960 of Lecture Notes in Computer Science, pages 275-359. Springer, 2004. [ bib | http ]
[83]	Andreas Nonnengart, Georg Rock, and Werner Stephan. Verification support environment (VSE). In Proceedings of the 4th International Workshop on Planning and Scheduling for Space (IWPSS'04), number 228 in ESA-WPP, ESA-ESOC, Darmstadt, Germany, June 2004. European Space Agency Publications Division. [ bib | .pdf ]
[84]	Wolfgang Paul. Towards a worldwide verification technology. In First IFIP TC 2/WG 2.3 Conference on Verified Software: Theories, Tools, Experiments (VSTTE 2005), October 10-13, 2005, Revised Selected Papers and Discussions, volume 4171, pages 19-25, Zürich, Switzerland, June 2008. Springer. [ bib | http | .pdf ]
[85]	Elena Petrova. Verification of the C0 Compiler Implementation on the Source Code Level. PhD thesis, Saarland University, Computer Science Department, May 2007. [ bib | .pdf ]
[86]	Amir Pnueli, Andreas Podelski, and Andrey Rybalchenko. Separating fairness and well-foundedness for the analysis of fair discrete systems. In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 124-139. Springer, 2005. [ bib | http | .pdf ]
[87]	Andreas Podelski and Andrey Rybalchenko. Transition invariants. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 32-41. IEEE Computer Society, 2004. [ bib | http | .ps ]
[88]	Andreas Podelski and Andrey Rybalchenko. Transition predicate abstraction and fair termination. In Jens Palsberg and Martín Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 132-144. ACM, 2005. [ bib | http ]
[89]	Andreas Podelski and Ina Schaefer. Local reasoning for termination. In Dino Distefano, Radu Iosif, and Peter O'Hearn, editors, COSMICAH 2005: Workshop on Verification of Concurrent Systems with Dynamic Allocated Heaps (a Satellite Event of ICALP 2005) - Informal Proceedings, number RR-05-04 in Research Reports, pages 16-30, July 2005. [ bib | http | .pdf ]
[90]	Andreas Podelski, Ina Schaefer, and Silke Wagner. Summaries for while programs with recursion. In Shmuel Sagiv, editor, Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3444 of Lecture Notes in Computer Science, pages 94-107. Springer, 2005. [ bib | http ]
[91]	Andreas Podelski and Silke Wagner. Model checking of hybrid systems: From reachability towards stability. In João P. Hespanha and Ashish Tiwari, editors, Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29-31, 2006, Proceedings, volume 3927 of Lecture Notes in Computer Science, pages 507-521. Springer, 2006. [ bib | http ]
[92]	Andreas Podelski and Thomas Wies. Boolean heaps. In Chris Hankin and Igor Siveroni, editors, Static Analysis, 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005, Proceedings, volume 3672 of Lecture Notes in Computer Science, pages 268-283. Springer, 2005. [ bib | http ]
[93]	Norbert Schirmer. A verification environment for sequential imperative programs in Isabelle/HOL. In Franz Baader and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, volume 3452 of Lecture Notes in Computer Science, pages 398-414. Springer, 2005. [ bib | http | .pdf ]
[94]	Norbert Schirmer. Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technical University of Munich, April 2006. [ bib | http ]
[95]	Norbert Schirmer and Makarius Wenzel. State spaces - The locale way. In 4th International Workshop on Systems Software Verification (SSV 2009), volume 254 of Electronic Notes in Theoretical Computer Science, pages 161-179. Elsevier Science B.V., 2009. [ bib | http ]
[96]	Julien Schmaltz. A formal model of lower system layers. In Aarti Gupta and Panagiotis Manolios, editors, Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, November 12-16, 2006, Proceedings, pages 191-192, San Jose, CA, USA, November 2006. IEEE Computer Society. [ bib | http ]
[97]	Julien Schmaltz. A formal model of clock domain crossing and automated verification of time-triggered hardware. In Jason Baumgartner and Mary Sheeran, editors, Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings, pages 223-230. IEEE Computer Society, 2007. [ bib | http ]
[98]	Artem Starostin. Formal Verification of Demand Paging. PhD thesis, Saarland University, Computer Science Department, March 2010. [ bib | .pdf ]
[99]	Artem Starostin and Alexandra Tsyban. Correct microkernel primitives. In 3rd International Workshop on Systems Software Verification (SSV 2008), volume 217C of Electronic Notes in Theoretical Computer Science, pages 169-185. Elsevier Science B.V., 2008. [ bib | http ]
[100]	Artem Starostin and Alexandra Tsyban. Verified process-context switch for C-programmed kernels. In Jim Woodcock and Natarajan Shankar, editors, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, volume 5295 of Lecture Notes in Computer Science, pages 240-254, Toronto, Canada, October 2008. Springer. [ bib | http ]
[101]	Gernot Stenz. Unit propagation in a tableau framework. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, volume 3702 of Lecture Notes in Computer Science, pages 338-342. Springer, 2005. [ bib | http | .pdf ]
[102]	Alexandra Tsyban. Formal Verification of a Framework for Microkernel Programmers. PhD thesis, Saarland University, Computer Science Department, November 2009. [ bib | .pdf ]
[103]	Sergey Tverdyshev. Combination of Isabelle/HOL with automatic tools. In Bernhard Gramlich, editor, Frontiers of Combining Systems: 5th International Workshop, FroCoS 2005, Vienna Austria, September 19-21, 2005. Proceedings, volume 3717 of Lecture Notes in Computer Science, pages 302-309. Springer, 2005. [ bib | http ]
[104]	Sergey Tverdyshev. Formal Verification of Gate-Level Computer Systems. PhD thesis, Saarland University, Computer Science Department, May 2009. [ bib | .pdf ]
[105]	Sergey Tverdyshev. A verified platform for a gate-level electronic control unit. In Armin Biere and Carl Pixley, editors, Formal Methods in Computer-Aided Design, 9th International Conference (FMCAD 2009), pages 164-171, Austin, Texas, USA, November 2009. IEEE Computer Society. [ bib | http ]
[106]	Sergey Tverdyshev and Eyad Alkassar. Efficient bit-level model reductions for automated hardware verification. In 15th International Symposium on Temporal Representation and Reasoning (TIME 2008), pages 164-172. IEEE Computer Society Press, 2008. [ bib | http ]
[107]	Sergey Tverdyshev and Andrey Shadrin. Formal verification of gate-level computer systems. In Kristin Yvonne Rozier, editor, LFM 2008: Sixth NASA Langley Formal Methods Workshop, NASA Scientific and Technical Information (STI), pages 56-58. NASA, 2008. [ bib | .pdf ]
[108]	Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, and Frank Tip. An operational semantics and type safety proof for multiple inheritance in C++. In Peri L. Tarr and William R. Cook, editors, Proceedings of the 21th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006, October 22-26, 2006, Portland, Oregon, USA, pages 345-362. ACM, 2006. [ bib | http ]
[109]	Makarius Wenzel. Structured induction proofs in Isabelle/Isar. In Jonathan M. Borwein and William M. Farmer, editors, Mathematical Knowledge Management, 5th International Conference, MKM 2006, Wokingham, UK, August 11-12, 2006, Proceedings, volume 4108 of Lecture Notes in Computer Science, pages 17-30. Springer, 2006. [ bib | http ]
[110]	Markus Wenzel and Larry Paulson. Isabelle/Isar. In Freek Wiedijk, editor, The Seventeen Provers of the World, volume 3600 of Lecture Notes in Computer Science, pages 41-49. Springer, 2006. [ bib | http ]
[111]	Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin C. Rinard. Field constraint analysis. In E. Allen Emerson and Kedar S. Namjoshi, editors, Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, volume 3855 of Lecture Notes in Computer Science, pages 157-173. Springer, 2006. [ bib | http ]

This file was generated by bibtex2html 1.95.