4 Search Results for "Bj�rner, Nikolaj"


Document
Analysis of Core-Guided MaxSat Using Cores and Correction Sets

Authors: Nina Narodytska and Nikolaj Bjørner

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)


Abstract
Core-guided solvers are among the best performing algorithms for solving maximum satisfiability problems. These solvers perform a sequence of relaxations of the formula to increase the lower bound on the optimal solution at each relaxation step. In addition, the relaxations allow generating a large set of minimal cores (MUSes) of the original formula. However, properties of these cores in relation to the optimization objective have not been investigated. In contrast, minimum hitting set based solvers (MaxHS) extract a set of cores that are known to have properties related to the optimization objective, e.g., the size of the minimum hitting set of the discovered cores equals the optimum when the solver terminates. In this work we analyze minimal cores and minimum correction sets (MinCSes) of the input formula and its sub-formulas that core-guided solvers produce. We demonstrate that a set of MUSes that a core-guided algorithm discovers possess the same key properties as cores extracted by MaxHS solvers. For instance, we prove the size of a minimum hitting set of these cores equals the optimal cost. We also show that it discovers all MinCSes of special subformulas of the input formula. We discuss theoretical and practical implications of our results.

Cite as

Nina Narodytska and Nikolaj Bjørner. Analysis of Core-Guided MaxSat Using Cores and Correction Sets. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{narodytska_et_al:LIPIcs.SAT.2022.26,
  author =	{Narodytska, Nina and Bj{\o}rner, Nikolaj},
  title =	{{Analysis of Core-Guided MaxSat Using Cores and Correction Sets}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.26},
  URN =		{urn:nbn:de:0030-drops-167006},
  doi =		{10.4230/LIPIcs.SAT.2022.26},
  annote =	{Keywords: maximum satisfiability, unsatisfiable cores, correction sets}
}
Document
Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)

Authors: Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu

Published in: Dagstuhl Reports, Volume 11, Issue 9 (2022)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21431 "Rigorous Methods for Smart Contracts". Blockchain technologies have emerged as an exciting field for both researchers and practitioners focusing on formal guarantees for software. It is arguably a "once in a lifetime" opportunity for rigorous methods to be integrated in audit processes for parties deploying smart contracts, whether for fund raising, securities trading, or supply-chain management. Smart contracts are programs managing cryptocurrency accounts on a blockchain. Research in the area of smart contracts includes a fascinating combination of formal methods, programming-language semantics, and cryptography. First, there is vibrant development of verification and program-analysis techniques that check the correctness of smart-contract code. Second, there are emerging designs of programming languages and methodologies for writing smart contracts such that they are more robust by construction or more amenable to analysis and verification. Programming-language abstraction layers expose low-level cryptographic primitives enabling developers to design high-level cryptographic protocols. Automated-reasoning mechanisms present a common underlying enabler; and the specific needs of the smart-contract world offer new challenges. This workshop brought together stakeholders in the aforementioned areas related to advancing reliable smart-contract technologies.

Cite as

Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu. Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). In Dagstuhl Reports, Volume 11, Issue 9, pp. 80-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{bjrner_et_al:DagRep.11.9.80,
  author =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  title =	{{Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)}},
  pages =	{80--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{9},
  editor =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.11.9.80},
  URN =		{urn:nbn:de:0030-drops-159198},
  doi =		{10.4230/DagRep.11.9.80},
  annote =	{Keywords: automated reasoning, cryptographic protocols, program verification, programming languages, smart contracts}
}
Document
Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)

Authors: Sébastien Bardin, Nikolaj Bjørner, and Cristian Cadar

Published in: Dagstuhl Reports, Volume 9, Issue 2 (2019)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 19062 "Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving", whose main goals were to bring together leading researchers in the different subfields of automated reasoning and constraint solving, foster greater communication between these communities and exchange ideas about new research directions. Constraint solving is at the heart of several key technologies, including program analysis, testing, formal methods, compilers, security analysis, optimization, and AI. During the last two decades, constraint solving has been highly successful and transformative: on the one hand, SAT/SMT solvers have seen a significant performance improvement with a concomitant impact on software engineering, formal methods and security; on the other hand, CP solvers have also seen a dramatic performance improvement, with deep impact in AI and optimization. These successes bring new applications together with new challenges, not yet met by any current technology. The seminar brought together researchers from SAT, SMT and CP along with application researchers in order to foster cross-fertilization of ideas, deepen interactions, identify the best ways to serve the application fields and in turn help improve the solvers for specific domains.

Cite as

Sébastien Bardin, Nikolaj Bjørner, and Cristian Cadar. Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062). In Dagstuhl Reports, Volume 9, Issue 2, pp. 27-47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@Article{bardin_et_al:DagRep.9.2.27,
  author =	{Bardin, S\'{e}bastien and Bj{\o}rner, Nikolaj and Cadar, Cristian},
  title =	{{Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (Dagstuhl Seminar 19062)}},
  pages =	{27--47},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{2},
  editor =	{Bardin, S\'{e}bastien and Bj{\o}rner, Nikolaj and Cadar, Cristian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.9.2.27},
  URN =		{urn:nbn:de:0030-drops-108574},
  doi =		{10.4230/DagRep.9.2.27},
  annote =	{Keywords: Automated Decision Procedures, Constraint Programming, SAT, SMT}
}
Document
Canonical Regular Types

Authors: Ethan K. Jackson, Nikolaj Bjørner, and Wolfram Schulte

Published in: LIPIcs, Volume 11, Technical Communications of the 27th International Conference on Logic Programming (ICLP'11) (2011)


Abstract
Regular types represent sets of structured data, and have been used in logic programming (LP) for verification. However, first-class regular type systems are uncommon in LP languages. In this paper we present a new approach to regular types, based on type canonization, aimed at providing a practical first-class regular type system.

Cite as

Ethan K. Jackson, Nikolaj Bjørner, and Wolfram Schulte. Canonical Regular Types. In Technical Communications of the 27th International Conference on Logic Programming (ICLP'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 11, pp. 73-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Copy BibTex To Clipboard

@InProceedings{jackson_et_al:LIPIcs.ICLP.2011.73,
  author =	{Jackson, Ethan K. and Bj{\o}rner, Nikolaj and Schulte, Wolfram},
  title =	{{Canonical Regular Types}},
  booktitle =	{Technical Communications of the 27th International Conference on Logic Programming (ICLP'11)},
  pages =	{73--83},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-31-6},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{11},
  editor =	{Gallagher, John P. and Gelfond, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2011.73},
  URN =		{urn:nbn:de:0030-drops-31806},
  doi =		{10.4230/LIPIcs.ICLP.2011.73},
  annote =	{Keywords: Regular types, Canonical forms, Type canonizer}
}
  • Refine by Author
  • 3 Bjørner, Nikolaj
  • 1 Bardin, Sébastien
  • 1 Bjørner, Nikolaj S.
  • 1 Cadar, Cristian
  • 1 Christakis, Maria
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Solvers
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Formal language definitions
  • 1 Software and its engineering → Software verification and validation
  • 1 Theory of computation → Logic

  • Refine by Keyword
  • 1 Automated Decision Procedures
  • 1 Canonical forms
  • 1 Constraint Programming
  • 1 Regular types
  • 1 SAT
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2022
  • 1 2011
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail