×

zbMATH — the first resource for mathematics

Bjørner, Nikolaj S.

Compute Distance To:
Author ID: bjorner.nikolaj-s Recent zbMATH articles by "Bjørner, Nikolaj S."
Published as: Bjorner, Nikolaj; Bjørner, N.; Bjørner, N. S.; Bjørner, Nikolaj; Bjørner, Nikolaj S.
Documents Indexed: 50 Publications since 1997, including 5 Books

Publications by Year

Citations contained in zbMATH Open

33 Publications have been cited 203 times in 157 Documents Cited by Year
Efficient E-matching for SMT solvers. Zbl 1213.68578
de Moura, Leonardo; Bjørner, Nikolaj
36
2007
Generalized property directed reachability. Zbl 1273.68229
Hoder, Kryštof; Bjørner, Nikolaj
20
2012
Model-based theory combination. Zbl 1277.03007
de Moura, Leonardo; Bjørner, Nikolaj
16
2008
Engineering DPLL(T) + saturation. Zbl 1165.68479
de Moura, Leonardo; Bjørner, Nikolaj
15
2008
Symbolic finite state transducers: algorithms and applications. Zbl 1321.68341
Veanes, Margus; Hooimeijer, Pieter; Livshits, Benjamin; Molnar, David; Bjorner, Nikolaj
13
2012
Deciding effectively propositional logic using DPLL and substitution sets. Zbl 1197.03011
Piskac, Ruzica; de Moura, Leonardo; Bjørner, Nikolaj
10
2010
Automatic generation of invariants and intermediate assertions. Zbl 0902.68120
Bjørner, Nikolaj; Browne, Anca; Manna, Zohar
10
1997
Path feasibility analysis for string-manipulating programs. Zbl 1234.68070
Bjørner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei
9
2009
Symbolic automata constraint solving. Zbl 1306.68097
Veanes, Margus; Bjørner, Nikolaj; de Moura, Leonardo
7
2010
Linear quantifier elimination as an abstract decision procedure. Zbl 1291.68325
Bjørner, Nikolaj
7
2010
Deciding effectively propositional logic using DPLL and substitution sets. Zbl 1165.03320
de Moura, Leonardo; Bjørner, Nikolaj
7
2008
Property-directed inference of universal invariants or proving their absence. Zbl 1381.68169
Karbyshev, A.; Bjørner, N.; Itzhaky, S.; Rinetzky, N.; Shoham, S.
6
2015
Horn clause solvers for program verification. Zbl 06484064
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey
6
2015
Satisfiability modulo theories: an appetizer. Zbl 1266.03047
de Moura, Leonardo; Bjørner, Nikolaj
5
2009
Symbolic automata: the toolkit. Zbl 1352.68138
Veanes, Margus; Bjørner, Nikolaj
4
2012
Bugs, moles and skeletons: symbolic reasoning for software development. Zbl 1291.68377
de Moura, Leonardo; Bjørner, Nikolaj
4
2010
Property directed polyhedral abstraction. Zbl 1432.68257
Bjørner, Nikolaj; Gurfinkel, Arie
3
2015
Taking satisfiability to the next level with Z3 (abstract). Zbl 1358.68248
Bjørner, Nikolaj
3
2012
Foundations of finite symbolic tree transducers. Zbl 1257.68100
Veanes, Margus; Bjørner, Nikolaj
3
2011
Monadic decomposition. Zbl 1426.03026
Veanes, Margus; Bjørner, Nikolaj; Nachmanson, Lev; Bereg, Sergey
2
2017
Symbolic tree automata. Zbl 1317.68103
Veanes, Margus; Bjørner, Nikolaj
2
2015
Computing all implied equalities via SMT-based partition refinement. Zbl 1423.68408
Berdine, Josh; Bjørner, Nikolaj
2
2014
Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Zbl 1218.68006
Bjørner, Nikolaj (ed.); Sofronie-Stokkermans, Viorica (ed.)
2
2011
Deductive verification of real-time systems using STeP. Zbl 0954.68084
Bjørner, N. S.; Manna, Z.; Sipma, H. B.; Uribe, T. E.
2
2001
Scaling network verification using symmetry and surgery. Zbl 1347.68237
Plotkin, Gordon D.; Bjørner, Nikolaj; Lopes, Nuno P.; Rybalchenko, Andrey; Varghese, George
1
2016
Resourceful reachability as HORN-LA. Zbl 1406.68049
Berdine, Josh; Bjørner, Nikolaj; Ishtiaq, Samin; Kriener, Jael E.; Wintersteiger, Christoph M.
1
2013
From primal infon logic with individual variables to Datalog. Zbl 1357.68212
Bjørner, Nikolaj; de Caso, Guido; Gurevich, Yuri
1
2012
Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Zbl 1238.68012
Bjørner, Nikolaj (ed.); Voronkov, Andrei (ed.)
1
2012
Content-dependent chunking for differential compression, the local maximum approach. Zbl 1201.68015
Bjørner, Nikolaj; Blass, Andreas; Gurevich, Yuri
1
2010
Symbolic bounded conformance checking of model programs. Zbl 1274.68082
Veanes, Margus; Bjørner, Nikolaj
1
2010
Input-output model programs. Zbl 1250.68198
Veanes, Margus; Bjørner, Nikolaj
1
2009
Linear functional fixed-points. Zbl 1242.68062
Bjørner, Nikolaj; Hendrix, Joe
1
2009
Models and software model checking of a distributed file replication system. Zbl 1151.68470
Bjørner, Nikolaj
1
2007
Monadic decomposition. Zbl 1426.03026
Veanes, Margus; Bjørner, Nikolaj; Nachmanson, Lev; Bereg, Sergey
2
2017
Scaling network verification using symmetry and surgery. Zbl 1347.68237
Plotkin, Gordon D.; Bjørner, Nikolaj; Lopes, Nuno P.; Rybalchenko, Andrey; Varghese, George
1
2016
Property-directed inference of universal invariants or proving their absence. Zbl 1381.68169
Karbyshev, A.; Bjørner, N.; Itzhaky, S.; Rinetzky, N.; Shoham, S.
6
2015
Horn clause solvers for program verification. Zbl 06484064
Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey
6
2015
Property directed polyhedral abstraction. Zbl 1432.68257
Bjørner, Nikolaj; Gurfinkel, Arie
3
2015
Symbolic tree automata. Zbl 1317.68103
Veanes, Margus; Bjørner, Nikolaj
2
2015
Computing all implied equalities via SMT-based partition refinement. Zbl 1423.68408
Berdine, Josh; Bjørner, Nikolaj
2
2014
Resourceful reachability as HORN-LA. Zbl 1406.68049
Berdine, Josh; Bjørner, Nikolaj; Ishtiaq, Samin; Kriener, Jael E.; Wintersteiger, Christoph M.
1
2013
Generalized property directed reachability. Zbl 1273.68229
Hoder, Kryštof; Bjørner, Nikolaj
20
2012
Symbolic finite state transducers: algorithms and applications. Zbl 1321.68341
Veanes, Margus; Hooimeijer, Pieter; Livshits, Benjamin; Molnar, David; Bjorner, Nikolaj
13
2012
Symbolic automata: the toolkit. Zbl 1352.68138
Veanes, Margus; Bjørner, Nikolaj
4
2012
Taking satisfiability to the next level with Z3 (abstract). Zbl 1358.68248
Bjørner, Nikolaj
3
2012
From primal infon logic with individual variables to Datalog. Zbl 1357.68212
Bjørner, Nikolaj; de Caso, Guido; Gurevich, Yuri
1
2012
Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Zbl 1238.68012
Bjørner, Nikolaj (ed.); Voronkov, Andrei (ed.)
1
2012
Foundations of finite symbolic tree transducers. Zbl 1257.68100
Veanes, Margus; Bjørner, Nikolaj
3
2011
Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Zbl 1218.68006
Bjørner, Nikolaj (ed.); Sofronie-Stokkermans, Viorica (ed.)
2
2011
Deciding effectively propositional logic using DPLL and substitution sets. Zbl 1197.03011
Piskac, Ruzica; de Moura, Leonardo; Bjørner, Nikolaj
10
2010
Symbolic automata constraint solving. Zbl 1306.68097
Veanes, Margus; Bjørner, Nikolaj; de Moura, Leonardo
7
2010
Linear quantifier elimination as an abstract decision procedure. Zbl 1291.68325
Bjørner, Nikolaj
7
2010
Bugs, moles and skeletons: symbolic reasoning for software development. Zbl 1291.68377
de Moura, Leonardo; Bjørner, Nikolaj
4
2010
Content-dependent chunking for differential compression, the local maximum approach. Zbl 1201.68015
Bjørner, Nikolaj; Blass, Andreas; Gurevich, Yuri
1
2010
Symbolic bounded conformance checking of model programs. Zbl 1274.68082
Veanes, Margus; Bjørner, Nikolaj
1
2010
Path feasibility analysis for string-manipulating programs. Zbl 1234.68070
Bjørner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei
9
2009
Satisfiability modulo theories: an appetizer. Zbl 1266.03047
de Moura, Leonardo; Bjørner, Nikolaj
5
2009
Input-output model programs. Zbl 1250.68198
Veanes, Margus; Bjørner, Nikolaj
1
2009
Linear functional fixed-points. Zbl 1242.68062
Bjørner, Nikolaj; Hendrix, Joe
1
2009
Model-based theory combination. Zbl 1277.03007
de Moura, Leonardo; Bjørner, Nikolaj
16
2008
Engineering DPLL(T) + saturation. Zbl 1165.68479
de Moura, Leonardo; Bjørner, Nikolaj
15
2008
Deciding effectively propositional logic using DPLL and substitution sets. Zbl 1165.03320
de Moura, Leonardo; Bjørner, Nikolaj
7
2008
Efficient E-matching for SMT solvers. Zbl 1213.68578
de Moura, Leonardo; Bjørner, Nikolaj
36
2007
Models and software model checking of a distributed file replication system. Zbl 1151.68470
Bjørner, Nikolaj
1
2007
Deductive verification of real-time systems using STeP. Zbl 0954.68084
Bjørner, N. S.; Manna, Z.; Sipma, H. B.; Uribe, T. E.
2
2001
Automatic generation of invariants and intermediate assertions. Zbl 0902.68120
Bjørner, Nikolaj; Browne, Anca; Manna, Zohar
10
1997
all top 5

