4 Search Results for "Adams, Bram"

Document
DOI: 10.4230/LIPIcs.ITP.2025.35
Verifying an Efficient Algorithm for Computing Bernoulli Numbers

Authors: Manuel Eberl and Peter Lammich

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The Bernoulli numbers B_k are a sequence of rational numbers that is ubiquitous in mathematics, but difficult to compute efficiently (compared to e.g. approximating π). In 2008, Harvey gave the currently fastest known practical way for computing them: his algorithm computes B_k mod p in time O(p log^{1 + o(1)} p). By doing this for O(k) many small primes p in parallel and then combining the results with the Chinese Remainder Theorem, one recovers the value of B_k as a rational number in O(k² log^{2 + o(1)} k) time. One advantage of this approach is that the expensive part of the algorithm is highly parallelisable and has very low memory requirements. This algorithm still holds the world record with its computation of B_{10⁸}. We give a verified efficient LLVM implementation of this algorithm. This was achieved by formalising the necessary mathematical background theory in Isabelle/HOL, proving an abstract version of the algorithm correct, and refining this abstract version down to LLVM using Lammich’s Isabelle-LLVM framework, including many low-level optimisations. The performance of the resulting LLVM code is comparable with Harvey’s original unverified and hand-optimised C++ implementation.
Cite as

Manuel Eberl and Peter Lammich. Verifying an Efficient Algorithm for Computing Bernoulli Numbers. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{eberl_et_al:LIPIcs.ITP.2025.35,
  author =	{Eberl, Manuel and Lammich, Peter},
  title =	{{Verifying an Efficient Algorithm for Computing Bernoulli Numbers}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.35},
  URN =		{urn:nbn:de:0030-drops-246331},
  doi =		{10.4230/LIPIcs.ITP.2025.35},
  annote =	{Keywords: Bernoulli numbers, LLVM, verification, Isabelle, Chinese remainder theorem, modular arithmetic, Montgomery arithmetic}
}
Document
DOI: 10.4230/LIPIcs.GIScience.2025.14
Guiding Geospatial Analysis Processes in Dealing with Modifiable Areal Unit Problems

Authors: Guoray Cai and Yue Hao

Published in: LIPIcs, Volume 346, 13th International Conference on Geographic Information Science (GIScience 2025)

Abstract
Geospatial analysis has been widely applied in different domains for critical decision making. However, the results of spatial analysis are often plagued with uncertainties due to measurement errors, choice of data representations, and unintended transformation artifacts. A well known example of such problems is the Modifiable Areal Unit Problem (MAUP) which has well documented effects on the outcome of spatial analysis on area-aggregated data. Existing methods for addressing the effects of MAUP are limited, are technically complex, and are often inaccessible to practitioners. As a result, analysts tend to ignore the effects of MAUP in practice due to lack of expertise, high cognitive loads, and resource limitations. To address these challenges, this paper proposes a machine-guidance approach to augment the analyst’s capacity in mitigating the effect of MAUP. Based on an analysis of practical challenges faced by human analysts, we identified multiple opportunities for the machine to guide the analysts by alerting to the rise of MAUP, assessing the impact of MAUP, choosing mitigation methods, and generating visual guidance messages using GIS functions and tools. For each of the opportunities, we characterize the behavior patterns and the underlying guidance strategies that generate the behavior. We illustrate the behavior of machine guidance using a hotspot analysis scenario in the context of crime policing, where MAUP has strong effects on the patterns of crime hotspots. Finally, we describe the computational framework used to build a prototype guidance system and identify a number of research questions to be addressed. We conclude by discussing how the machine guidance approach could be an answer to some of the toughest problems in geospatial analysis.
Cite as

