Search Results

Documents authored by Bjorner, Nikolaj

Found 2 Possible Name Variants:

Bjorner, Nikolaj

Document
DOI: 10.4230/DagRep.5.2.44
Formal Foundations for Networking (Dagstuhl Seminar 15071)

Authors: Nikolaj Bjorner, Nate Foster, Philip Brighten Godfrey, and Pamela Zave

Published in: Dagstuhl Reports, Volume 5, Issue 2 (2015)

Abstract
This report documents the program and outcomes of Dagstuhl Seminar 15071 "Formal Foundations for Networking." Networking is in the midst of a revolution being driven by rapidly expanding infrastructures and emerging software-defined networking architectures. There is a growing need for tools and methodologies that provide rigorous guarantees about performance, reliability, and security. This seminar brought together leading researchers and practitioners from the fields of formal methods, networking, programming languages, and security, to investigate the task of developing formal foundations for networks.
Cite as

Nikolaj Bjorner, Nate Foster, Philip Brighten Godfrey, and Pamela Zave. Formal Foundations for Networking (Dagstuhl Seminar 15071). In Dagstuhl Reports, Volume 5, Issue 2, pp. 44-63, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.5.2.44,
  author =	{Bjorner, Nikolaj and Foster, Nate and Godfrey, Philip Brighten and Zave, Pamela},
  title =	{{Formal Foundations for Networking (Dagstuhl Seminar 15071)}},
  pages =	{44--63},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{2},
  editor =	{Bjorner, Nikolaj and Foster, Nate and Godfrey, Philip Brighten and Zave, Pamela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.2.44},
  URN =		{urn:nbn:de:0030-drops-50440},
  doi =		{10.4230/DagRep.5.2.44},
  annote =	{Keywords: Formal methods, logic, middleboxes, model checking, networking, program synthesis, security, software-defined networking, verification}
}
Document
DOI: 10.4230/DagRep.3.10.1
Deduction and Arithmetic (Dagstuhl Seminar 13411)

Authors: Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach

Published in: Dagstuhl Reports, Volume 3, Issue 10 (2014)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13411 "Deduction and Arithmetic". The aim of this seminar was to bring together researchers working in deduction and fields related to arithmetic constraint solving. Current research in deduction can be categorized in three main strands: SMT solvers, automated first-order provers, and interactive provers. Although dealing with arithmetic has been in focus of all three for some years, there is still need of much better support of arithmetic. Reasong about arithmetic will stay at the center of attention in all three main approaches to automated deduction during the coming five to ten years. The seminar was an important event for the subcommunities involved that made it possible to communicate with each other so as to avoid duplicate effort and to exploit synergies. It succeeded also in identifying a number of important trends and open problems.
Cite as

Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach. Deduction and Arithmetic (Dagstuhl Seminar 13411). In Dagstuhl Reports, Volume 3, Issue 10, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.3.10.1,
  author =	{Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph},
  title =	{{Deduction and Arithmetic (Dagstuhl Seminar 13411)}},
  pages =	{1--24},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{10},
  editor =	{Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.10.1},
  URN =		{urn:nbn:de:0030-drops-44250},
  doi =		{10.4230/DagRep.3.10.1},
  annote =	{Keywords: Automated Deduction; Program Verification; Arithmetic Constraint Solving}
}
Document
DOI: 10.4230/DagRep.2.11.45
Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461)

Authors: Nikolaj Bjorner, Krishnendu Chatterjee, Laura Kovacs, and Rupak M. Majumdar

Published in: Dagstuhl Reports, Volume 2, Issue 11 (2013)

Abstract
This report documents the program and the outcomes of the Dagstuhl Seminar 12461 "Games and Decisions for Rigorous Systems Engineering". The seminar brought together researchers working in rigorous software engineering, with a special focus on the interaction between synthesis and automated deduction. This event was the first seminar of this kind and a kickoff of a series of seminars organised on rigorous systems engineering. The theme of the seminar was close in spirit to many events that have been held over the last decades. The talks scheduled during the seminar naturally reflected fundamental research themes of the involved communities.
Cite as

