LIPIcs, Volume 82
CSL 2017, August 20-24, 2017, Stockholm, Sweden
Editors: Valentin Goranko and Mads Dam
Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Serenella Cerrito, Valentin Goranko, and Sophie Paillocher. Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 23:1-23:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{cerrito_et_al:LIPIcs.FSCD.2023.23, author = {Cerrito, Serenella and Goranko, Valentin and Paillocher, Sophie}, title = {{Partial Model Checking and Partial Model Synthesis in LTL Using a Tableau-Based Approach}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {23:1--23:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.23}, URN = {urn:nbn:de:0030-drops-180075}, doi = {10.4230/LIPIcs.FSCD.2023.23}, annote = {Keywords: Linear temporal logic LTL, partial transition systems, partial model checking, partial model synthesis, tableaux} }
Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)
Serenella Cerrito, Amélie David, and Valentin Goranko. Minimisation of Models Satisfying CTL Formulas. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 13:1-13:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{cerrito_et_al:LIPIcs.TIME.2019.13, author = {Cerrito, Serenella and David, Am\'{e}lie and Goranko, Valentin}, title = {{Minimisation of Models Satisfying CTL Formulas}}, booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)}, pages = {13:1--13:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-127-6}, ISSN = {1868-8969}, year = {2019}, volume = {147}, editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.13}, URN = {urn:nbn:de:0030-drops-113718}, doi = {10.4230/LIPIcs.TIME.2019.13}, annote = {Keywords: CTL, model minimisation, bisimulation reduction, tableaux-based reduction} }
Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)
Valentin Goranko, Antti Kuusisto, and Raine Rönnholm. CTL with Finitely Bounded Semantics. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 14:1-14:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{goranko_et_al:LIPIcs.TIME.2017.14, author = {Goranko, Valentin and Kuusisto, Antti and R\"{o}nnholm, Raine}, title = {{CTL with Finitely Bounded Semantics}}, booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)}, pages = {14:1--14:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-052-1}, ISSN = {1868-8969}, year = {2017}, volume = {90}, editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.14}, URN = {urn:nbn:de:0030-drops-79325}, doi = {10.4230/LIPIcs.TIME.2017.14}, annote = {Keywords: CTL, finitely bounded semantics, tableaux, decidability} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Valentin Goranko and Mads Dam. LIPIcs, Volume 82, CSL'17, Complete Volume. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@Proceedings{goranko_et_al:LIPIcs.CSL.2017, title = {{LIPIcs, Volume 82, CSL'17, Complete Volume}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017}, URN = {urn:nbn:de:0030-drops-78103}, doi = {10.4230/LIPIcs.CSL.2017}, annote = {Keywords: Conference Proceedings, Software/Program Verification, Formal Definitions and Theory, Language Constructs and Features, Theory of Computation} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Valentin Goranko and Mads Dam. Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 0:i-0:xviii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{goranko_et_al:LIPIcs.CSL.2017.0, author = {Goranko, Valentin and Dam, Mads}, title = {{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {0:i--0:xviii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.0}, URN = {urn:nbn:de:0030-drops-76671}, doi = {10.4230/LIPIcs.CSL.2017.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Anuj Dawar and Daniel Leivant. The Ackermann Award 2017. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 1:1-1:4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{dawar_et_al:LIPIcs.CSL.2017.1, author = {Dawar, Anuj and Leivant, Daniel}, title = {{The Ackermann Award 2017}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {1:1--1:4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.1}, URN = {urn:nbn:de:0030-drops-76938}, doi = {10.4230/LIPIcs.CSL.2017.1}, annote = {Keywords: Ackermann Award, jury report, citation} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Phokion G. Kolaitis. Schema Mappings: Structural Properties and Limits (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{kolaitis:LIPIcs.CSL.2017.2, author = {Kolaitis, Phokion G.}, title = {{Schema Mappings: Structural Properties and Limits}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.2}, URN = {urn:nbn:de:0030-drops-76707}, doi = {10.4230/LIPIcs.CSL.2017.2}, annote = {Keywords: logic and databases, schema mappings, data exchange, metric spaces} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Laura Kovács. First-Order Interpolation and Grey Areas of Proofs (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 3:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{kovacs:LIPIcs.CSL.2017.3, author = {Kov\'{a}cs, Laura}, title = {{First-Order Interpolation and Grey Areas of Proofs}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {3:1--3:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.3}, URN = {urn:nbn:de:0030-drops-76912}, doi = {10.4230/LIPIcs.CSL.2017.3}, annote = {Keywords: theorem proving, interpolation, proof transformations, constraint solving, program analysis} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Stephan Kreutzer. Current Trends and New Perspectives for First-Order Model Checking (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 4:1-4:5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{kreutzer:LIPIcs.CSL.2017.4, author = {Kreutzer, Stephan}, title = {{Current Trends and New Perspectives for First-Order Model Checking}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {4:1--4:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.4}, URN = {urn:nbn:de:0030-drops-77095}, doi = {10.4230/LIPIcs.CSL.2017.4}, annote = {Keywords: Finite Model Theory, Computational Model Theory, Algorithmic Meta Theorems, Model-Checking, Logical Approaches in Graph Theory} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Meena Mahajan. Arithmetic Circuits: An Overview (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 5:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{mahajan:LIPIcs.CSL.2017.5, author = {Mahajan, Meena}, title = {{Arithmetic Circuits: An Overview}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {5:1--5:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.5}, URN = {urn:nbn:de:0030-drops-76858}, doi = {10.4230/LIPIcs.CSL.2017.5}, annote = {Keywords: algebraic complexity, circuits, formulas, branching programs, determinant, permanent} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Wolfgang Thomas. Determinacy of Infinite Games: Perspectives of the Algorithmic Approach (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 6:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{thomas:LIPIcs.CSL.2017.6, author = {Thomas, Wolfgang}, title = {{Determinacy of Infinite Games: Perspectives of the Algorithmic Approach}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {6:1--6:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.6}, URN = {urn:nbn:de:0030-drops-77083}, doi = {10.4230/LIPIcs.CSL.2017.6}, annote = {Keywords: Infinite games, descriptive set theory, automata theory, transducers, automatic synthesis} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Margus Veanes. Symbolic Automata Theory with Applications (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 7:1-7:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{veanes:LIPIcs.CSL.2017.7, author = {Veanes, Margus}, title = {{Symbolic Automata Theory with Applications}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {7:1--7:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.7}, URN = {urn:nbn:de:0030-drops-76872}, doi = {10.4230/LIPIcs.CSL.2017.7}, annote = {Keywords: automaton, transducer, symbolic} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 8:1-8:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{ahrens_et_al:LIPIcs.CSL.2017.8, author = {Ahrens, Benedikt and Lumsdaine, Peter LeFanu and Voevodsky, Vladimir}, title = {{Categorical Structures for Type Theory in Univalent Foundations}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.8}, URN = {urn:nbn:de:0030-drops-76960}, doi = {10.4230/LIPIcs.CSL.2017.8}, annote = {Keywords: Categorical Semantics, Type Theory, Univalence Axiom} }
Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing Cycles from Proofs. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 9:1-9:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{alertubella_et_al:LIPIcs.CSL.2017.9, author = {Aler Tubella, Andrea and Guglielmi, Alessio and Ralph, Benjamin}, title = {{Removing Cycles from Proofs}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {9:1--9:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.9}, URN = {urn:nbn:de:0030-drops-77008}, doi = {10.4230/LIPIcs.CSL.2017.9}, annote = {Keywords: proof theory, deep inference, proof complexity} }
Feedback for Dagstuhl Publishing