9 Search Results for "Fujita, Masahiro"


Document
Verifying Reliability (Dagstuhl Seminar 12341)

Authors: Görschwin Fey, Masahiro Fujita, Natasa Miskov-Zivanov, Kaushik Roy, and Matteo Sonza Reorda

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


Abstract
Moore's law has been the driving force behind the increasing computing power of today's devices which is based on shrinking feature sizes. This shrinking process makes future devices extremely susceptible to soft errors due to, e.g., external influences like environmental radiation and internal issues like stress effects, aging and process variation. For future technology nodes "Designing reliable systems from unreliable components".

Cite as

Görschwin Fey, Masahiro Fujita, Natasa Miskov-Zivanov, Kaushik Roy, and Matteo Sonza Reorda. Verifying Reliability (Dagstuhl Seminar 12341). In Dagstuhl Reports, Volume 2, Issue 8, pp. 54-73, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@Article{fey_et_al:DagRep.2.8.57,
  author =	{Fey, G\"{o}rschwin and Fujita, Masahiro and Miskov-Zivanov, Natasa and Roy, Kaushik and Sonza Reorda, Matteo},
  title =	{{Verifying Reliability (Dagstuhl Seminar 12341)}},
  pages =	{54--73},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2012},
  volume =	{2},
  number =	{8},
  editor =	{Fey, G\"{o}rschwin and Fujita, Masahiro and Miskov-Zivanov, Natasa and Roy, Kaushik and Sonza Reorda, Matteo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.2.8.57},
  URN =		{urn:nbn:de:0030-drops-37830},
  doi =		{10.4230/DagRep.2.8.57},
  annote =	{Keywords: Reliability, fault modeling, formal methods}
}
Document
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-dev.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
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-dev.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
SMT-Solving for the First-Order Theory of the Reals

Authors: Erika Abraham and Ulrich Loup

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


Abstract
SAT-solving is a highly actual research area with increasing success and plenty of industrial applications. SMT-solving, extending SAT with theories, has its main focus on linear real constrains. However, there are only few solvers going further to more expressive but still decidable logics like the first-order theory of the reals with addition and multiplication. The main requests on theory solvers that must be fulfilled for their efficient embedding into an SMT solver are (a) incrementality, (b) the efficient computation of minimal infeasible subsets, and (c) the support of backtracking. For the first-order theory of the reals we are not aware of any solver offering those functionalities. In this work we address the possibilities to extend existing theory solving algorithms to come up with a theory solver suited for SMT.

Cite as

Erika Abraham and Ulrich Loup. SMT-Solving for the First-Order Theory of the Reals. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{abraham_et_al:DagSemProc.09461.3,
  author =	{Abraham, Erika and Loup, Ulrich},
  title =	{{SMT-Solving for the First-Order Theory of the Reals}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--7},
  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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.3},
  URN =		{urn:nbn:de:0030-drops-25081},
  doi =		{10.4230/DagSemProc.09461.3},
  annote =	{Keywords: SMT-solving, first-order theory of the reals, verification}
}
Document
Solving hard instances in QF-BV combining Boolean reasoning with computer algebra

Authors: Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz

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


Abstract
This paper describes our new satisfyability (SAT) modulo theory (SMT) solver STABLE for the quantifier-free logic over fixed size bit vectors. Our main application domain is formal verification of system-on-chip (SoC) modules designed for complex computational tasks, for example, in signal processing applications. Ensuring proper functional behavior for such modules, including arithmetic correctness of the data paths, is considered a very difficult problem. We show how methods from computer algebra can be integrated into an SMT solver such that instances can be handled where the arithmetic problem parts are specified mixing various levels of abstraction from the plain gate level for small highly optimized components up to the pure word level used in high-level specifications. If the arithmetic problem parts include multiplications such mixed problem descriptions quickly drive current SMT solvers towards their capacity limits. High performance data paths are often designed at a level of abstraction that we call the arithmetic bit level (ABL). We show how ABL information, if available in an SMT instance, can be used to transform the decision problem into an equivalent set of variety subset problems. These problems can be solved efficiently with techniques from computer algebra based on Gröbner basis theory over finite rings Z/2^n . Sometimes, instances contain problem parts at a level below the ABL using gate-level operations. These problem parts, e.g., originate from custom-designed arithmetic components that are highly optimized using the gate-level constructs of a hardware description language (HDL). For such cases we integrate a local ABL extraction technique based on local Reed-Muller forms.

