CURRICULUM VITAE
Nikolaj S.
Bjørner Ph.D.
e-mail: nikolaj@cs.stanford.edu
http://theory.stanford.edu/~nikolaj
OBJECTIVE:
To design and implement the sexiest systems.
EXPERIENCE:
- 2002 - Microsoft
XDegrees merged with another company, but their ticker symbol is still MSFT.
We are now working with the Core File Systems group.
- 2000 - 2002 XDegrees:
As a first employee bootstrapped the software development.
Assumed leadership roles in the design and implementation of a
system for scalable peer-to-peer resource
sharing including an extensible resource naming service, together with
SOAP and WebDAV extensions of HTTP server and proxy interfaces.
Co-author of two pending patents on
the naming system protocols and its security aspects.
- 1998 - 2000 Kestrel Institute:
Designed and implemented a bootstrapped
specification based-program transformation
system for an algebraic/functional language using polymorphic
types and reflection.
Participated in DARPA and NSA sponsored projects on
program transformation, integration of verification systems,
design of embedded systems, and high performance knowledge bases.
Took on existing programs and assumed leadership responsibilities,
was awarded new contracts on embedded system design.
EDUCATION:
- 1994-1998: Ph.D.. student at Stanford University, Computer Science.
- 1992-1994: MsSc student at Stanford University, Computer Science
- 1990-1992: 5 additional courses taken at Copenhagen University Computer
Science (DIKU).
- 1989-1992: CS/EE student at the Danish Technical University (DTU)
- 1989 High school diploma.
DISSERTATION:
Integration of Decision Procedures in Temporal
Verification. Thesis advisor: Professor Zohar Manna.
The dissertation
proposes novel algorithms for resolving constraints on data-types that are
commonly used in software and hardware. A powerful framework allowing modular
and efficient integration with expressive extensions is used to glue the various
components. The algorithms are used for establishing temporal properties (time
dependent) of concurrent, reactive, and hybrid systems. The procedures are
part of STeP (Stanford Temporal Prover:
www-step.stanford.edu)
tool, written
in well over 100,000 lines academic strength C, ML and Java. STeP has been
distributed in around 150 licensed copies in industry and academia.
TEACHING:
Formal Methods for Concurrent and Reactive Systems (1996),
Logic and automated reasoning (1995), Automata Theory (1995), Logic and
automated reasoning (1993), Graph Theory (1992), Group Theory (1992),
Combinatorics (1991), Error correcting codes (1991), Graph Theory (1990).
BUZZ WORDS:
C, C++, SML, Ocaml, Java, LISP, Python, Perl, Pascal, Prolog,
Shell programming, Shell extensions, MIDL, RPC,
Lex, yacc, XML, SOAP, HTML, HTTP, DNS, TCP/IP, UDP, IP4(+2),
AES, TLS, SSL, Kerberos, Model checking, Decision procedures,
Type inference, Static program analysis, Solaris, Linux, Windows.
SELECTED PAPERS:
- Nikolaj Bjørner and César Muñoz
Absolute Explicit Unification
RTA 2000.
- Nikolaj Bjørner and Mark Pichora. Deciding Fixed
and Nonfixed-size Bit-vectors. TACAS 98.
- Nikolaj Bjørner, Zohar Manna and Uri Lerner. Deductive
verification of parameterized fault-tolerant systems: A case study.
ICTL 97.
- Nikolaj Bjørner, Mark Stickel and Tomás E. Uribe. A practical
integration of first-order reasoning and decision procedures. CADE 97.
- Nikolaj Bjørner, Anca Browne and Zohar Manna. Automatic
Generation of Invariants and Intermediate Assertions. This appeared in the
February 97 issue of Theoretical Computer Science dedicated to CP'95. It is a
much reworked revision of the paper appearing in CP'95.
- Nikolaj Bjørner Minimal Typing
Derivations. Workshop on ML and its applications. Orlando 94.
- The STeP group. STeP: The
Stanford Temporal Prover. Technical report STAN-CS-TR-94-1518, Computer
Science Department, Stanford University, July 1994.
- More papers available at http://theory.stanford.edu/~nikolaj
OTHER ACTIVITIES:
- Summer exchange student at Joint Venture Dialogue, Moscow, July 1991.
- Assistant researcher, Stanford January-June 1994.
- Visitor at Intel research laboratories, Haifa, September 1995.
- Invited lecture: An overview of Synthesis of
Reactive Systems. Presented at a DIMACS workshop New Brunswick, March
25-28 1996
- Invited course: An introduction to
STeP. Presented at a three day course at University of Indonesia,
Jakarta, July 21-24, 1997
- Workshop talk: Decision procedures for hardware verification. Technion,
Haifa, March 20-21, 1998
HONORS AND AWARDS:
The following awards helped completing my Master's
degree at Stanford: The Simon Spies Honorary award for Young Researchers (one
given every year), 100,000 DKr.
Otto Mønsteds Fond 10,000 DKr.
Reiholdt W. Jorck og Hustrus Fond 6,000 DKr.
Toyota Fonden 20,000 DKr.
Knud Højgårds Fond. 25,000 DKr.
Travel grant from The Danish Ministry of Education 10,000 DKr.
United Nations University employee scholarship, 8,250 US$ .
US
citizenship. Diplomas and references available upon request.