Nikolaj Bjorner, Krishnendu Chatterjee, Laura Kovacs, and Rupak M. Majumdar. Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). In Dagstuhl Reports, Volume 2, Issue 11, pp. 45-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.2.11.45,
  author =	{Bjorner, Nikolaj and Chatterjee, Krishnendu and Kovacs, Laura and Majumdar, Rupak M.},
  title =	{{Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461)}},
  pages =	{45--65},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{11},
  editor =	{Bjorner, Nikolaj and Chatterjee, Krishnendu and Kovacs, Laura and Majumdar, Rupak M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.11.45},
  URN =		{urn:nbn:de:0030-drops-39092},
  doi =		{10.4230/DagRep.2.11.45},
  annote =	{Keywords: Systems Engineering, Software Verification, Reactive Synthesis, Automated Deduction}
}
Document
DOI: 10.4230/DagRep.1.7.23
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272)

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Reports, Volume 1, Issue 7 (2011)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 11272 "Decision Procedures in Soft, Hard and Bio-ware (Follow Up)". It was held as a follow-on for a seminar 10161, of the same title, that took place in late April 2010 during the initial eruption of Eyjafjallajökull. In spite of the travel disruptions caused by the eruption of the volcano, the original seminar received a respectable turnout by European, mainly German and Italian participants. Unfortunately, the eruption hindered participation from overseas or even more distant parts of Europe. This caused the seminar to cover only part of the original objective. The follow-on seminar focused on the remaining objectives, in particular to bio-ware and constraint solving methods.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). In Dagstuhl Reports, Volume 1, Issue 7, pp. 23-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.1.7.23,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272)}},
  pages =	{23--35},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{7},
  editor =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.7.23},
  URN =		{urn:nbn:de:0030-drops-32775},
  doi =		{10.4230/DagRep.1.7.23},
  annote =	{Keywords: Hardware and Software Verification, Bio-analysis, Satisfiability Modulo Theories, Dynamic Symbolic Execution, Interpolants}
}
Document
DOI: 10.4230/DagSemProc.10161.1
10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)

Abstract
From April 19th, 2010 to April 23rd, 2010, the Dagstuhl Seminar 10161 "Decision Procedures in Soft, Hard and Bio-ware" was held in Schloss Dagstuhl Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as links to slides and links to papers behind the presentations and papers produced as a result of the seminar are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. 10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bjorner_et_al:DagSemProc.10161.1,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware}},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.1},
  URN =		{urn:nbn:de:0030-drops-27421},
  doi =		{10.4230/DagSemProc.10161.1},
  annote =	{Keywords: Decision Procedures, Satisfiability Modulo Theories, Software Verification, Dynamic Symbolic Execution, Interpolants, Hardware Verification, Bio-analysis}
}
Document
DOI: 10.4230/DagSemProc.10161.2
10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)

Abstract
The main goal of the seminar Decision Procedures in Soft, Hard and Bio-ware was to bring together renowned as well as young aspiring researchers from two groups. The first group formed by researchers who develop both theory and efficient implementations of decision procedures. The second group comprising of researchers from application areas such as program analysis and testing, crypto-analysis, hardware verification, industrial planning and scheduling, and bio-informatics, who have worked with, and contributed to, high quality decision procedures. The purpose of the seminar was to heighten awareness between tool and theory developers for decision procedures with the array of applications found in software, hardware and biological systems analysis.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. 10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bjorner_et_al:DagSemProc.10161.2,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware }},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.2},
  URN =		{urn:nbn:de:0030-drops-27369},
  doi =		{10.4230/DagSemProc.10161.2},
  annote =	{Keywords: Decision procedures, software, hardware, bioware}
}

Bjorner, Nikolaj S.

Document
DOI: 10.4230/DagRep.5.9.18
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381)

Authors: Nikolaj S. Bjorner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, and Christoph Weidenbach

Published in: Dagstuhl Reports, Volume 5, Issue 9 (2016)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15381 "Information from Deduction: Models and Proofs". The aim of the seminar was to bring together researchers working in deduction and applications that rely on models and proofs produced by deduction tools. Proofs and models serve two main purposes: (1) as an upcoming paradigm towards the next generation of automated deduction tools where search relies on (partial) proofs and models; (2) as the actual result of an automated deduction tool, which is increasingly integrated into application tools. Applications are rarely well served by a simple yes/no answer from a deduction tool. Many use models as certificates for satisfiability to extract feasible program executions; others use proof objects as certificates for unsatisfiability in the context of high-integrity systems development. Models and proofs even play an integral role within deductive tools as major methods for efficient proof search rely on refining a simultaneous search for a model or a proof. The topic is in a sense evergreen: models and proofs will always be an integral part of deduction. Nonetheless, the seminar was especially timely given recent activities in deduction and applications, and it enabled researchers from different subcommunities to communicate with each other towards exploiting synergies.
Cite as

Nikolaj S. Bjorner, Jasmin Christian Blanchette, Viorica Sofronie-Stokkermans, and Christoph Weidenbach. Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). In Dagstuhl Reports, Volume 5, Issue 9, pp. 18-37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.5.9.18,
  author =	{Bjorner, Nikolaj S. and Blanchette, Jasmin Christian and Sofronie-Stokkermans, Viorica and Weidenbach, Christoph},
  title =	{{Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381)}},
  pages =	{18--37},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{9},
  editor =	{Bjorner, Nikolaj S. and Blanchette, Jasmin Christian and Sofronie-Stokkermans, Viorica and Weidenbach, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.9.18},
  URN =		{urn:nbn:de:0030-drops-56830},
  doi =		{10.4230/DagRep.5.9.18},
  annote =	{Keywords: Automated Deduction, Program Verification, Certification}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact