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: Bj=oslash=rner:Nikolaj
Facilitated 4 volumes:
Ed
PrCoPrCo
EdContributed to:
2015
2015
20152014
2014
2014
2013
20132012
2012
2012
2012
201220122011
2011
20102010200920092008200820072008
2000199819971996
199520162016Wrote 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.