BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Brazil
1 × Estonia
1 × France
1 × Hungary
1 × India
1 × Italy
1 × Portugal
2 × Australia
2 × Germany
3 × Austria
7 × USA
7 × United Kingdom
Collaborated with:
L.M.d.Moura M.Veanes A.Rybalchenko K.Hoder A.Phan K.L.McMillan E.K.Jackson W.Schulte T.E.Uribe S.Itzhaky A.Gurfinkel J.Berdine J.Hendrix C.Muñoz M.C.Pichora L.Fleckenstein D.Monniaux N.Tillmann A.Voronkov M.E.Stickel K.v.Gleissenthall A.Karbyshev M.Sagiv L.Nachmanson S.Bereg V.Ganesh R.Michel A.Browne E.Y.Chang M.Colón A.Kapur Z.Manna H.Sipma N.Rinetzky S.Shoham T.W.Reps A.V.Thakur P.Hooimeijer B.Livshits D.Molnar G.D.Plotkin N.P.Lopes G.Varghese T.Ball A.Gember M.Schapira A.Valadarsky L.d.Alfaro H.Devarajan J.Lee
Talks about:
smt (5) quantifi (4) properti (4) satisfi (4) direct (4) fix (4) univers (3) program (3) theori (3) symbol (3)

♂ Person: Nikolaj Bjørner

DBLP DBLP: Bj=oslash=rner:Nikolaj

Facilitated 4 volumes:

FM 2015Ed
ASE 2012PrCo
ASE 2011PrCo
CADE 2011Ed

Contributed to:

CAV 20152015
TACAS 20152015
VMCAI 20152015
CAV 20142014
IJCAR 20142014
PLDI 20142014
HILT 20132013
SAS 20132013
IJCAR 20122012
MoDELS 20122012
POPL 20122012
SAT 20122012
SMT 20122012
TACAS 20122012
CAV 20112011
ICLP 20112011
ICTSS 20102010
IJCAR 20102010
CAV 20092009
TACAS 20092009
IJCAR 20082008
TACAS 20082008
CADE 20072007
SMT 20072008
RTA 20002000
TACAS 19981998
CADE 19971997
CAV 19961996
TAPSOFT CAAP/FASE 19951995
PLDI 20162016
POPL 20162016

Wrote 36 papers:

