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 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} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Deepak Kapur. Automatically Generating Loop Invariants Using Quantifier Elimination. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{kapur:DagSemProc.05431.3, author = {Kapur, Deepak}, title = {{Automatically Generating Loop Invariants Using Quantifier Elimination}}, booktitle = {Deduction and Applications}, pages = {1--17}, 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.3}, URN = {urn:nbn:de:0030-drops-5116}, doi = {10.4230/DagSemProc.05431.3}, annote = {Keywords: Program verification, loop invariants, inductive assertions, quantifier elimination} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Viktor Kuncak, Martin Rinard, and Bruno Marnette. On Algorithms and Complexity for Sets with Cardinality Constraints. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{kuncak_et_al:DagSemProc.05431.4, author = {Kuncak, Viktor and Rinard, Martin and Marnette, Bruno}, title = {{On Algorithms and Complexity for Sets with Cardinality Constraints}}, booktitle = {Deduction and Applications}, 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.4}, URN = {urn:nbn:de:0030-drops-5125}, doi = {10.4230/DagSemProc.05431.4}, annote = {Keywords: Static analysis, data structure consistency, program verification, decision procedures} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. Proving and Disproving Termination in the Dependency Pair Framework. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{giesl_et_al:DagSemProc.05431.6, author = {Giesl, J\"{u}rgen and Thiemann, Ren\'{e} and Schneider-Kamp, Peter}, title = {{Proving and Disproving Termination in the Dependency Pair Framework}}, booktitle = {Deduction and Applications}, pages = {1--1}, 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.6}, URN = {urn:nbn:de:0030-drops-5091}, doi = {10.4230/DagSemProc.05431.6}, annote = {Keywords: Termination, non-termination, term rewriting, dependency pairs} }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
Deepak Kapur, Andreas Podelski, and Andrei Voronkov. Deduction and Infinite-state Model Checking (Dagstuhl Seminar 03171). Dagstuhl Seminar Report 376, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)
@TechReport{kapur_et_al:DagSemRep.376, author = {Kapur, Deepak and Podelski, Andreas and Voronkov, Andrei}, title = {{Deduction and Infinite-state Model Checking (Dagstuhl Seminar 03171)}}, pages = {1--5}, ISSN = {1619-0203}, year = {2003}, type = {Dagstuhl Seminar Report}, number = {376}, 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.376}, URN = {urn:nbn:de:0030-drops-152564}, doi = {10.4230/DagSemRep.376}, }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
Hendrik Decker, Jorge Bocca, Michael Kifer, and Andrei Voronkov. Logic Databases and the Meaning of Change (Dagstuhl Seminar 9639). Dagstuhl Seminar Report 157, pp. 1-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1997)
@TechReport{decker_et_al:DagSemRep.157, author = {Decker, Hendrik and Bocca, Jorge and Kifer, Michael and Voronkov, Andrei}, title = {{Logic Databases and the Meaning of Change (Dagstuhl Seminar 9639)}}, pages = {1--31}, ISSN = {1619-0203}, year = {1997}, type = {Dagstuhl Seminar Report}, number = {157}, 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.157}, URN = {urn:nbn:de:0030-drops-150449}, doi = {10.4230/DagSemRep.157}, }
Feedback for Dagstuhl Publishing