Nikolaj S. Bjørner Ph.D.


To design and implement the sexiest systems.




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: 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.


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).


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.


  1. Nikolaj Bjørner and César Muñoz Absolute Explicit Unification RTA 2000.
  2. Nikolaj Bjørner and Mark Pichora. Deciding Fixed and Nonfixed-size Bit-vectors.  TACAS 98.
  3. Nikolaj Bjørner, Zohar Manna and Uri Lerner. Deductive verification of parameterized fault-tolerant systems: A case study. ICTL 97.
  4. Nikolaj Bjørner, Mark Stickel and Toms E. Uribe. A practical integration of first-order reasoning and decision procedures. CADE 97.
  5. 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.
  6. Nikolaj Bjørner Minimal Typing Derivations. Workshop on ML and its applications. Orlando 94.
  7. The STeP group. STeP: The Stanford Temporal Prover. Technical report STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994.
  8. More papers available at



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øjgrds 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.