Skip to content

Publications

Jump to bottom Edit New page
Nikolaj Bjorner edited this page Sep 19, 2019 · 9 revisions
  1. Andreas Fröhlich, Armin Biere, Christoph M. Wintersteiger, Youssef Hamadi: Stochastic Local Search for Satisfiability Modulo Theories. AAAI 2015.
  2. Nikolaj Bjørner and Anh-Dung Phan and Lars Fleckenstein. nu-Z: An Optimizing SMT Solver. TACAS April 2015.
  3. Nikolaj Bjørner and Arie Gurfinkel.Property Directed Polyhedral Abstraction. VMCAI 2015.</em>
  4. Aleksandar Zeljic, Christoph M. Wintersteiger, and Philipp Rümmer. Approximations for Model Construction. IJCAR 2014.
  5. Markus N. Rabe, Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov, and Youssef Hamadi. Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains. QEST 2014.
  6. Nikolaj Bjørner and Anh-Dung Phan. newZ: Maximal Satisfaction with Z3. Invited paper, in SCSS 2014.
  7. Josh Berdine and Nikolaj Bjørner. Computing All Implied Equalities via SMT-based Partition Refinement. IJCAR 2014. Technical Report.
  8. Margus Veanes, Nikolaj Bjørner, Lev Nachmanson and Sergey Bereg.Monadic Decomposition. CAV 2014.
  9. Shachar Itzhaky, Nikolaj Bjørner, Thomas Reps, Mooly Sagiv, and Aditya Thakur.Property Directed Shape Analysis. CAV 2014.
  10. Nuno Lopes, Nikolaj Bjorner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. Checking beliefs in Dynamic Networks. Technical Report. Revised version to appear in NSDI 2015.
  11. Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira and Asaf Valadarsky.VeriCon: Towards Verifying Controller Programs in Software-Defined Networks. PLDI 2014
  12. Nikolaj Bjørner, Konstantin Korovin, Arie Gurfinkel and Ori Lahav.Instantiations, Zippers and EPR Interpolation. Short paper at LPAR 19.
  13. Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph Wintersteiger.Resourceful Reachability as HORN-LA. LPAR 19. 
  14. Nikolaj Bjørner, Ken McMillan and Andrey Rybalchenko.Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. In informal proceedings of HOPA 2013 (workshop on Higher-Order Program Analysis).
  15. Nikolaj Bjørner, Ken McMillan and Andrey Rybalchenko.On Solving Universally Quantified Horn Clauses. SAS 2013
  16. Nikolaj Bjørner, Ken McMillan, Andrey Rybalchenko.Program Verification as Satisfiability Modulo Theories. SMT workshop 2012. Slides
  17. Nikolaj Bjørner, Vijay Ganesh, Raphael Michel, Margus Veanes. An SMT-liB Format for Sequences and Regular Expressions. SMT workshop 2012.
  18. Leonardo de Moura and Grant Passmore. Computation in real closed infinitesimal and transcendental extensions of the rationals. In Automated Deduction - CADE-24, 24th International Conference on Automated Deduction, Lake Placid, New York, June 9-14, 2013, Proceedings, 2013.
  19. Leonardo de Moura and Grant Passmore. The Strategy Challenge in SMT Solving, volume 7788 of Lecture Notes in Artificial Intelligence. Springer, 2013. [.pdf]
  20. Leonardo de Moura and Dejan Jovanović. A model-constructing satisfiability calculus. In 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI, Rome, Italy, 2013, 2013. [ .pdf ]
  21. Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. In Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 339-354. Springer, 2012. [ .pdf ]
  22. Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. Technical Report MSR-TR-2012-20, Microsoft Research, 2012. [ http ]
  23. Nikolaj Bjørner. Taking Satisfiability to the Next Level with Z3. IJCAR 2012.
  24. Anh-Dung Phan, Nikolaj Bjørner, David Monniaux. Anatomy of Alternating Quantifier Satisfiability. SMT workshop 2012. [ .pdf ]
  25. Krystof Hoder and Nikolaj Bjørner. Generalized Property Directed Reachability. In SAT 2012. [.pdf]
  26. Christoph Wintersteiger, Youssef Hamadi, and Leonardo de Moura. Efficiently solving quantified bit-vector formulas. Formal Methods in System Design, 2012. [ http | .pdf ]
  27. Nikolaj Bjørner and Leonardo de Moura. Tractability and Modern Satisfiability Modulo Theories Solvers. In Handbook of Tractability. Cambridge University Press, 2012. [.pdf]
  28. Krystof Hoder, Nikolaj Bjørner, and Leonardo de Moura. muZ - an efficient engine for fixed points with constraints. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 457-462, 2011. [.pdf]
  29. Leonardo de Moura and Nikolaj Bjørner. Satisfiability modulo theories: introduction and applications. Commun. ACM, 54(9):69-77, 2011. [ http ]
  30. Dejan Jovanović and Leonardo de Moura. Cutting to the chase solving linear integer arithmetic. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 338-353. Springer, 2011. [ .pdf ]
  31. Maria Paola Bonacina, Christopher Lynch, and Leonardo de Moura. On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning, 47(2):161-189, 2011. [ .pdf ]
  32. Leonardo de Moura and Nikolaj Bjørner. Bugs, moles and skeletons: Symbolic reasoning for software development. In Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science, pages 400-411. Springer, 2010. [ .pdf ]
  33. Nikolaj Bjørner. Linear Quantifier Elimination as an Abstract Decision Procedure. IJCAR 2010.
  34. Margus Veanes, Nikolaj Bjørner, and Leonardo de Moura. Symbolic automata constraint solving. In Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 640-654, 2010. [ .pdf ]
  35. Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning, 44(4):401-424, 2010. [ http ]
  36. Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura. Efficiently solving quantified bit-vector formulas. In Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pages 239-246. IEEE, 2010. [ .pdf ]
  37. Leonardo de Moura and Nikolaj Bjørner. Generalized, efficient array decision procedures. In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA, pages 45-52. IEEE, 2009. [ .pdf ]
  38. Nikolaj Bjørner and Leonardo de Moura. Tapas: Theory combinations and practical applications. In Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, volume 5813 of Lecture Notes in Computer Science, pages 1-6. Springer, 2009. [ http ]
  39. Leonardo de Moura and Nikolaj Bjørner. Satisfiability modulo theories: An appetizer. In Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers, volume 5902 of Lecture Notes in Computer Science, pages 23-36. Springer, 2009. [ .pdf ] 
  40. Nikolaj Bjørner and Joe Hendrix. Linear Functional Fixed-points. CAV 2009.
  41. Maria Paola Bonacina, Christopher Lynch, and Leonardo de Moura. On deciding satisfiability by DPLL(Γ+T) and unsound theorem proving. In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663 of Lecture Notes in Computer Science, pages 35-50. Springer, 2009. [ .pdf ]
  42. Yeting Ge and Leonardo de Moura. Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 306-320. Springer, 2009. [ .pdf ]
  43. Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura. A concurrent portfolio approach to SMT solving. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 715-720. Springer, 2009. [ .pdf ]
  44. Grant Olney Passmore and Leonardo de Moura. Superfluous S-polynomials in strategy-independent groebner bases. In 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2009, Timisoara, Romania, September 26-29, 2009, pages 45-53. IEEE Computer Society, 2009. [ .pdf ]
  45. Nikolaj Bjørner and Leonardo de Moura. z310: Applications, enablers, challenges and directions. In Sixth International Workshop on Constraints in Formal Verification Grenoble, France, 2009. [ .pdf ]
  46. Leonardo de Moura and Grant Olney Passmore. On locally minimal nullstellensatz proofs. In 7th International Workshop on Satisfiability Modulo Theories, SMT, Montreal, Canada, 2009. [ .pdf ]
  47. Leonardo de Moura and Grant Olney Passmore. On locally minimal nullstellensatz proofs. Technical Report MSR-TR-2009-90, Microsoft Research, 2009. [ .pdf ]
  48. Grant Olney Passmore and Leonardo de Moura. Universality of polynomial positivity and a variant of Hilbert's 17th problem. In Automated Deduction: Decidability, Complexity, Tractability, ADDCT'09, Montreal, Canada, 2009. [ .pdf ]
  49. Ruzica Piskac, Leonardo de Moura, and Nikolaj Bjørner. Deciding effectively propositional logic with equality. Technical Report MSR-TR-2008-181, Microsoft Research, 2008. [ http ]
  50. Leonardo de Moura and Nikolaj Bjørner. Deciding effectively propositional logic using DPLL and substitution sets. In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 410-425. Springer, 2008.
  51. Leonardo de Moura and Nikolaj Bjørner. Engineering DPLL(T) + Saturation. In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 475-490. Springer, 2008. [ .pdf ]
  52. Leonardo de Moura and Nikolaj Bjørner. Proofs and refutations, and Z3. In Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008, volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. [ .pdf ]
  53. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. [ .pdf ]
  54. Leonardo de Moura and Nikolaj Bjørner. Model-based theory combination. Electr. Notes Theor. Comput. Sci., 198(2):37-49, 2008. [ .pdf ]
  55. Nikolaj Bjørner, Bruno Dutertre, and Leonardo de Moura. Accelerating lemma learning using joins - DPPL(Join). In 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR'08, 2008. [ .pdf ]
  56. Nikolaj Bjørner, Leonardo de Moura, and Nikolai Tillmann. Satisfiability modulo bit-precise theories for program exploration. In Fifth International Workshop on Constraints in Formal Verification, (CFV'08), Sydney, Australia, 2008. [ .pdf ]
  57. Leonardo de Moura and Nikolaj Bjørner. Efficient E-Matching for SMT solvers. In Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pages 183-198. Springer, 2007. [ .pdf ]

                            

Add a custom sidebar
Clone this wiki locally