Cite as

Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz. Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{wedler_et_al:DagSemProc.09461.4,
  author =	{Wedler, Markus and Pavlenko, Evgeny and Dreyer, Alexander and Seelisch, Frank and Stoffel, Dominik and Greuel, Gert-Martin and Kunz, Wolfgang},
  title =	{{Solving hard instances in QF-BV combining Boolean reasoning with computer algebra}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--20},
  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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.4},
  URN =		{urn:nbn:de:0030-drops-25096},
  doi =		{10.4230/DagSemProc.09461.4},
  annote =	{Keywords: SAT modulo Theory, Quantifier Free logic over fixed sized bitvectors; Computer Algebra}
}
Document
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-dev.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
Towards Model Validation and Verification with SAT Techniques

Authors: Martin Gogolla

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


Abstract
After sketching how system development and the UML (Unified Modeling Language) and the OCL (Object Constraint Language) are related, validation and verification with the tool USE (UML-based Specification Environment) is demonstrated. As a more efficient alternative for verification tasks, two approaches using SAT-based techniques are put forward: First, a direct encoding of UML and OCL with Boolean variables and propositional formulas, and second, an encoding employing an intermediate, higher-level language (KODKOD, stongly connected to ALLOY). A number of further, presently not realized verification and validation tasks and the transformation of higher-level modeling concepts into simple UML/OCL models, which are checkable with SAT-based techniques, are shortly discussed. Finally, the potential of SAT-based techniques for model development is again emphasized.

Cite as

Martin Gogolla. Towards Model Validation and Verification with SAT Techniques. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{gogolla:DagSemProc.09461.6,
  author =	{Gogolla, Martin},
  title =	{{Towards Model Validation and Verification with SAT Techniques}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--11},
  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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.6},
  URN =		{urn:nbn:de:0030-drops-25078},
  doi =		{10.4230/DagSemProc.09461.6},
  annote =	{Keywords: UML, OCL, Invariant, Pre- and postcondition, Model validation, Model verification}
}
Document
Computer Aided Design and Test - BDDs versus SAT (Dagstuhl Seminar 01051)

Authors: Bernd Becker, Masahiro Fujita, Christoph Meinel, and Fabio Somenzi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Bernd Becker, Masahiro Fujita, Christoph Meinel, and Fabio Somenzi. Computer Aided Design and Test - BDDs versus SAT (Dagstuhl Seminar 01051). Dagstuhl Seminar Report 297, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)


Copy BibTex To Clipboard

@TechReport{becker_et_al:DagSemRep.297,
  author =	{Becker, Bernd and Fujita, Masahiro and Meinel, Christoph and Somenzi, Fabio},
  title =	{{Computer Aided Design and Test - BDDs versus SAT (Dagstuhl Seminar 01051)}},
  pages =	{1--25},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{297},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.297},
  URN =		{urn:nbn:de:0030-drops-151811},
  doi =		{10.4230/DagSemRep.297},
}
Document
Computer Aided Design and Test Decision Diagrams - Concepts and Applications (Dagstuhl Seminar 9705)

Authors: Bernd Becker, Randy Bryant, Masahiro Fujita, and Christoph Meinel

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)


Abstract

Cite as

Bernd Becker, Randy Bryant, Masahiro Fujita, and Christoph Meinel. Computer Aided Design and Test Decision Diagrams - Concepts and Applications (Dagstuhl Seminar 9705). Dagstuhl Seminar Report 166, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1997)


Copy BibTex To Clipboard

@TechReport{becker_et_al:DagSemRep.166,
  author =	{Becker, Bernd and Bryant, Randy and Fujita, Masahiro and Meinel, Christoph},
  title =	{{Computer Aided Design and Test Decision Diagrams - Concepts and Applications (Dagstuhl Seminar 9705)}},
  pages =	{1--18},
  ISSN =	{1619-0203},
  year =	{1997},
  type = 	{Dagstuhl Seminar Report},
  number =	{166},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.166},
  URN =		{urn:nbn:de:0030-drops-150539},
  doi =		{10.4230/DagSemRep.166},
}
  • Refine by Author
  • 4 Fujita, Masahiro
  • 3 Becker, Bernd
  • 3 Drechsler, Rolf
  • 2 Meinel, Christoph
  • 1 Abraham, Erika
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Word Level
  • 1 BMC
  • 1 Boolean Satisfiability
  • 1 Formal Methods
  • 1 Invariant
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 6 2010
  • 1 1997
  • 1 2001
  • 1 2012

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