| Alkassar, E. and Hillebrand, M. A. and Leinenbach, D. C. and Schirmer, N. W. and Starostin, A. and Tsyban, A. |
|
EE |
BibTeX |
| Balancing the Load: Leveraging Semantics Stack for Systems Verification. | | In Klein, Gerwin and Huuck, Ralf and Schlich, Bastian, editors, Journal of Automated Reasoning: Special Issue on Operating Systems Verification, | | pages 389-454, Springer, 2009. | | ISBN 0168-7433 | | | | Hillebrand, M. and Leinenbach, D. |
|
EE |
BibTeX |
| Formal Verification of a Reader-Writer Lock Implementation in C. | | In 4th International Workshop on Systems Software Verification (SSV09), | | volume 254 of Electronic Notes in Theoretical Computer Science, pages 123-141, Elsevier Science B. V., 2009. | | | | Cohen, E. and Dahlweid, M. and Hillebrand, M. and Leinenbach, D. and Moskal, M. and Santen, T. and Schulte, W. and Tobies, S. |
|
EE |
BibTeX |
| VCC: A Practical System for Verifying Concurrent C. | | In Stefan Berghofer and Tobias Nipkow and Christian Urban and Markus Wenzel, editors, Proceedings of the 22nd International Conference on Theorem proving in Higher-Order Logics (TPHOLs 2009), | | Munich, Germany | | volume 5674 of Lecture Notes in Computer Science, pages 23--42, Springer, 2009. | | | | Leinenbach, D. and Santen, T. |
|
EE |
BibTeX |
| Verifying the Microsoft Hyper-V Hypervisor with VCC. | | In 16th International Symposium on Formal Methods (FM 2009), | | Eindhoven, the Netherlands | | volume 5850 of Lecture Notes in Computer Science, pages 806-809, Springer, 2009. | | Note: Invited paper. | | | | Cohen, E. and Alkassar, E. and Boyarinov, V. and Dahlweid, M. and Degenbaev, U. and Hillebrand, M. and Langenstein, B. and Leinenbach, D. and Moskal, M. and Obua, S. and Paul, W. and Pentchev, H. and Petrova, E. and Santen, T. and Schirmer, N. and Schmaltz, S. and Schulte, W. and Shadrin, A. and Tobies, S. and Tsyban, A. and Tverdyshev, S. |
 |
EE |
BibTeX |
| Invariants, Modularity, and Rights. | | In Amir Pnueli and Irina Virbitskaite and Andrei Voronkov, editors, Perspectives of Systems Informatics (PSI 2009), | | Novosibirsk, Russia | | volume 5947 of Lecture Notes in Computer Science, pages 43--55, Springer, 2009. | | | | Leinenbach, D. and Petrova, E. |
|
EE |
BibTeX |
| Pervasive Compiler Verification -- From Verified Programs to Verified Systems. | | In 3rd intl Workshop on Systems Software Verification (SSV08)., | | volume 217C of Electronic Notes in Theoretical Computer Science, pages 23-40, Elsevier Science B. V., 2008. | | | | Alkassar, Eyad and Hillebrand, Mark A. and Leinenbach, Dirk and Schirmer, Norbert W. and Starostin, Artem |
|
EE |
BibTeX |
| The Verisoft Approach to Systems Verification. | | In Natarajan Shankar and Jim Woodcock, editors, 2nd IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), | | volume 5295 of LNCS, pages 209--224, Springer, 2008. | | | | Leinenbach, Dirk |
|
|
BibTeX |
| Compiler Verification in the Context of Pervasive System Verification. | | | Dissertation, Saarland University, Saarbrücken, 2008. | | | | Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D. and Paul, W.J. |
|
EE |
BibTeX |
| Putting it all together - Formal Verification of the VAMP. | | In STTT Journal, Special Issue on Recent Advances in Hardware Verification, | | Springer, 2006. | | | | Gargano, M. and Hillebrand, M. and Leinenbach, D. and Paul, W. |
|
EE |
BibTeX |
| On the Correctness of Operating System Kernels. | | In Hurd, J. and Melham, T., editors, Theorem Proving in High Order Logics (TPHOLs) 2005, | | Oxford, U.K. | | LNCS, Springer, 2005. | | | | Leinenbach, D. and Paul, W. and Petrova, E. |
|
EE |
BibTeX |
| Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctness. | | In 3rd International Conference on Software Engineering and Formal Methods (SEFM 2005), | | Koblenz, Germany | | 2005. | | Note: This material is presented to ensure timely dissemination of
scholarly and technical work. Copyright and all rights therein are
retained by authors or by other copyright holders. All persons copying
this information are expected to adhere to the terms and constraints
invoked by each author's copyright. In most cases, these works may not
be reposted without the explicit permission of the copyright holder. | | | | Beyer, S. and Böhm, P. and Gerke, M. and Hillebrand, M. and In der Rieden, T. and Knapp, S. and Leinenbach, D. and Paul, W.J. |
|
EE |
BibTeX |
| Towards the Formal Verification of Lower System Layers in Automotive Systems. | | In 23nd IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD 2005), 2-5 October 2005, San Jose, CA, USA, Proceedings, | | pages 317-324, IEEE, 2005. | | ISBN 0-7695-2451-6 | | | | In der Rieden, T., and Leinenbach, D., and W. J. Paul |
|
EE |
BibTeX |
| Towards the Pervasive Verification of Automotive Systems. | | In Dominique Borrione, and Wolfgang Paul, editors, Correct Hardware Design and Verification Methods (CHARME 2005), | | volume 3725 of Lecture Notes in Computer Science, pages 3-4, Springer, 2005. | | ISBN 3-540-29105-9 | | | | Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D. and Paul, W.J. |
|
EE |
BibTeX |
| Instantiating uninterpreted functional units and memory system: functional verification of the VAMP. | | In Geist, D. and Tronci, E., editors, CHARME 2003, | | volume 2860 of LNCS, pages 51-65, Springer, 2003. | | | | Berg, C. and Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D. |
|
|
BibTeX |
| Formal Verification of the VAMP Microprocessor (Project Status). | | In Charatonik, Witold and Ganzinger, Harald, editors, Symposium on the Effectiveness of Logic in Computer Science (ELICS02), | | pages 31-36, Max-Planck-Institut für Informatik, 2002. | | | | Leinenbach, Dirk |
|
|
BibTeX |
| Implementierung eines maschinell verifizierten Prozessors. | | | Diplomarbeit, Universität des Saarlandes, 2002. | | | | Beyer, S. and Jacobi, C. and Kroening, D. and Leinenbach, D. |
|
|
BibTeX |
| Correct Hardware by Synthesis from PVS. | | 2002. | | unpublished, available at http://www-wjp.cs.uni-saarland.de/publikationen/BJKL02.pdf | | |
|
