Education

1/2002 - 6/2005		Ph.D. degree in Computer Science with a minor in Mathematics, Department of Computer Science, Wayne State University, Detroit, Michigan. Advisor: Frank Stomp. Research area: Formal Methods and Verification of Software (GPA: 3.93)
9/1999 - 12/2001		M.A. degree in Computer Science, Department of Computer Science, Wayne State University, Detroit, Michigan. Advisor: Frank Stomp. Research area: Formal Methods and Verification of Software (GPA: 3.92)
9/1997 - 8/1999		Doctoral (RNDr.) degree in Computer Science, Charles University, Prague, Czech Republic. Advisor: Frantisek Plasil. Research area: Object-Oriented Paradigms in Distributed Environments (GPA: N/A)
6/1994 - 5/1996		Master's (Mgr.) degree, with honors, in Computer Science, Palacky University, Olomouc, Czech Republic. Advisor: Vladimir Sklenar. Research area: Abstract Data Views (GPA: 4.0)
9/1991 - 5/1994		Bachelor's (Bc.) degree in Computer Science, Palacky University, Olomouc, Czech Republic. (GPA: 3.96)

Skills Summary

	Experience in design and development of core infrastructure systems, and in management of a team and a project
	Extensive background in Formal Methods including experience in applications of Linear-Time Temporal Logic, analysis of concurrent and distributed algorithms, development of formal correctness proofs, mechanization of proofs using the PVS theorem prover, and software verification using the SPARK proof checker and the SPIN verification system
	Ability to conduct independent research, to publish research papers in journals and conference proceedings, and to present results at international conferences and seminars
	Proficiency in software development using several programming languages including C++, Java, and Delphi; in using UML and Rational Rose; in applications of object-oriented and component-based technologies including CORBA, DCOM, and web-based technologies including HTML, JavaScript, and Java servlets; in design and use of a formal specification language for description of component software
	Practical experience in management of Windows, Unix/Linux, and Novell NetWare systems; in programming using Basic, Pascal, Lisp, Scheme, ML, Prolog, Smalltalk, Assembler x86; in applications of many software packages including Microsoft Office, WordPerfect Suite, LaTeX, Paradox, Btrieve, Mathematica
	Experience in teaching computer science courses including discrete mathematics, data structures and algorithms, programming, and formal languages and automata; in preparation, presentation, evaluation and grading; in leading and advising teaching assistants
	Fluent in Czech (native), English, and Russian; basics in German and Spanish

Service

	Member of IEEE Computer Society
	Member of Association for Computing Machinery
	Referee for the 10th IEEE International Conference on Engineering of Complex Computer Systems
	Referee for the 2004 International Symposium on Computer and Information Sciences
	Elected representative of Computer Science graduate students (2000 - 2001)
	Member of the organizational committee of the Objects '97 conference

Honors/Awards

	WSU Department of Computer Science research assistantship award (2003 - 2004)
	WSU Department of Computer Science nomination for the 2003 Garrett T. Heberlein Endowed Award for Excellence in Teaching for Graduate Students (2003)
	WSU Graduate School conference travel award (2002)
	WSU Graduate School tuition award (1999 - 2003)
	Palacky University College of Sciences Dean's award for an outstanding student project in Computer Science (1996)
	Palacky University College of Sciences scholarship for excellent students (1993 - 1996)

Work Experience

10/2005 - present		Staff Software Engineer, Google Inc., New York, NY. Leading design and implementation of core infrastructure systems supporting distributed storage of data
9/2004 - 8/2005		Lecturer, Department of Computer Science, Wayne State University, Detroit, MI. Teaching Discrete Structures in Computer Science, C++ Programming, Data Structures, Formal Languages and Grammars; Advising undergraduate students
9/2003 - 8/2004		Graduate Research Assistant, Department of Computer Science, Wayne State University, Detroit, MI. Conducting research in the area of formal software verification, focusing on verification of distributed algorithms using Linear-Time Temporal Logic, and on proof mechanization using PVS theorem prover
9/2003 - 8/2004		Graduate Teaching Consultant, Office for Teaching and Learning, Wayne State University, Detroit, MI. Advising teaching assistants; responsible for scheduling and management of class observations, videotaping lectures, interviewing students, and interviewing and debriefing teaching assistants
5/2002 - 8/2003		Graduate Teaching Assistant, Department of Computer Science, Wayne State University, Detroit, MI. Lecturer of Formal Languages and Automata, Data Structures and Algorithms Analysis; responsible for course design, preparation, teaching, evaluation, and grading
1/2001 - 4/2002		Graduate Teaching Assistant, Department of Computer Science and Engineering, Oakland University, Rochester, MI. Lecturer of Discrete Structures and Foundations of Computer Science, C++ Programming and Data Structures; responsible for course design, preparation, teaching, evaluation, and grading
9/1999 - 12/2000		Graduate Teaching Assistant, Department of Computer Science, Wayne State University, Detroit, MI. Lecturer of Operating Systems and C++ Programming; responsible for course design, preparation, teaching, evaluation, and grading
1/1999 - 8/1999		Researcher, Institute of Computer Science, Czech Academy of Sciences, Prague, Czech Republic; Conducting research in Component and Object-Oriented Methodologies
9/1998 - 8/1999		Teaching Assistant, Department of Software Engineering, Charles University, Prague. Leading lab sessions in Object-Oriented Technologies and Operating Systems; responsible for lab preparation, teaching, evaluation, and grading
6/1996 - 8/1998		Lead Developer of a suite of public transportation applications Client: FS Software, Olomouc, Czech Republic; suite used in 30 major cities Project: FS Mapa ("FS Maps") Description: An application for tracking positions of public transportation vehicles via GPS; 40 KLOC in Delphi; lead developer and designer Project: FS Rady ("FS Schedules") Description: An application for designing, generating and printing schedules for public transportation systems; 90 KLOC in Delphi; lead developer and designer Project: Btrieve for Delphi Description: A component supporting seamless integration of Btrieve databases in Delphi; 25 KLOC in Delphi; 10 KLOC in C++; integration of Delphi, C++, and Btrieve components; lead developer and designer Project: FS Spoje ("FS Connections") Description: An application for finding connections in transportation schedules; 30 KLOC in Java; web-based (Java Servlet) application; interoperability with other applications in the FS Software suite; lead developer and designer
9/1996 - 3/1998		System administrator of Windows NT and Novell Netware networks, Department of Computer Science, Palacky University, Czech Republic. Setup and maintenance including management of IIS and Exchange servers, user accounts, shared printers, shared software, resolving network problems
9/1995 - 12/1997		Teaching Assistant, Department of Computer Science, Palacky University, Olomouc, Czech Republic. Lecturer of Programming in C++, Programming in Java, Object-Oriented Programming, and Programming for the Win32 Platform; responsible for course design, preparation, teaching, evaluation, and grading
9/1994 - 5/1996		Team Manager and Lead Developer, Palacky University, Czech Republic Client: Palacky University, Olomouc, Czech Republic Project: Alvis ("Algorithm Visualization") Description: An application for visualization of algorithms; 500 KLOC in C++; Manager of a team of 12 student programmers and a lead developer implementing the core functionality of the system
9/1992 - 8/1996		System administrator of Novell NetWare network, GJO high school, Litovel, Czech Republic. Setup and maintenance of network, accounts, printers, resolving problems
9/1992 - 6/1996		Teacher, GJO high school, Litovel, Czech Republic. Teaching Programming in Pascal; responsible for class design, teaching, evaluation, and grading

References
    Available upon request

Publications
    Available here