Institut für Rechnerarchitektur
und Parallelrechner
Dr. Sergey Tverdyshev
Universität des Saarlandes   Gebäude E1 3
FR 6.2 Informatik   Raum 307
Postfach 151150   Tel: +49 (0)681 302-64713
D-66041 Saarbrücken   Fax: +49 (0)681 302-4290
Germany   eMail:
1981 geboren
1997 Mittelschule 36, Khabarovsk, Russland
1997 - 2002 Diplom mit Auszeichnung "Ingenieur - Systemtechiker" in der Fachrichtung "Steuerung und Informatik in der technische Systeme" vom Staatliche Technische Universitat Khabarowsk, Russland
2001 - 2003 M.Sc. mit 1.6 (A-) von der Universitaet des Saarlandes, Saarbruecken
2003 Wiisenschaftliche Mitarbeit im Forschungsprojekt Verisoft
Formale Verifikation von Hardware und Software
Private Homepage
Baumann, C. and Blasum, H. and Bormer, T. and Tverdyshev, S.   BibTeX
Proving Memory Separation in a Microkernel by Code Level Verification.
In Wilfried Steiner and Roman Obermaisser, editors, 1st International Workshop on Architectures and Applications for Mixed-Criticality Systems (AMICS 2011),
Newport Beach, CA, USA
IEEE Computer Society, 2011.
Note: Verified Code Sources:
Endres, E. and Muller, C. and Shadrin, A. and Tverdyshev, S.   EE BibTeX
Towards the Formal Verification of a Distributed Real-Time Automotive System.
In Cesar Munoz, editors, Second NASA Formal Methods Symposium NFM 2010,
pages 212-217, NASA, 2010.
unpublished, available at
Hillebrand, M. and Tverdyshev, S.   EE BibTeX
Formal Verification of Gate-Level Computer Systems.
In A. Morozov, K. Wagner, A. Rybalchenko, and A. Frid., editors, 4th International Computer Science Symposium in Russia,
volume 5675 of LNCS, pages 322-333, Springer, 2009.
Tverdyshev, Sergey   BibTeX
Formal Verification of Gate-Level Computer Systems.
Dissertation, Saarland University, Computer Science Department, 2009.
Tverdyshev, Sergey   EE BibTeX
A Verified Platform for a Gate-Level Electronic Control Unit.
In Formal Methods in Computer Aided Design, FMCAD'09,
IEEE, pages 164-171, IEEE, 2009.
ISBN 978-1-4244-4966
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.
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.
Tverdyshev, S. and Shadrin, A.   EE BibTeX
Formal Verification of Gate-Level Computer Systems (short paper).
In Kristin Yvonne Rozier, editors, LFM 2008,
NASA Scientific and Technical Information (STI), pages 56-58, NASA, 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.
Tverdyshev, Sergey EE BibTeX
Combination of Isabelle/HOL with Automatic Tools.
In Bernhard Gramlich, editors, FroCoS 2005,
volume 3717 of Lecture Notes in Computer Science, pages 302-309, Springer Verlag, 2005.
ISBN 3-540-29051-6
Tverdyshev, Sergey   BibTeX
Documentation and Modelling of the IPC Mechanism in the L4 Kernel.
Diplomarbeit, Saarland University, 2003.