Search Results

Documents authored by Drechsler, Rolf

Document
DOI: 10.4230/DagSemProc.09461.1
09461 Abstracts Collection – Algorithms and Applications for Next Generation SAT Solvers

Authors: Bernd Becker, Valeria Bertacco, Rolf Drechsler, and Masahiro Fujita

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract
From 8th to 13th November 2009, the Dagstuhl Seminar 09461 "Algorithms and Applications for Next Generation SAT Solvers" 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 abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts, slides or full papers are provided, if available.
Cite as

Bernd Becker, Valeria Bertacco, Rolf Drechsler, and Masahiro Fujita. 09461 Abstracts Collection – Algorithms and Applications for Next Generation SAT Solvers. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:DagSemProc.09461.1,
  author =	{Becker, Bernd and Bertacco, Valeria and Drechsler, Rolf and Fujita, Masahiro},
  title =	{{09461 Abstracts Collection – Algorithms and Applications for Next Generation SAT Solvers}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.1},
  URN =		{urn:nbn:de:0030-drops-25113},
  doi =		{10.4230/DagSemProc.09461.1},
  annote =	{Keywords: Boolean Satisfiability, Formal Methods, Word Level, Quantification, Multithreading}
}
Document
DOI: 10.4230/DagSemProc.09461.2
Formal Verification of Abstract SystemC Models

Authors: Daniel Grosse, Hoang M. Le, and Rolf Drechsler

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract
In this paper we present a formal verification approach for abstract SystemC models. The approach allows checking expressive properties and lifts induction known from bounded model checking to a higher level, to cope with the large state space of abstract SystemC programs. The technique is tightly integrated with our SystemC to C transformation and generation of monitoring logic to form a complete and efficient method. Properties specifying both hardware and software aspects, e.g. pre- and post-conditions as well as temporal relations of transactions and events, can be specified. As shown by experiments modern proof techniques allow verifying important non-trivial behavior. Moreover, our inductive technique gives significant speed-ups in comparison to simple methods.
Cite as

Daniel Grosse, Hoang M. Le, and Rolf Drechsler. Formal Verification of Abstract SystemC Models. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{grosse_et_al:DagSemProc.09461.2,
  author =	{Grosse, Daniel and Le, Hoang M. and Drechsler, Rolf},
  title =	{{Formal Verification of Abstract SystemC Models}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.2},
  URN =		{urn:nbn:de:0030-drops-25102},
  doi =		{10.4230/DagSemProc.09461.2},
  annote =	{Keywords: SystemC, TLM, BMC, SAT, SMT}
}
Document
DOI: 10.4230/DagSemProc.09461.5
SWORD – Module-based SAT Solving

Authors: Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract
In the paper, SWORD is described – a decision procedure for bit-vector logic that uses SAT techniques and exploits word level information. The main idea of SWORD is based on the following observation: While current SAT solvers perform very well on instances with a large number of logic operations, their performance on arithmetic operations degrades with increasing data-path width. In contrast, pure word-level approaches are able to handle arithmetic operations very fast, but suffer from irregularities in the word-level structure (e.g. bit slicing). SWORD tries to combine the best of both worlds: On the one hand, it includes fast propagation, sophisticated data structures, as well as advanced techniques like non-chronological backtracking and learning from modern SAT solvers. On the other hand word-level information is exploited in the decision heuristic and during propagation.
Cite as

Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler. SWORD – Module-based SAT Solving. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{wille_et_al:DagSemProc.09461.5,
  author =	{Wille, Robert and Jung, Jean Christoph and S\"{u}lflow, Andre and Drechsler, Rolf},
  title =	{{SWORD – Module-based SAT Solving}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.5},
  URN =		{urn:nbn:de:0030-drops-25069},
  doi =		{10.4230/DagSemProc.09461.5},
  annote =	{Keywords: SAT Solver, Word Level, SAT Modulo Theories}
}
Document
DOI: 10.4230/DagSemProc.08351.6
SAT-based Automatic Test Pattern Generation

Authors: Rolf Drechsler, Stephan Eggersglüß, Görschwin Fey, and Daniel Tille

Published in: Dagstuhl Seminar Proceedings, Volume 8351, Evolutionary Test Generation (2009)

Abstract
Due to the rapidly growing size of integrated circuits, there is a need for new algorithms for Automatic Test Pattern Generation (ATPG). While classical algorithms reach their limit, there have been recent advances in algorithms to solve Boolean Satisfiability (SAT). Because Boolean SAT solvers are working on Conjunctive Normal Forms (CNF), the problem has to be transformed. During transformation, relevant information about the problem might get lost and therefore is not available in the solving process. In the following we briefly motivate the problem and provide the latest developments in the field. The technique was implemented and experimental results are presented. The approach was combined with the ATPG framework of NXP Semiconductors. Significant improvements in overall performance and robustness are demonstrated.
Cite as

Rolf Drechsler, Stephan Eggersglüß, Görschwin Fey, and Daniel Tille. SAT-based Automatic Test Pattern Generation. In Evolutionary Test Generation. Dagstuhl Seminar Proceedings, Volume 8351, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{drechsler_et_al:DagSemProc.08351.6,
  author =	{Drechsler, Rolf and Eggersgl\"{u}{\ss}, Stephan and Fey, G\"{o}rschwin and Tille, Daniel},
  title =	{{SAT-based Automatic Test Pattern Generation}},
  booktitle =	{Evolutionary Test Generation},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{8351},
  editor =	{Holger Schlingloff and Tanja E. J. Vos and Joachim Wegener},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08351.6},
  URN =		{urn:nbn:de:0030-drops-20152},
  doi =		{10.4230/DagSemProc.08351.6},
  annote =	{Keywords: Circuit, ATPG, SAT, Boolean Satisfiability}
}
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