Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Nikolaj Bjorner

Nikolaj Bjorner

I work with Leonardo de Moura and Christoph Wintersteiger on a state-of-the-art SMT constraint solver Z3.  Z3 is used for program verification and test case generation. I also work with Karthick Jayaraman from Azure on validating firewalls using Z3. Until 2006, I was in the Core File Systems group where I designed and implemented the core of DFS-R which is included as part of Windows Server 2003 R2, Windows Live Messenger (Sharing Folders), and Vista Meetings Space. I also designed some of the chunking utilities used in the remote differential compression protocol RDC.


Recent Papers and Reports

Conferences and workshops 

  • ICDCIT 2015 (invited speaker)
  • Dagstuhl seminar on Formal Foundations of Networking (co-organizer)
  • FM 2015 (PC co-chair)
  • QUANTIFY @ CADE 2015 (PC)
  • ICFEM 2015 (PC)
  • TASE 2015 (PC)
  • FMCAD 2015 (PC)
  • Dagstuhl seminar on Deduction: Extracting Information from Deduction, Models and Proofs. (co-organizer)
  • ICDCIT 2016 (PC co-chair)



Old workshops and conferences

        notes on SMT and Verification