Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23, author = {Jackson, Vincent and Murray, Toby and Rizkallah, Christine}, title = {{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23}, URN = {urn:nbn:de:0030-drops-207510}, doi = {10.4230/LIPIcs.ITP.2024.23}, annote = {Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras} }
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.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.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.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.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.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.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.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} }
Feedback for Dagstuhl Publishing