Cited by 334 Authors

10 Reynolds, Andrew
8 Bonacina, Maria Paola
8 Tinelli, Cesare
7 Barrett, Clark W.
6 Bjørner, Nikolaj S.
6 Veanes, Margus
6 Weidenbach, Christoph
4 Cimatti, Alessandro
4 de Moura, Leonardo
4 Fontaine, Pascal
4 Ghilardi, Silvio
4 Kuncak, Viktor
3 Blanchette, Jasmin Christian
3 Echenim, Mnacho
3 Griggio, Alberto
3 Johansson, Moa
3 Lynch, Christopher A.
3 Peltier, Nicolas
3 Ranise, Silvio
3 Rümmer, Philipp
2 Brucker, Achim D.
2 Bruttomesso, Roberto
2 Bultan, Tevfik
2 Conchon, Sylvain
2 D’Antoni, Loris
2 De Oliveira, Diego Caminha B.
2 Déharbe, David
2 Deters, Morgan
2 Dross, Claire
2 Feldman, Yotam M. Y.
2 Garg, Pranav
2 Gurfinkel, Arie
2 Hansen, Michael Reichhardt
2 Ibarra, Oscar H.
2 Iosif, Radu
2 Jovanović, Dejan
2 Kesten, Yonit
2 Klebanov, Vladimir
2 Korovin, Konstantin
2 Kruglov, Evgeniĭ Valentinovich
2 Liang, Tianyi
2 Löding, Christof
2 Madhusudan, Parthasarathy
2 Manna, Zohar
2 Neider, Daniel
2 Nicolini, Enrica
2 Oe, Duckki
2 Padon, Oded
2 Phan, Anh-Dung
2 Piskac, Ruzica
2 Plaisted, David Alan
2 Pnueli, Amir
2 Ringeissen, Christophe
2 Roveri, Marco
2 Rusinowitch, Michaël
2 Sagiv, Mooly
2 Sánchez, César
2 Sebastiani, Roberto
2 Shoham, Sharon
2 Sipma, Henny B.
2 Stump, Aaron
2 Tribastone, Mirco
2 Tsiskaridze, Nestan
2 Ulbrich, Mattias
2 Vandin, Andrea
2 Vogler, Heiko
2 Wolff, Burkhart
2 Yu, Fang
2 Zhan, Bohua
1 Aarts, Fides
1 Ábrahám, Erika
1 Abujarad, Fuad
1 Aiken, Alex
1 Alagi, Gábor
1 Alberti, Francesco
1 Alkhalaf, Muath
1 Althaus, Ernst
1 Alur, Rajeev
1 Aravantinos, Vincent
1 Areces, Carlos
1 Aschermann, Cornelius
1 Avigad, Jeremy
1 Banerjee, Anindya
1 Bantegui, Michael
1 Barbosa, Haniel
1 Bardin, Sébastien
1 Bartocci, Ezio
1 Baumgartner, Peter
1 Beldiceanu, Nicolas
1 Berglund, Martin
1 Berzish, Murphy
1 Besson, Frédéric
1 Bester, Willem
1 Beyer, Dirk
1 Bhattacharyya, Arnab
1 Biere, Armin
1 Bjørner, Dines
1 Blass, Andreas Raphael
1 Bobot, François
1 Bodik, Rastislav
...and 234 more Authors

Citations by Year