6 Search Results for "Meredith, David"

Document
DOI: 10.4230/LIPIcs.FORC.2026.11
Limitations on Accurate, Trusted, Human-Level Reasoning

Authors: Rina Panigrahy and Vatsal Sharan

Published in: LIPIcs, Volume 368, 7th Symposium on Foundations of Responsible Computing (FORC 2026)

Abstract
We identify a fundamental incompatibility between the goals of accuracy, trust, and human-level reasoning in artificial intelligence (AI) systems, for strict mathematical definitions of these notions. We define accuracy of a system as the property that it never makes any false claims when it has the ability to abstain from making a prediction on any input, and trust as the assumption that the system is accurate. We define human-level reasoning as the property of an AI system always matching or exceeding human capability. Our core finding is that - for our formal definitions of these notions - an accurate and trusted AI system cannot be a human-level reasoning system: for such an accurate, trusted system there are task instances which are easily and provably solvable by a human but not by the system. Our proofs draw parallels to Gödel’s incompleteness theorems and Turing’s proof of the undecidability of the halting problem, and can be regarded as interpretations of Gödel’s and Turing’s results. Key to our proof is the formalization of the notion of trust, which allows us to separate the intrinsic property of a system (being accurate) from its epistemic status (being trusted).
Cite as

Rina Panigrahy and Vatsal Sharan. Limitations on Accurate, Trusted, Human-Level Reasoning. In 7th Symposium on Foundations of Responsible Computing (FORC 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 368, pp. 11:1-11:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{panigrahy_et_al:LIPIcs.FORC.2026.11,
  author =	{Panigrahy, Rina and Sharan, Vatsal},
  title =	{{Limitations on Accurate, Trusted, Human-Level Reasoning}},
  booktitle =	{7th Symposium on Foundations of Responsible Computing (FORC 2026)},
  pages =	{11:1--11:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-419-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{368},
  editor =	{Lin, Huijia (Rachel)},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FORC.2026.11},
  URN =		{urn:nbn:de:0030-drops-259840},
  doi =		{10.4230/LIPIcs.FORC.2026.11},
  annote =	{Keywords: Accuracy, Safety, Trust, Complexity-theoretic limitations}
}
Document
DOI: 10.4230/OASIcs.PARMA-DITAM.2026.3
High Performance Visualization with VisIVO Across Cloud and HPC

Authors: Umer Arshad, Eva Sciacca, Nicola Tuccari, Fabio Pitari, and Giuseppa Muscianisi

Published in: OASIcs, Volume 141, 17th Workshop on Parallel Programming and Run-Time Management Techniques for Many-Core Architectures and 15th Workshop on Design Tools and Architectures for Multicore Embedded Computing Platforms (PARMA-DITAM 2026)

Abstract
The rapid growth of data in Astrophysics and Cosmology creates significant challenges that require scalable computing and advanced visualization solutions. Cineca is Italy’s largest supercomputing center and a leading global provider of high-performance computing (HPC) services. This paper shows that the integration of the VisIVO scientific visualization framework is with the cloud-based InterActive Computing (IAC) service at Cineca. This integration enables GPU-accelerated, real-time visualization on HPC resources via a Jupyter interface in their browser. A new dedicated Python wrapper and a custom Jupyter kernel enable VisIVO to run smoothly from interactive notebooks, avoid command-line operations, and visualize data directly on HPC compute nodes. Furthermore, we enabled cloud-oriented RESTful APIs, built with the Flask framework, to perform VisIVO operations remotely via simple web services. This setup hides the backend’s complexity and simplifies connections with other applications. Our framework increases system accessibility, ensures reproducibility of results, and supports rapid data exploration for large astrophysical simulations. The system was evaluated using real-world cases, including visual analysis of cosmological simulations generated using the OpenGadget3 code. Results indicate that the system is scalable and reliable, and that it facilitates interactive scientific discovery on high-performance computing (HPC) infrastructures.
Cite as

Umer Arshad, Eva Sciacca, Nicola Tuccari, Fabio Pitari, and Giuseppa Muscianisi. High Performance Visualization with VisIVO Across Cloud and HPC. In 17th Workshop on Parallel Programming and Run-Time Management Techniques for Many-Core Architectures and 15th Workshop on Design Tools and Architectures for Multicore Embedded Computing Platforms (PARMA-DITAM 2026). Open Access Series in Informatics (OASIcs), Volume 141, pp. 3:1-3:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{arshad_et_al:OASIcs.PARMA-DITAM.2026.3,
  author =	{Arshad, Umer and Sciacca, Eva and Tuccari, Nicola and Pitari, Fabio and Muscianisi, Giuseppa},
  title =	{{High Performance Visualization with VisIVO Across Cloud and HPC}},
  booktitle =	{17th Workshop on Parallel Programming and Run-Time Management Techniques for Many-Core Architectures and 15th Workshop on Design Tools and Architectures for Multicore Embedded Computing Platforms (PARMA-DITAM 2026)},
  pages =	{3:1--3:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-416-1},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{141},
  editor =	{Baroffio, Davide and Busia, Paola and Denisov, Lev and Shukla, Nitin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.PARMA-DITAM.2026.3},
  URN =		{urn:nbn:de:0030-drops-256700},
  doi =		{10.4230/OASIcs.PARMA-DITAM.2026.3},
  annote =	{Keywords: High-performance computing, HPC, VisIVO, Scientific visualization, Interactive visualization, Cloud computing, Jupyter, Flask, REST API}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
Pearl/Brave New Idea
DOI: 10.4230/LIPIcs.ECOOP.2025.42
Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea)

Authors: Cameron Moy, Ryan Jung, and Matthias Felleisen

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Contract systems enable programmers to state specifications and have them enforced at run time. First-order contracts are expressed using ordinary code, while higher-order contracts are expressed using the notation familiar from type systems. Most interface descriptions, though, come with properties that involve not just assertions about single method calls, but entire call chains. Typical contract systems cannot express these specifications concisely. Such specifications demand domain-specific notations. In response, this paper proposes that contract systems abstract over the notation used for stating specifications. It presents an architecture for such a system, some illustrative examples, and an evaluation in terms of common notations from the literature.
Cite as

Cameron Moy, Ryan Jung, and Matthias Felleisen. Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 42:1-42:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{moy_et_al:LIPIcs.ECOOP.2025.42,
  author =	{Moy, Cameron and Jung, Ryan and Felleisen, Matthias},
  title =	{{Contract Systems Need Domain-Specific Notations}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{42:1--42:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.42},
  URN =		{urn:nbn:de:0030-drops-233348},
  doi =		{10.4230/LIPIcs.ECOOP.2025.42},
  annote =	{Keywords: software contracts, domain-specific languages}
}
Document
Vision
DOI: 10.4230/TGDK.1.1.3
Knowledge Engineering Using Large Language Models

Authors: Bradley P. Allen, Lise Stork, and Paul Groth

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Knowledge engineering is a discipline that focuses on the creation and maintenance of processes that generate and apply knowledge. Traditionally, knowledge engineering approaches have focused on knowledge expressed in formal languages. The emergence of large language models and their capabilities to effectively work with natural language, in its broadest sense, raises questions about the foundations and practice of knowledge engineering. Here, we outline the potential role of LLMs in knowledge engineering, identifying two central directions: 1) creating hybrid neuro-symbolic knowledge systems; and 2) enabling knowledge engineering in natural language. Additionally, we formulate key open research questions to tackle these directions.
Cite as

