Nikolaj Bjørner

Nikolaj Bjørner, Viorica Sofronie-Stokkermans: Preface: Special Issue of Selected Extended Papers of CADE-23. J. Autom. Reasoning 51(1): 1-2 (2013)

Nikolaj Bjørner, Laura Kovács: Foreword. J. Symb. Comput. 47(12): 1413-1415 (2012)

Margus Veanes, Nikolaj Bjørner: Alternating simulation and IOCO. STTT 14(4): 387-405 (2012)

Nikolaj Bjørner, Guido de Caso, Yuri Gurevich: From Primal Infon Logic with Individual Variables to Datalog. Correct Reasoning 2012: 72-86

Nikolaj Bjørner: Taking Satisfiability to the Next Level with Z3 - (Abstract). IJCAR 2012: 1-8

Moshe Gabel, Assaf Schuster, Ran-Gilad Bachrach, Nikolaj Bjørner: Latent fault detection in large scale services. DSN 2012: 1-12

Ethan K. Jackson, Wolfram Schulte, Nikolaj Bjørner: Detecting Specification Errors in Declarative Languages with Constraints. MoDELS 2012: 399-414

Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj Bjørner: Symbolic finite state transducers: algorithms and applications. POPL 2012: 137-150

Krystof Hoder, Nikolaj Bjørner: Generalized Property Directed Reachability. SAT 2012: 157-171

Thomas Ball, Nikolaj Bjørner, Leonardo Mendonça de Moura, Kenneth L. McMillan, Margus Veanes: Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials. SPIN 2012: 1-6

Margus Veanes, Nikolaj Bjørner: Symbolic Automata: The Toolkit. TACAS 2012: 472-477

Nikolaj Bjørner, Andrei Voronkov (Eds.): Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings. Lecture Notes in Computer Science 7180, Springer 2012, isbn 978-3-642-28716-9

Nikolaj Bjørner, Krishnendu Chatterjee, Laura Kovács, Rupak Majumdar: Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). Dagstuhl Reports 2(11): 45-65 (2012)

Leonardo Mendonça de Moura, Nikolaj Bjørner: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9): 69-77 (2011)

Margus Veanes, Nikolaj Bjørner: Foundations of Finite Symbolic Tree Transducers. Bulletin of the EATCS 105: 141-173 (2011)

Nikolaj Bjørner: Engineering Theories with Z3. APLAS 2011: 4-16

Krystof Hoder, Nikolaj Bjørner, Leonardo Mendonça de Moura: μZ- An Efficient Engine for Fixed Points with Constraints. CAV 2011: 457-462

Nikolaj Bjørner: Engineering Theories with Z3. CPP 2011: 1-2

Margus Veanes, Nikolaj Bjørner: Symbolic Tree Transducers. Ershov Memorial Conference 2011: 377-393

Ethan K. Jackson, Nikolaj Bjørner, Wolfram Schulte: Canonical Regular Types. ICLP (Technical Communications) 2011: 73-83

Nikolaj Bjørner, Viorica Sofronie-Stokkermans (Eds.): Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings. Lecture Notes in Computer Science 6803, Springer 2011, isbn 978-3-642-22437-9

Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov: Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports 1(7): 23-35 (2011)

Ruzica Piskac, Leonardo Mendonça de Moura, Nikolaj Bjørner: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reasoning 44(4): 401-424 (2010)

Nikolaj Bjørner, Andreas Blass, Yuri Gurevich: Content-dependent chunking for differential compression, the local maximum approach. J. Comput. Syst. Sci. 76(3-4): 154-203 (2010)

Sergio Mera, Nikolaj Bjørner: DKAL and Z3: A Logic Embedding Experiment. Fields of Logic and Computation 2010: 504-528

Nikolaj Bjørner: Linear Quantifier Elimination as an Abstract Decision Procedure. IJCAR 2010: 316-330

Leonardo Mendonça de Moura, Nikolaj Bjørner: Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. IJCAR 2010: 400-411

Margus Veanes, Nikolaj Bjørner, Leonardo Mendonça de Moura: Symbolic Automata Constraint Solving. LPAR (Yogyakarta) 2010: 640-654

Margus Veanes, Nikolaj Bjørner: Alternating Simulation and IOCO. ICTSS 2010: 47-62

Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte: Symbolic Bounded Model Checking of Abstract State Machines. Int. J. Software and Informatics 3(2-3): 149-170 (2009)

Nikolaj Bjørner, Joe Hendrix: Linear Functional Fixed-points. CAV 2009: 124-139

