@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} } @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} } @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.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} } @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.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} } @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} } @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.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} }