CAV-2015-KarbyshevBIRS #invariant #proving
Property-Directed Inference of Universal Invariants or Proving Their Absence (AK, NB, SI, NR, SS), pp. 583–602.
TACAS-2015-BjornerPF #named #optimisation #smt
νZ — An Optimizing SMT Solver (NB, ADP, LF), pp. 194–199.
VMCAI-2015-BjornerG #abstraction
Property Directed Polyhedral Abstraction (NB, AG), pp. 263–281.
CAV-2014-ItzhakyBRST #analysis
Property-Directed Shape Analysis (SI, NB, TWR, MS, AVT), pp. 35–51.
CAV-2014-VeanesBNB #composition #monad
Monadic Decomposition (MV, NB, LN, SB), pp. 628–645.
IJCAR-2014-BerdineB #refinement #smt
Computing All Implied Equalities via SMT-Based Partition Refinement (JB, NB), pp. 168–183.
PLDI-2014-BallBGIKSSV #named #network #source code #towards #verification
VeriCon: towards verifying controller programs in software-defined networks (TB, NB, AG, SI, AK, MS, MS, AV), p. 31.
HILT-2013-Bjorner #development #modulo theories #satisfiability
Satisfiability modulo theories for high integrity development (NB), pp. 5–6.
SAS-2013-BjornerMR #horn clause #on the #quantifier
On Solving Universally Quantified Horn Clauses (NB, KLM, AR), pp. 105–125.
IJCAR-2012-Bjorner #satisfiability
Taking Satisfiability to the Next Level with Z3 — (NB), pp. 1–8.
MoDELS-2012-JacksonSB #constraints #declarative #detection #fault #specification
Detecting Specification Errors in Declarative Languages with Constraints (EKJ, WS, NB), pp. 399–414.
POPL-2012-VeanesHLMB #algorithm #finite #transducer
Symbolic finite state transducers: algorithms and applications (MV, PH, BL, DM, NB), pp. 137–150.
SAT-2012-HoderB #reachability
Generalized Property Directed Reachability (KH, NB), pp. 157–171.
SMT-2012-BjornerGMV #regular expression #sequence
SMT-LIB Sequences and Regular Expressions (NB, VG, RM, MV), pp. 77–87.
SMT-2012-BjornerMR #modulo theories #satisfiability #verification
Program Verification as Satisfiability Modulo Theories (NB, KLM, AR), pp. 3–11.
SMT-2012-PhanBM #quantifier #satisfiability
Anatomy of Alternating Quantifier Satisfiability (ADP, NB, DM), pp. 120–130.
TACAS-2012-VeanesB #automaton #tool support
Symbolic Automata: The Toolkit (MV, NB), pp. 472–477.
CAV-2011-HoderBM #constraints #fixpoint #named #performance
μZ — An Efficient Engine for Fixed Points with Constraints (KH, NB, LMdM), pp. 457–462.
ICLP-2011-JacksonBS #canonical
Canonical Regular Types (EKJ, NB, WS), pp. 73–83.
ICTSS-2010-VeanesB #simulation
Alternating Simulation and IOCO (MV, NB), pp. 47–62.
IJCAR-2010-Bjorner #linear #quantifier
Linear Quantifier Elimination as an Abstract Decision Procedure (NB), pp. 316–330.
IJCAR-2010-MouraB #debugging #development #reasoning
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development (LMdM, NB), pp. 400–411.
CAV-2009-BjornerH #fixpoint #functional #linear
Linear Functional Fixed-points (NB, JH), pp. 124–139.
TACAS-2009-BjornerTV #analysis #source code #string
Path Feasibility Analysis for String-Manipulating Programs (NB, NT, AV), pp. 307–321.
IJCAR-2008-MouraB #effectiveness #logic #set #using
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets (LMdM, NB), pp. 410–425.
IJCAR-2008-MouraB08a
Engineering DPLL(T) + Saturation (LMdM, NB), pp. 475–490.
TACAS-2008-MouraB #named #performance #smt
Z3: An Efficient SMT Solver (LMdM, NB), pp. 337–340.
CADE-2007-MouraB #performance #smt
Efficient E-Matching for SMT Solvers (LMdM, NB), pp. 183–198.
SMT-2007-MouraB08 #modelling
Model-based Theory Combination (LMdM, NB), pp. 37–49.
RTA-2000-BjornerM #unification
Absolute Explicit Unification (NB, CM), pp. 31–46.
TACAS-1998-BjornerP
Deiding Fixed and Non-fixed Size Bit-vectors (NB, MCP), pp. 376–392.
CADE-1997-BjornerSU #first-order #integration #reasoning
A Practical Integration of First-Order Reasoning and Decision Procedures (NB, MES, TEU), pp. 101–115.
CAV-1996-BjornerBCCKMSU #named #realtime #verification
STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems (NB, AB, EYC, MC, AK, ZM, HS, TEU), pp. 415–418.
TAPSOFT-1995-MannaBBCCADKLSU #named #proving
STeP: The Stanford Temporal Prover (ZM, NB, AB, EYC, MC, LdA, HD, AK, JL, HS, TEU), pp. 793–794.
PLDI-2016-GleissenthallBR #quantifier #verification
Cardinalities and universal quantifiers for verifying parameterized systems (KvG, NB, AR), pp. 599–613.
POPL-2016-PlotkinBLRV #network #scalability #symmetry #using #verification
Scaling network verification using symmetry and surgery (GDP, NB, NPL, AR, GV), pp. 69–83.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.