Bradley P. Allen, Lise Stork, and Paul Groth. Knowledge Engineering Using Large Language Models. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{allen_et_al:TGDK.1.1.3,
  author =	{Allen, Bradley P. and Stork, Lise and Groth, Paul},
  title =	{{Knowledge Engineering Using Large Language Models}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{3:1--3:19},
  ISSN =	{2942-7517},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.3},
  URN =		{urn:nbn:de:0030-drops-194777},
  doi =		{10.4230/TGDK.1.1.3},
  annote =	{Keywords: knowledge engineering, large language models}
}
Document
DOI: 10.4230/DagSemProc.06171.8
Point-set algorithms for pattern discovery and pattern matching in music

Authors: David Meredith

Published in: Dagstuhl Seminar Proceedings, Volume 6171, Content-Based Retrieval (2006)

Abstract
An algorithm that discovers the themes, motives and other perceptually significant repeated patterns in a musical work can be used, for example, in a music information retrieval system for indexing a collection of music documents so that it can be searched more rapidly. It can also be used in software tools for music analysis and composition and in a music transcription system or model of music cognition for discovering grouping structure, metrical structure and voice-leading structure. In most approaches to pattern discovery in music, the data is assumed to be in the form of strings. However, string-based methods become inefficient when one is interested in finding highly embellished occurrences of a query pattern or searching for polyphonic patterns in polyphonic music. These limitations can be avoided by representing the music as a set of points in a multidimensional Euclidean space. This point-set pattern matching approach allows the maximal repeated patterns in a passage of polyphonic music to be discovered in quadratic time and all occurrences of these patterns to be found in cubic time. More recently, Clifford et al. (2006) have shown that the best match for a query point set within a text point set of size n can be found in O(n log n) time by incorporating randomised projection, uniform hashing and FFT into the point-set pattern matching approach. Also, by using appropriate heuristics for selecting compact maximal repeated patterns with many non-overlapping occurrences, the point-set pattern discovery algorithms described here can be adapted for data compression. Moreover, the efficient encodings generated when this compression algorithm is run on music data seem to resemble the motivic-thematic analyses produced by human experts.
Cite as

David Meredith. Point-set algorithms for pattern discovery and pattern matching in music. In Content-Based Retrieval. Dagstuhl Seminar Proceedings, Volume 6171, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{meredith:DagSemProc.06171.8,
  author =	{Meredith, David},
  title =	{{Point-set algorithms for pattern discovery and pattern matching in music}},
  booktitle =	{Content-Based Retrieval},
  pages =	{1--23},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6171},
  editor =	{Tim Crawford and Remco C. Veltkamp},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06171.8},
  URN =		{urn:nbn:de:0030-drops-6525},
  doi =		{10.4230/DagSemProc.06171.8},
  annote =	{Keywords: Content-based music retrieval, point-set pattern matching}
}
  • Refine by Type
  • 6 Document/PDF
  • 5 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 2 2025
  • 1 2023
  • 1 2006

  • Refine by Author
  • 1 Aceto, Luca
  • 1 Achilleos, Antonis
  • 1 Allen, Bradley P.
  • 1 Arshad, Umer
  • 1 Attard, Duncan Paul
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 1 OASIcs
  • 1 TGDK
  • 1 DagSemProc

  • Refine by Classification
  • 2 Computing methodologies → Machine learning
  • 2 Computing methodologies → Philosophical/theoretical foundations of artificial intelligence
  • 1 Computing methodologies
  • 1 Computing methodologies → Natural language processing
  • 1 Software and its engineering → Domain specific languages
  • Show More...

  • Refine by Keyword
  • 1 Accuracy
  • 1 Cloud computing
  • 1 Complexity-theoretic limitations
  • 1 Content-based music retrieval
  • 1 Flask
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact