| Alkassar, E. and Cohen, E. and Kovalev, M. and Paul, W. |
 |
|
BibTeX |
| Verification of TLB Virtualization Implemented in C. | | In 4th International Conference
on Veri ed Software: Theories, Tools, and Experiments, VSTTE'12, | | Philadelphia, USA | | Lecture Notes in Computer Science, Springer-Verlag, 2012. | | | | Alkassar, E. and Böhme, S. and Mehlhorn, K. and Rizkallah, C. |
|
|
BibTeX |
| Verification of Certifying Computations. | | In Conference on Computer Aided Verification (CAV 2011), | | LNCS, 2011. | | Note: To appear | | | | Klebanov, V and Müller, P. and Shankar, N. and Leavens, G. and Wüstholz, V. and Alkassar, E. and Arthan, R. and Bronish, D. and Chapman, R. and Cohen, E. and Hillebrand, M. and Jacobs, B and Leino, R. and Monahan, R. and Piessens, F. and Polikarpova, N. and Ridge, T. and Smans, J. and Tobies, S. and Tuerk, T. and Ulbrich, M. and Wei, B. |
|
|
BibTeX |
| The 1st Verified Software Competition: Experience Report. | | In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods (FM 2011), | | LNCS, 2011. | | Note: Best Paper Award | | | | Alkassar, E. and Hillebrand, M. and Paul, W. and Petrova, E. |
|
EE |
BibTeX |
| Automated Verification of a Small Hypervisor. | | In Third International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'10), | | Edinburgh, UK | | volume 6217 of LNCS, pages 40-54, Springer, 2010. | | | | Alkassar, E. and Paul, W. and Starostin, A. and Tsyban, A. |
|
EE |
BibTeX |
| Pervasive Verification of an OS Microkernel: Inline Assembly, Memory Consumption, Concurrent Devices. | | In Third International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'10), | | Edinburgh | | volume 6217 of LNCS, pages 71-85, Springer, 2010. | | | | Alkassar, E. and Cohen, E. and Hillebrand, M. and Kovalev, M. and Paul, W. |
|
|
BibTeX |
| Verifying Shadow Page Table Algorithms. | | In Formal Methods in Computer Aided Design (FMCAD) 2010, | | Lugano, Switzerland | | pages 267-270, IEEE, 2010. | | | | Alkassar, E. and Cohen, E. and Hillebrand, M. and Pentchev, H. |
|
|
BibTeX |
| Modular Specification and Verification of Interprocess Communication. | | In Formal Methods in Computer Aided Design (FMCAD) 2010, | | IEEE, 2010. | | Note: to appear | | | | Alkassar, E. and Bogan, S. and Paul, W. |
|
EE |
BibTeX |
| Proving the Correctness of Client/Server Software. | | In Sadhana Journal, | | pages 145-192, Springer, 2009. | | | | 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 | | | | Alkassar, Eyad |
|
|
BibTeX |
| OS Veri cation Extended - On the Formal Veri cation of Device Drivers and the Correctness of Client/Server Software. | | | Dissertation, University of Saarland, 2009. | | | | 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. | | | | Alkassar, Eyad and Schirmer, Norbert and Starostin, Artem |
|
EE |
BibTeX |
| Formal Pervasive Verification of a Paging Mechanism. | | In C. R. Ramakrishnan and Jakob Rehof, editors, 14th intl Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08), | | volume 4963 of LNCS, pages 109-123, Springer, 2008. | | | | Tverdyshev, S. and Alkassar, E. |
|
EE |
BibTeX |
| Efficient Bit-Level Model Reductions for Automated Hardware Verification. | | In Stéphane Demri and Christian S. Jensen, editors, 15th International Symposium on Temporal Representation and Reasoning: TIME2008, | | pages pp. 164-172, IEEE Computer Society Press, 2008. | | | | Alkassar, Eyad and Böhm, Peter and Knapp, Steffen |
|
EE |
BibTeX |
| Formal Correctness of a Gate-Level Automotive Bus Controller Implementation. | | In Bernd Kleinjohann and Lisa Kleinjohann and Wayne Wolf, editors, 6th IFIP Working Conference on Distributed and Parallel Embedded Systems (DIPES08), | | pages 57-68, Springer, 2008. | | | | Alkassar, Eyad and Böhm, Peter and Knapp, Steffen |
|
EE |
BibTeX |
| Correctness of a Fault-Tolerant Real-Time Scheduler Algorithm and its Hardware Implementation. | | In Formal Methods and Models for Codesign (MEMOCODE'2008), | | pages 175--186, IEEE Computer Society Press, 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. | | | | Alkassar, Eyad and Hillebrand, Mark A. |
|
EE |
BibTeX |
| Formal Functional Verification of Device Drivers. | | 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 225--239, Springer, 2008. | | | | Alkassar, E. and Hillebrand, M. and Knapp, S. and Rusev, R. and Tverdyshev, S. |
|
EE |
BibTeX |
| Formal Device and Programming Model for a Serial Interface. | | In B. Beckert, editors, Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany, | | pages 4--20, CEUR-WS Workshop Proceedings, 2007. | | | | Alkassar, Eyad |
|
|
BibTeX |
| Constructing a Formal Framework for Modeling and Verifying a Real Operating System. | | | Masterarbeit, Universität des Saarlandes, 2005. | | |
|
