Nikolaj S. Bjørner

Ph.D., Computer Science

e-mail: nikolaj@cs.stanford.edu

CV/Resume

Research interests

Integration of Decision Procedures in Temporal Verification.

Temporal logics for synthesis and verification of reactive, concurrent, real-time, and hybrid systems.

Type inference of polymorphic typed languages.

Papers

Nikolaj Bjørner and César Muñoz Absolute Explicit Unification RTA 2000.

John Anton, Nikolaj Bjorner, and Johan Gunnarsson. Railway control design by combining Specware and Mathematica To appear in The Sandia conference on High Integrity Software, November 14-17, 1999, New Mexico.

Nikolaj Bjørner. Type checking meta programs Appeared in the workshop on Logical Frameworks and Meta-languages 28 September 1999, Paris, France.

Nikolaj Bjørner. Integrating Decision Procedures for Temporal Verification. Slightly revised version of my Thesis, November 1998.

Nikolaj Bjørner. Reactive Verification with Queues. In proceedings of Engineering Automation for Computer Based Systems. Carmel October, 1998.

Zohar Manna and the STeP group. An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. In TOOLS'98, LNCS.

Nikolaj Bjørner and Mark Pichora. Deciding Fixed and Nonfixed-size Bit-vectors. A shorter version of this paper is to be presented at TACAS 98.

Nikolaj Bjørner, Zohar Manna and Uri Lerner. Deductive verification of parameterized fault-tolerant systems: A case study. Presented at ICTL 97.

Nikolaj Bjørner, Mark Stickel and Tomás E. Uribe. A practical integration of first-order reasoning and decision procedures. Presented at CADE 97. See also the demo page.

Nikolaj Bjørner, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Deductive Verification of Real-time Systems Using STeP . Presented at ARTS 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. This paper is a revised version of Automatic Generation of Invariants and Intermediate Assertions which appeared in 1st International Conference on Principles and Practice of Constraint Programming, Lecture Notes in Computer Science 976, Cassis, France (September 1995), pp. 589-623. The two versions contain different examples and treat different abstraction domains.

Zohar Manna and the STeP group. STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems. In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 415-418, Springer-Verlag, 1996. 4-page description.

Nikolaj Bjørner, Anca Browne, Eddie Chang, Michael Colon, Arjun Kapur, Zohar Manna, Henny Sipma, Tomas Uribe. STeP: The Stanford Temporal Prover Educational Release, User's Manual.

The STeP group. STeP: The Stanford Temporal Prover (2-page abstract). In TAPSOFT'95: Theory and Practice of Software Development, Lecture Notes in Computer Science 915, May 1995, pp. 793-794.

Nikolaj Bjørner Minimal Typing Deriviations. Workshop on ML and its applications. Orlando 94. Full paper.

The STeP group. STeP: The Stanford Temporal Prover. Technical report STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994.

Slides

Nikolaj Bjørner. An overview of Synthesis Presented at a DIMACS 96 workshop March 25-28 1996. A one page abstract will appear in a DIMACS technical report.

Nikolaj S. Bjorner