Guoray Cai and Yue Hao. Guiding Geospatial Analysis Processes in Dealing with Modifiable Areal Unit Problems. In 13th International Conference on Geographic Information Science (GIScience 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 346, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cai_et_al:LIPIcs.GIScience.2025.14,
  author =	{Cai, Guoray and Hao, Yue},
  title =	{{Guiding Geospatial Analysis Processes in Dealing with Modifiable Areal Unit Problems}},
  booktitle =	{13th International Conference on Geographic Information Science (GIScience 2025)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-378-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{346},
  editor =	{Sila-Nowicka, Katarzyna and Moore, Antoni and O'Sullivan, David and Adams, Benjamin and Gahegan, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2025.14},
  URN =		{urn:nbn:de:0030-drops-238433},
  doi =		{10.4230/LIPIcs.GIScience.2025.14},
  annote =	{Keywords: Machine Guidance, Geo-Spatial Analysis, Modifiable Areal Unit Problem (MAUP)}
}
Document
DOI: 10.4230/DagRep.8.3.94
Automatic Quality Assurance and Release (Dagstuhl Seminar 18122)

Authors: Bram Adams, Benoit Baudry, Sigrid Eldh, and Andy Zaidman

Published in: Dagstuhl Reports, Volume 8, Issue 3 (2018)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 18122 "Automatic Quality Assurance and Release". The main goal of this seminar was to bridge the knowledge divide on how researchers and industry professionals reason about and implement DevOps for automatic quality assurance. Through the seminar, we have built up a common understanding of DevOps tools and practices, but we have also identified major academic and educational challenges for this field of research.
Cite as

Bram Adams, Benoit Baudry, Sigrid Eldh, and Andy Zaidman. Automatic Quality Assurance and Release (Dagstuhl Seminar 18122). In Dagstuhl Reports, Volume 8, Issue 3, pp. 94-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{adams_et_al:DagRep.8.3.94,
  author =	{Adams, Bram and Baudry, Benoit and Eldh, Sigrid and Zaidman, Andy},
  title =	{{Automatic Quality Assurance and Release (Dagstuhl Seminar 18122)}},
  pages =	{94--127},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{3},
  editor =	{Adams, Bram and Baudry, Benoit and Eldh, Sigrid and Zaidman, Andy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.3.94},
  URN =		{urn:nbn:de:0030-drops-92994},
  doi =		{10.4230/DagRep.8.3.94},
  annote =	{Keywords: DevOps, automated quality assurance, Continuous Integration, Continuous Deployment, software testing}
}
Document
DOI: 10.4230/DagSemProc.06302.4
Face-off: AOP+LMP vs. legacy software

Authors: Kris De Schutter and Bram Adams

Published in: Dagstuhl Seminar Proceedings, Volume 6302, Aspects For Legacy Applications (2007)

Abstract
Our presentation relates on a first attempt to see if aspect-oriented programming (AOP) can really help with the revitalisation of legacy business software. By means of four realistic case studies covering reverse engineering, restructuring and integration, we discuss the applicability of the aspect-oriented paradigm in the context of two major programming languages for such environments: Cobol and C. For each case, we consider both advantages and disadvantages.
Cite as

Kris De Schutter and Bram Adams. Face-off: AOP+LMP vs. legacy software. In Aspects For Legacy Applications. Dagstuhl Seminar Proceedings, Volume 6302, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{deschutter_et_al:DagSemProc.06302.4,
  author =	{De Schutter, Kris and Adams, Bram},
  title =	{{Face-off: AOP+LMP vs. legacy software}},
  booktitle =	{Aspects For Legacy Applications},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6302},
  editor =	{Siobh\'{a}n Clarke and Leon Moonen and Ganesan Ramalingam},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06302.4},
  URN =		{urn:nbn:de:0030-drops-8886},
  doi =		{10.4230/DagSemProc.06302.4},
  annote =	{Keywords: AOP, legacy software, reverse-engineering, re-engineering, Cobol, C}
}
  • Refine by Type
  • 4 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 1 2018
  • 1 2007

  • Refine by Author
  • 2 Adams, Bram
  • 1 Baudry, Benoit
  • 1 Cai, Guoray
  • 1 De Schutter, Kris
  • 1 Eberl, Manuel
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 DagRep
  • 1 DagSemProc

  • Refine by Classification
  • 1 Computing methodologies → Artificial intelligence
  • 1 Information systems → Geographic information systems
  • 1 Information systems → Spatial-temporal systems
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 AOP
  • 1 Bernoulli numbers
  • 1 C
  • 1 Chinese remainder theorem
  • 1 Cobol
  • 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