Margus Veanes, Nikolaj Bjørner: Symbolic Bounded Conformance Checking of Model Programs. Ershov Memorial Conference 2009: 388-400

Leonardo Mendonça de Moura, Nikolaj Bjørner: Generalized, efficient array decision procedures. FMCAD 2009: 45-52

Nikolaj Bjørner, Leonardo Mendonça de Moura: Tapas: Theory Combinations and Practical Applications. FORMATS 2009: 1-6

Margus Veanes, Nikolaj Bjørner: Input-Output Model Programs. ICTAC 2009: 322-335

Leonardo Mendonça de Moura, Nikolaj Bjørner: Satisfiability Modulo Theories: An Appetizer. SBMF 2009: 23-36

Ethan K. Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte: Specifying and Composing Non-functional Requirements in Model-Based Development. Software Composition 2009: 72-89

Nikolaj Bjørner: SMT Solvers for Testing, Program Analysis and Verification at Microsoft. SYNASC 2009: 15

Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov: Path Feasibility Analysis for String-Manipulating Programs. TACAS 2009: 307-321

Leonardo Mendonça de Moura, Nikolaj Bjørner: Model-based Theory Combination. Electr. Notes Theor. Comput. Sci. 198(2): 37-49 (2008)

Leonardo Mendonça de Moura, Nikolaj Bjørner: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. IJCAR 2008: 410-425

Leonardo Mendonça de Moura, Nikolaj Bjørner: Engineering DPLL(T) + Saturation. IJCAR 2008: 475-490

Margus Veanes, Nikolaj Bjørner, Alexander Raschke: An SMT Approach to Bounded Reachability Analysis of Model Programs. FORTE 2008: 53-68

Leonardo Mendonça de Moura, Nikolaj Bjørner: Proofs and Refutations, and Z3. LPAR Workshops 2008

Dries Vanoverberghe, Nikolaj Bjørner, Jonathan de Halleux, Wolfram Schulte, Nikolai Tillmann: Using Dynamic Symbolic Execution to Improve Deductive Verification. SPIN 2008: 9-25

Leonardo Mendonça de Moura, Nikolaj Bjørner: Z3: An Efficient SMT Solver. TACAS 2008: 337-340

Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi: Modular difference logic is hard. CoRR abs/0811.0987 (2008)

Nikolaj Bjørner: Models and Software Model Checking of a Distributed File Replication System. Formal Methods and Hybrid Real-Time Systems 2007: 1-23

Leonardo Mendonça de Moura, Nikolaj Bjørner: Efficient E-Matching for SMT Solvers. CADE 2007: 183-198

Nikolaj Bjørner, Zohar Manna, Henny Sipma, Tomás E. Uribe: Deductive verification of real-time systems using STeP. Theor. Comput. Sci. 253(1): 27-60 (2001)

Nikolaj Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomás E. Uribe: Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods in System Design 16(3): 227-270 (2000)

Nikolaj Bjørner, César Muñoz: Absolute Explicit Unification. RTA 2000: 31-46

Nikolaj Bjørner, Mark C. Pichora: Deiding Fixed and Non-fixed Size Bit-vectors. TACAS 1998: 376-392

Nikolaj Bjørner, Anca Browne, Zohar Manna: Automatic Generation of Invariants and Intermediate Assertions. Theor. Comput. Sci. 173(1): 49-87 (1997)

Nikolaj Bjørner, Zohar Manna, Henny Sipma, Tomás E. Uribe: Deductive Verification of Real-Time Systems Using STeP. ARTS 1997: 22-43

Nikolaj Bjørner, Mark E. Stickel, Tomás E. Uribe: A Practical Integration of First-Order Reasoning and Decision Procedures. CADE 1997: 101-115

Nikolaj Bjørner, Anca Browne, Edward Y. Chang, Michael Colón, Arjun Kapur, Zohar Manna, Henny Sipma, Tomás E. Uribe: STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. CAV 1996: 415-418

Nikolaj Bjørner, Anca Browne, Zohar Manna: Automatic Generation of Invariants and Assertions. CP 1995: 589-623

Zohar Manna, Nikolaj Bjørner, Anca Browne, Edward Y. Chang, Michael Colón, Luca de Alfaro, Harish Devarajan, Arjun Kapur, Jaejin Lee, Henny Sipma, Tomás E. Uribe: STeP: The Stanford Temporal Prover. TAPSOFT 1995: 793-794