Published in: Dagstuhl Reports, Volume 1, Issue 7 (2011)
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)
@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-dev.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} }
Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)
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)
@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-dev.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} }
Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)
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)
@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-dev.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} }
Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)
Grant Olney Passmore, Leonardo de Moura, and Paul B. Jackson. Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{passmore_et_al:DagSemProc.10161.3, author = {Passmore, Grant Olney and de Moura, Leonardo and Jackson, Paul B.}, title = {{Gr\"{o}bner Basis Construction Algorithms Based on Theorem Proving Saturation Loops}}, booktitle = {Decision Procedures in Software, Hardware and Bioware}, pages = {1--17}, 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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.3}, URN = {urn:nbn:de:0030-drops-27345}, doi = {10.4230/DagSemProc.10161.3}, annote = {Keywords: Groebner bases, ideal theory, automated theorem proving, SMT solvers} }
Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)
Juergen Christ and Jochen Hoenicke. Instantiation-Based Interpolation for Quantified Formulae. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
@InProceedings{christ_et_al:DagSemProc.10161.4, author = {Christ, Juergen and Hoenicke, Jochen}, title = {{Instantiation-Based Interpolation for Quantified Formulae}}, booktitle = {Decision Procedures in Software, Hardware and Bioware}, pages = {1--12}, 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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.4}, URN = {urn:nbn:de:0030-drops-27355}, doi = {10.4230/DagSemProc.10161.4}, annote = {Keywords: Interpolation Quantifier SMT} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis. 07401 Abstracts Collection – Deduction and Decision Procedures. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{baader_et_al:DagSemProc.07401.1, author = {Baader, Franz and Cook, Byron and Giesl, J\"{u}rgen and Nieuwenhuis, Robert}, title = {{07401 Abstracts Collection – Deduction and Decision Procedures}}, booktitle = {Deduction and Decision Procedures}, pages = {1--20}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2007}, volume = {7401}, editor = {Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.1}, URN = {urn:nbn:de:0030-drops-12521}, doi = {10.4230/DagSemProc.07401.1}, annote = {Keywords: Decision Procedures, Deduction, Boolean Satisfiability, First-Order Logic, Integer Arithmetic, Combination of Theories, Satisfiability Modulo Theories Rewrite Systems, Formal Verification, Model Finding} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis. 07401 Executive Summary – Deduction and Decision Procedures. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{baader_et_al:DagSemProc.07401.2, author = {Baader, Franz and Cook, Byron and Giesl, J\"{u}rgen and Nieuwenhuis, Robert}, title = {{07401 Executive Summary – Deduction and Decision Procedures}}, booktitle = {Deduction and Decision Procedures}, pages = {1--3}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2007}, volume = {7401}, editor = {Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.2}, URN = {urn:nbn:de:0030-drops-12515}, doi = {10.4230/DagSemProc.07401.2}, annote = {Keywords: Formal Logic, Deduction, Artificial Intelligence} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
René Thiemann, Jürgen Giesl, and Peter Schneider-Kamp. Decision Procedures for Loop Detection. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{thiemann_et_al:DagSemProc.07401.3, author = {Thiemann, Ren\'{e} and Giesl, J\"{u}rgen and Schneider-Kamp, Peter}, title = {{Decision Procedures for Loop Detection}}, booktitle = {Deduction and Decision Procedures}, pages = {1--17}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2007}, volume = {7401}, editor = {Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.3}, URN = {urn:nbn:de:0030-drops-12469}, doi = {10.4230/DagSemProc.07401.3}, annote = {Keywords: Non-Termination, Decision Procedures, Term Rewriting, Dependency Pairs} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
Silvio Ghilardi, Silvio Ranise, Enrica Nicolini, and Daniele Zucchelli. From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{ghilardi_et_al:DagSemProc.07401.4, author = {Ghilardi, Silvio and Ranise, Silvio and Nicolini, Enrica and Zucchelli, Daniele}, title = {{From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems}}, booktitle = {Deduction and Decision Procedures}, pages = {1--2}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2007}, volume = {7401}, editor = {Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.4}, URN = {urn:nbn:de:0030-drops-12479}, doi = {10.4230/DagSemProc.07401.4}, annote = {Keywords: Non disjoint combination, linear temporal logic, model checking} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, and Harald Zankl. Implementing RPO and POLO using SAT. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{schneiderkamp_et_al:DagSemProc.07401.5, author = {Schneider-Kamp, Peter and Fuhs, Carsten and Thiemann, Ren\'{e} and Giesl, J\"{u}rgen and Annov, Elena and Codish, Michael and Middeldorp, Aart and Zankl, Harald}, title = {{Implementing RPO and POLO using SAT}}, booktitle = {Deduction and Decision Procedures}, pages = {1--10}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2007}, volume = {7401}, editor = {Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.5}, URN = {urn:nbn:de:0030-drops-12491}, doi = {10.4230/DagSemProc.07401.5}, annote = {Keywords: Termination, SAT, recursive path order, polynomial interpretation} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs. Local Theory Extensions, Hierarchical Reasoning and Applications to Verification. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{sofroniestokkermans_et_al:DagSemProc.07401.6, author = {Sofronie-Stokkermans, Viorica and Ihlemann, Carsten and Jacobs, Swen}, title = {{Local Theory Extensions, Hierarchical Reasoning and Applications to Verification}}, booktitle = {Deduction and Decision Procedures}, pages = {1--22}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2007}, volume = {7401}, editor = {Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.6}, URN = {urn:nbn:de:0030-drops-12507}, doi = {10.4230/DagSemProc.07401.6}, annote = {Keywords: Automated reasoning, Combinations of decision procedures, Verification} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, Stephan Swiderski, Manh Thang Nguyen, Daniel De Schreye, and Alexander Serebrenik. Termination of Programs using Term Rewriting and SAT Solving. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{giesl_et_al:DagSemProc.07401.7, author = {Giesl, J\"{u}rgen and Schneider-Kamp, Peter and Thiemann, Ren\'{e} and Swiderski, Stephan and Nguyen, Manh Thang and De Schreye, Daniel and Serebrenik, Alexander}, title = {{Termination of Programs using Term Rewriting and SAT Solving}}, booktitle = {Deduction and Decision Procedures}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2007}, volume = {7401}, editor = {Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.7}, URN = {urn:nbn:de:0030-drops-12481}, doi = {10.4230/DagSemProc.07401.7}, annote = {Keywords: Termination, Term Rewriting, Haskell, Prolog, SAT Solving} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov. 05431 Abstracts Collection – Deduction and Applications. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{baader_et_al:DagSemProc.05431.1, author = {Baader, Franz and Baumgartner, Peter and Nieuwenhuis, Robert and Voronkov, Andrei}, title = {{05431 Abstracts Collection – Deduction and Applications}}, booktitle = {Deduction and Applications}, pages = {1--23}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5431}, editor = {Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.1}, URN = {urn:nbn:de:0030-drops-5625}, doi = {10.4230/DagSemProc.05431.1}, annote = {Keywords: Formal logic, deduction, artificial intelligence} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Jörg Siekmann. Proof Presentation. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{siekmann:DagSemProc.05431.5, author = {Siekmann, J\"{o}rg}, title = {{Proof Presentation}}, booktitle = {Deduction and Applications}, pages = {1--7}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5431}, editor = {Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.5}, URN = {urn:nbn:de:0030-drops-5611}, doi = {10.4230/DagSemProc.05431.5}, annote = {Keywords: Artificial intelligence, mathematics, proof presentation} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov. 05431 Executive Summary – Deduction and Applications. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{baader_et_al:DagSemProc.05431.2, author = {Baader, Franz and Baumgartner, Peter and Nieuwenhuis, Robert and Voronkov, Andrei}, title = {{05431 Executive Summary – Deduction and Applications}}, booktitle = {Deduction and Applications}, pages = {1--3}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2006}, volume = {5431}, editor = {Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.2}, URN = {urn:nbn:de:0030-drops-5100}, doi = {10.4230/DagSemProc.05431.2}, annote = {Keywords: Formal logic, deduction, artificial intelligence} }
Feedback for Dagstuhl Publishing