Recent Papers and Reports
Recent Papers and Reports
- Scaling Network Verification using Symmetry and Surgery. Gordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese. Preliminary version of paper to appear at POPL 2016.
- ddNF: An Efficient Data Structure for Header Spaces. Nikolaj Bjørner, Garvit Juniwal, Ratul Mahajan, Sanjit A. Seshia, George Varghese. MSR-TR 2015.
- On Conflicts and Strategies in QBF. Nikolaj Bjørner, Mikoláš Janota and William Klieber. Short Presentation Paper @ LPAR 20, Fiji, November 2015.
- Playing with Quantified Satisfaction. Nikolaj Bjørner, Mikoláš Janota. Short Presentation Paper @ LPAR 20. Fiji, November 2015.
- Maximum Satisfiability using Cores and Correction Sets. Nikolaj Bjorner, Nina Narodytska. IJCAI 2015.
- Property-Directed Inference of Universal Invariants or Proving Their Absence. Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham. CAV 2015.
- Horn Clause Solving for Program Verification. Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, Andrey Rybalchenko. YuriFest 75, Berlin 2015.
- Symbolic Tree Automata, Margus Veanes and Nikolaj Bjørner, Information Processing Letters, vol. 115, no. 3, pp. 418-424, Elsevier, March 2015
- Checking Cloud Contracts in Microsoft Azure. Nikolaj Bjørner and Karthick Jayaraman. Invited paper for ICDCIT February, 2015.
- Automated Analysis and Debugging of Network Connectivity Policies. Karthick Jayaraman, Nikolaj Bjorner, Geoff Outhred, and Charlie Kaufman
- nu-Z: An Optimizing SMT Solver. Nikolaj Bjørner and Anh-Dung Phan and Lars Fleckenstein. TACAS April 2015.
- Property Directed Polyhedral Abstraction. Nikolaj Bjørner and Arie Gurfinkel. VMCAI 2015.
- newZ: Maximal Satisfaction with Z3. Nikolaj Bjørner and Anh-Dung Phan. Invited paper, in SCSS 2014.
- Computing All Implied Equalities via SMT-based Partition Refinement. Josh Berdine and Nikolaj Bjørner, IJCAR 2014. Technical Report.
- Monadic Decomposition. Margus Veanes, Nikolaj Bjørner, Lev Nachmanson and Sergey Bereg. CAV 2014.
- Property Directed Shape Analysis. Shachar Itzhaky, Nikolaj Bjørner, Thomas Reps, Mooly Sagiv, and Aditya Thakur. CAV 2014.
- Checking beliefs in Dynamic Networks. Nuno Lopes, Nikolaj Bjorner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. Technical Report. Revised version in NSDI 2015.
- VeriCon: Towards Verifying Controller Programs in Software-Defined Networks. Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira and Asaf Valadarsky. PLDI 2014
- Software Engineering and Automated Deduction. Willem Visser, Nikolaj Bjørner, Natarajan Shankar. Future of Software Engineering session @ ICSE 2014.
- Instantiations, Zippers and EPR Interpolation. Nikolaj Bjørner, Konstantin Korovin, Arie Gurfinkel and Ori Lahav. Short paper at LPAR 19.
- Resourceful Reachability as HORN-LA. Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, Christoph Wintersteiger. LPAR 19.
- Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. Nikolaj Bjørner, Ken McMillan and Andrey Rybalchenko. In informal proceedings of HOPA 2013 (workshop on Higher-Order Program Analysis).
- On Solving Universally Quantified Horn Clauses. Nikolaj Bjørner, Ken McMillan and Andrey Rybalchenko. SAS 2013
- Journal of Automated Deduction, Preface to a special issue dedicated to CADE 23. Nikolaj Bjørner, Viorica Sofronie-Stokkermans.
- Program Verification as Satisfiability Modulo Theories. Nikolaj Bjørner, Ken McMillan, Andrey Rybalchenko. SMT workshop 2012. Slides
- An SMT-LIB Format for Sequences and Regular Expressions. Nikolaj Bjørner, Vijay Ganesh, Raphael Michel, Margus Veanes. SMT workshop 2012.
- Anatomy of Alternating Quantifier Satisfiability. Anh-Dung Phan, Nikolaj Bjørner, David Monniaux. SMT workshop 2012.
- Taking Satisfiability to the Next Level with Z3. Nikolaj Bjørner. Invited talk, IJCAR 2012.
- Generalized Property Directed Reachability. Krystof Hoder and Nikolaj Bjørner. In SAT 2012.
- Tractability and Modern Satisfiability Modulo Theories Solvers. Nikolaj Bjørner and Leonardo de Moura. In Handbook of Tractability. Editors: Lucas Bordeaux, Youssef Hamadi, Pushmeet Kohli, Robert Mateescu. Cambridge University Press.
- Latent Fault Detection in Cloud Services, Mickey Gabel, Assaf Schuster, Ran Gilad-Bachrach, Nikolaj Bjørner. In DSN 2012.
- Symbolic Automata: The Toolkit, Margus Veanes and Nikolaj Bjørner, in TACAS’12, Springer Verlag, March 2012
- Logic for Programming, Artificial Intelligence, and Reasoning – 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Nikolaj Bjørner, Andrei Voronkov. Proceedings Springer 2012
- From Primal Infon Logic with Individual Variables to Datalog Nikolaj Bjørner, Guido de Caso and Yuri Gurevich Microsoft Research Technical Report MSR-TR-2011-84, July 2011In Vladimir Lifschitz Festschrift
- Symbolic Finite State Transducers: Algorithms and Applications. Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjørner, in POPL’12, ACM SIGPLAN, January 2012
- Foreword to special issue dedicated to WING, Workshop on invariant generation, Journal of Symbolic Computation 2012. Editors Nikolaj Bjørner and Laura Kovacs.
- Engineering Theories with Z3. Nikolaj Bjørner. Invited talk, APLAS 2011.
- Foundations of Symbolic Tree Transducers. Margus Veanes and Nikolaj Bjørner. Bulletin of the EATCS, October 2011.
- Satisfiability Modulo Theories: Introduction and Applications. Leonardo de Moura, Nikolaj Bjørner. Communications of the ACM, September 2011.
- Automated Deduction – CADE-23 – 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 – August 5, 2011. Nikolaj Bjørner, Viorica Sofronie-Stokkermans. Proceedings. Springer 2011
- µZ – An Efficient Engine for Fixed-Points with Constraints. Krystof Hoder, Nikolaj Bjørner and Leonardo de Moura. CAV 2011.
- Applications and Challenges in Satisfiability Modulo Theories. Leonardo de Moura and Nikolaj Bjørner. In the First EasyChair Volume on WING (Workshop on Invariant Generation).
- Canonical Regular Types. Ethan Jackson, Nikolaj Bjørner, Wolfram Schulte. ICLP-2011.
- Symbolic Tree Transducers. Margus Veanes, Nikolaj Bjørner. PSI-2011.
- Symbolic Transducers. Margus Veanes, Nikolaj Bjørner. MSR-TR
- Alternating Simulation and IOCO, Margus Veanes, Nikolaj Bjørner. ICTSS 2010
- Symbolic Automata Constraint Solving. Margus Veanes, Nikolaj Bjørner, Leonardo de Moura. LPAR (Yogyakarta) 2010.
- DKAL and Z3: A Logic Embedding Experiment. Sergio Mera, Nikolaj Bjørner. Fields of Logic and Computation 2010: 504-528.
- Linear Quantifier Elimination as an Abstract Decision Procedure. Nikolaj Bjørner. IJCAR 2010.
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development. Leonardo de Moura, Nikolaj Bjørner. IJCAR 2010.
- TAPAS Theory Combinations and Practical Applications. Nikolaj Bjørner and Leonardo de Moura. Invited talk at FORMATS 2009. (Slides)
- Generalized, Efficient Array Decision Procedures. Leonardo de Moura, Nikolaj Bjørner. FMCAD 2009. Extended version in MSR-TR-121.
- Specifying and Composing Non-functional Requirements in Model-Based Development. Ethan K. Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner, Wolfram Schulte. Software Composition 2009: 72-89.
- Z310: Applications, Enablers, Challenges and Directions. Nikolaj Bjørner and Leonardo de Moura. Invited paper for CFV 2009. (Slides)
- Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis (MSR-TR-2009-57). Yannick Moy, Nikolaj Bjørner, Dave Sielaff. A workshop paper on the bit-precise aspects “Sound, Efficient, Bit-precise Static Analysis” appeared at CFV 2009.
- Input-Output Model Programs (MSR-TR-2009-56) Margus Veanes, Nikolaj Bjørner. ICTAC 2009.
- Symbolic Bounded Conformance Checking of Model Programs (MSR-TR-2009-28) Appeared at PSI 2009. Margus Veanes, Nikolaj Bjørner
- Symbolic Bounded Model Checking of Abstract State Machines (MSR-TR-2009-14) Margus Veanes, Nikolaj Bjørner, Yuri Gurevich, Wolfram Schulte.
- Linear Functional Fixed-points (MSR-TR-2009-8). Nikolaj Bjørner and Joe Hendrix. Revised conference version at CAV 2009. Slides
- RAP – Resource Adaptive Programming with an application to robust and fast file copying. Utkarsh Upadhyay and Nikolaj Bjørner. PDF
- Deciding Effectively Propositional Logic with Equality Ruzica Piskac, Leonardo de Moura, Nikolaj Bjørner. MSR-TR-2008-181.
- Nikolaj Bjørner, Bruno Dutertre and Leonardo de Moura. Accelerating Lemma Learning using Joins – DPPL(Join). Short paper at LPAR 2008. PDF.
- Proofs and Refutations, and Z3. Leonardo de Moura and Nikolaj Bjørner. IWIL 2008. PDF.
- Path Feasibility Analysis for String-Manipulating Programs Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov. MSR-TR-2008-153 (appeared at TACAS 2009).
- Modular difference logic is hard Nikolaj Bjørner, Andreas Blass, Yuri Gurevich, Madan Musuvathi. MSR-TR-2008-140
- Satisfiability Modulo Bit-precise Theories for Program Exploration Nikolaj Bjørner, Leonardo de Moura and Nikolai Tillmann. Invited workshop paper, CFV 2008. Power point Slides
- Engineering DPLL(T) + Saturation. Leonardo de Moura and Nikolaj Bjørner IJCAR 2008
- Deciding Effectively Propositional Logic using DPLL and Substitution Sets. Conference version at IJCAR 2008 Power Point slides. Leonardo de Moura, Ruzica Piskac and Nikolaj Bjørner
- Using Dynamic Symbolic Execution to Improve Deductive Verification Dries Vanoverberghe, Nikolaj Bjørner, Jonathan de Halleux, Wolfram Schulte, Nikolai Tillmann Invited paper, SPIN 2008.
- Bounded Reachability of Model Programs Margus Veanes; Ando Saabas; Nikolaj Bjørner
- An SMT Approach to Bounded Reachability Analysis of Model Programs. Margus Veanes, Nikolaj Bjørner, Alexander Raschke. FORTE 2008: 53-68
- Z3: An Efficient SMT Solver Leonardo de Moura and Nikolaj Bjørner TACAS, April 2008.Awarded The most influential tool paper in the first 20 years of TACAS at TACAS 2014.
- Relevancy Propagation Leonardo de Moura and Nikolaj Bjørner. Technical Note, October 2007.
- Content-Dependent Chunking for Differential Compression, The Local Maximum Approach Nikolaj Bjørner, Andreas Blass, Yuri Gurevich. MSR-TR August 2007.Appears in Journal of Computer and System Sciences, Elsevier, 2009.
- Models and Software Model Checking for a Distributed File Replication System. Nikolaj Bjørner. Appears in Formal Methods and Hybrid Real-Time Systems September 2007: 1-23.
- Efficient E-matching for SMT solvers. Leonardo de Moura and Nikolaj Bjørner. CADE 2007. PDF.
- Model-based Theory Combination. Leonardo de Moura and Nikolaj Bjørner. SMT 2007. PDF.
- Optimizing File Replication over Limited-Bandwidth Networks using Remote Differential Compression. Dan Teodosiu; Nikolaj Bjørner; Yuri Gurevich; Mark Manasse; Joe Porkka 2006.
Conferences and Workshops
Links
Links
- My very old home page
- RiSE: Research In Software Engineering.
- Automata Benchmarks
- RiSE & SMT slides
- SecGuru benchmarks
Slides
Slides
- Tutorial on Network Verification with George Varghese at SIGCOMM 2015.Slides, Demo
- Marktoberdorf summer school MOD-10-8-15 MOD-12-8-2015 MOD-14-8-2015
- VTSA 2014 summer school (lecturer)
- Slides 1, 2, 3
- FLAIRS 26, Invited talk
- Formal Methods and Networks, Summer School, Ithaca June 10-14 2013
- Verified Software Summer School, Shanghai, Aug 23-31, 2012Lecture 1 (August 29)Lecture 2 (August 30)Lecture 3 (August 31)Lecture 4 (August 31)
- MSR India Summer School, Bangalore June 24-28, 2008 lecture 1 lecture 2 lecture 3 lecture 4 lecture 5 Lab exercises
- UW Seminar, October 20, 2009. (Slides)
Old Workshops and Conferences
Old Workshops and Conferences
- TASE 2015 (PC)
- FMCAD 2015 (PC)
- Dagstuhl seminar on Deduction: Extracting Information from Deduction, Models and Proofs. (co-organizer)
- SYNASC 2015 (Track chair for Logic and Programming)
- FM 2015 (PC co-chair)
- TAP 2015 (PC)
- QUANTIFY @ CADE 2015 (PC)
- AMI @ CADE 2015 (PC)
- ICFEM 2015 (PC)
- ICDCIT 2015 (invited speaker)
- Dagstuhl seminar on Formal Foundations of Networking (co-organizer
- ICFEM 2014 (invited speaker)
- SDN and NFV Conference (invited speaker)
- CAV 2014 (PC)
- FMCAD 2014 (PC)
- CSTVA 2014 (Invited speaker)
- HCVS 2014 (co organizer)
- TASE 2014 (PC)
- ECAI 2014 (external reviewer)
- SAT/SMT Summer School (lecturer)
- Software for Quantified Reasoning (co organizer)
- SSFT14, Menlo Park
- IMDEA, Microsoft workshop
- TACAS 2014 (Tool chair)
- NFM 2014 (PC)
- ReRISE winter school (lecturer)
- Dagstuhl Seminar: Deduction and Arithmetic (co-organizer with Rainer Hähnle, Tobias Nipkow, Christoph Weidenbach)
- FMCAD 2013 (PC)
- CAS 2013 (keynote)
- PAS 2013 (invited speaker)
- SCSS 2013 (PC)
- ICDCIT 2014 (PC)
- QBF workshop 2013 (PC)
- CAV 2013 (SAT/SMT Track chair)
- SYNASC 2013 (PC chair)
- ICFEM 2013 (PC)
- HOPA
- FIMCP
- HCSS 2013, Keynote
- VMCAI 2013 (PC)
- ICFEM 2012 (PC)
- SYNASC 2012 (PC)
- YaC (Talk)
- Yandex (tech Talk)
- SEW-35 (PC)
- Dagstuhl Seminar, November 11-16 2012: Games & Decisions: Rigorous Systems Engineering (co-organizer with Laura Kovacs, Krishnendu Chatterjee, Rupak Majumdar)
- CPP 2012
- ASE 2012 (PC)
- ICEGOV 2012 (PC)
- Scandinavian Logic Symposium (Invited speaker), Roskilde Aug 20-21.
- DANSAS, Odense Aug 24. (Invited talk on Static analysis and verification as Satisfiability Modulo Theories). Slides.
- Turing-100 (PC)
- SMT 2012 (PC)
- WING 2012 (PC)
- AREIS 2012 (PC)
- SC 2012 (PC)
- CSL 2012 (PC)
- LPAR-18 (PC co-chair with Andrei Voronkov)
- IWIL 2012 (Invited Speaker)
- TAP 2012 (PC)
- NFM 2012 (PC)
- VMCAI 2012 (PC)
- Logic in CS workshop, Steklov Feb 1-3
- SMT/Z3 Course at DTU Jan 2-11
- APLAS+CPP 2011 (Keynote)
- Z3 SIG meeting MSR Cambridge (Nov 2-4)
- ASE 2011 (PC)
- Kutaisi 2011 (Invited speaker)
- Dagstuhl Seminar on SMT solvers in hard, soft and bio-ware. July 2011. (co-organizer)
- SC 2011 (PC)
- Software Engineering Workshop,Ireland 2011 (PC)
- CADE 2011 (PC co-chair with Viorica)
- ICFEM 2011 (PC)
- ICEGOV 2011 (PC)
- MIT Summer school on SAT/SMT (June 2011) (co-organizer)
- 1st HIPERFIT workshop: FORMULA & F*
- NFM 2011 (PC)
- TAP 2011 (PC)
- WRiSE 2011 (PC)
- Seminar on deduction at Scale, Ringberg. March 2011. (co-organizer)Photos
- TACAS 2011 (PC)
- POPL 2011 Tutorial on Theorem Proving Tools for Program Analysis
- ICDCIT 2011 (PC)
- ICGOV 2010 (PC)
- LPAR 17 (PC)
- CSL 2010 (PC)
- WING 2010 (chair with Laura Kovacs)
- SMT 2010 (PC)
- CASC 2010 (panel)
- IJCAR 2010 (PC)
- MSR Cambridge Workshop on Tractability(PPTX, PDF), July 5,6 2010.
- PLDI Tutorial on SMT/Z3
- Dagstuhl Seminar on SMT solvers in Soft-, Hard- and Bio-ware, Spring 2010, (co-organizer)
- NFM 2010 (invited speaker) (pptx, pdf)
- LPAR 16 (PC)
- QSIC 2010 (PC)
- ICDCIT 2010 (PC)
- FMCAD 2009 (Tutorial) (Slides)
- SYNASC 2009 (Tutorial) (Slides)
- FORMATS 2009 (Invited speaker)
- CADE 2009 (PC)
- CAV 2009 (PC)
- RV 2009 (PC)
- CFV 2009 (Invited speaker)
- WING 2009 (PC)
- ICEGOV2008 – 2nd International Conference on Theory and Practice of Electronic Governance (PC)
- SMT in Program Analysis and Verification at IJCAR 2008 (tutorial co-organizer)
- Practical Aspects of Automated Reasoning (PAAR-2008) (PC)
- ESARM 08 (PC)
- SMT 2008 (PC)
- IJCAR 2008 (PC)
- MSR India Summer School on Programming Languages, Analysis and Verification (lecturer)
- CSR 2007 (PC)
- WING 2007 (PC)
- ESARLT 2007 (PC)
- LPAR 2007 (PC)