Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)
Bernd Becker, Luca Cardelli, Holger Hermanns, and Sofiene Tahar. 10271 Abstracts Collection – Verification over discrete-continuous boundaries. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{becker_et_al:DagSemProc.10271.1, author = {Becker, Bernd and Cardelli, Luca and Hermanns, Holger and Tahar, Sofiene}, title = {{10271 Abstracts Collection – Verification over discrete-continuous boundaries}}, booktitle = {Verification over discrete-continuous boundaries}, pages = {1--19}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10271}, editor = {Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.1}, URN = {urn:nbn:de:0030-drops-27922}, doi = {10.4230/DagSemProc.10271.1}, annote = {Keywords: Formal verification, cyber-physical systems, analog circuits, theorem proving, systems biology, mean-field methods} }
Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)
Erika Abraham, Florian Corzilius, Ulrich Loup, and Thomas Sturm. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{abraham_et_al:DagSemProc.10271.2, author = {Abraham, Erika and Corzilius, Florian and Loup, Ulrich and Sturm, Thomas}, title = {{A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra}}, booktitle = {Verification over discrete-continuous boundaries}, pages = {1--9}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10271}, editor = {Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.2}, URN = {urn:nbn:de:0030-drops-27907}, doi = {10.4230/DagSemProc.10271.2}, annote = {Keywords: SMT-solving, Real Algebra, Hybrid Systems, Verification, Synthesis} }
Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)
Michael Brickenstein and Alexander Dreyer. Network-driven Boolean Normal Forms. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{brickenstein_et_al:DagSemProc.10271.3, author = {Brickenstein, Michael and Dreyer, Alexander}, title = {{Network-driven Boolean Normal Forms}}, booktitle = {Verification over discrete-continuous boundaries}, pages = {1--8}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10271}, editor = {Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.3}, URN = {urn:nbn:de:0030-drops-27894}, doi = {10.4230/DagSemProc.10271.3}, annote = {Keywords: Groebner, normal forms, Boolean polynomials, cryptanalysis, verification} }
Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)
Florian Schupfer and Christoph Grimm. Towards more Dependable Verification of Mixed-Signal Systems. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{schupfer_et_al:DagSemProc.10271.4, author = {Schupfer, Florian and Grimm, Christoph}, title = {{Towards more Dependable Verification of Mixed-Signal Systems}}, booktitle = {Verification over discrete-continuous boundaries}, pages = {1--13}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10271}, editor = {Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.4}, URN = {urn:nbn:de:0030-drops-27911}, doi = {10.4230/DagSemProc.10271.4}, annote = {Keywords: Affine Arithmetic, Range based methods, Verification, Semi-symbolic simulation} }
Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)
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)
@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} }
Published in: OASIcs, Volume 4, 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06) (2006)
Jan Reineke, Björn Wachter, Stefan Thesing, Reinhard Wilhelm, Ilia Polian, Jochen Eisinger, and Bernd Becker. A Definition and Classification of Timing Anomalies. In 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06). Open Access Series in Informatics (OASIcs), Volume 4, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{reineke_et_al:OASIcs.WCET.2006.671, author = {Reineke, Jan and Wachter, Bj\"{o}rn and Thesing, Stefan and Wilhelm, Reinhard and Polian, Ilia and Eisinger, Jochen and Becker, Bernd}, title = {{A Definition and Classification of Timing Anomalies}}, booktitle = {6th International Workshop on Worst-Case Execution Time Analysis (WCET'06)}, pages = {1--6}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-939897-03-3}, ISSN = {2190-6807}, year = {2006}, volume = {4}, editor = {Mueller, Frank}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2006.671}, URN = {urn:nbn:de:0030-drops-6713}, doi = {10.4230/OASIcs.WCET.2006.671}, annote = {Keywords: Timing analysis, Worst-case execution time, Timing anomalies, Scheduling Anomalies, Abstraction} }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
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)
@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}, }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
Bernd Becker, Christoph Meinel, Shin-Ichi Minato, and Fabio Somenzi. Computer Aided Design and Test Decision Diagrams - Concepts and Applications (Dagstuhl Seminar 99041). Dagstuhl Seminar Report 229, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1999)
@TechReport{becker_et_al:DagSemRep.229, author = {Becker, Bernd and Meinel, Christoph and Minato, Shin-Ichi and Somenzi, Fabio}, title = {{Computer Aided Design and Test Decision Diagrams - Concepts and Applications (Dagstuhl Seminar 99041)}}, pages = {1--16}, ISSN = {1619-0203}, year = {1999}, type = {Dagstuhl Seminar Report}, number = {229}, 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.229}, URN = {urn:nbn:de:0030-drops-151155}, doi = {10.4230/DagSemRep.229}, }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
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)
@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}, }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
Bernd Becker, Randy Bryant, Oliver Coudert, and Christoph Meinel. Computer Aided Design and Test (Dagstuhl Seminar 9507). Dagstuhl Seminar Report 105, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1995)
@TechReport{becker_et_al:DagSemRep.105, author = {Becker, Bernd and Bryant, Randy and Coudert, Oliver and Meinel, Christoph}, title = {{Computer Aided Design and Test (Dagstuhl Seminar 9507)}}, pages = {1--24}, ISSN = {1619-0203}, year = {1995}, type = {Dagstuhl Seminar Report}, number = {105}, 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.105}, URN = {urn:nbn:de:0030-drops-149934}, doi = {10.4230/DagSemRep.105}, }
Feedback for Dagstuhl Publishing