2 Search Results for "Burkhart, Daniel"

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.14
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL

Authors: Matt Griffin, Brijesh Dongol, and Azalea Raad

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

Abstract
This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP’s intermediate language, called BIL and integrate it with Hoare logic (to enable proofs of correctness) as well as incorrectness logic (to enable proofs of incorrectness). IsaBIL inherits the full flexibility of BAP, allowing us to verify binaries for a wide range of languages (C, C++, Rust), toolchains (LLVM, Ghidra) and target architectures (x86, RISC-V), and can also be used when the source code for a binary is unavailable. To make verification tractable, we develop a number of big-step rules that combine BIL’s existing small-step rules at different levels of abstraction to support reuse. We develop high-level reasoning rules for RISC-V instructions (our main target architecture) to further optimise verification. Additionally, we develop Isabelle proof tactics that exploit common patterns in C binaries for RISC-V to discharge large numbers of proof goals (often in the 100s) automatically. IsaBIL includes an Isabelle/ML based parser for BIL programs, allowing one to automatically generate the associated Isabelle/HOL program locale from a BAP output. Taken together, IsaBIL provides a highly flexible proof environment for program binaries. As examples, we prove correctness of key examples from the Joint Strike Fighter coding standards and the MITRE database.
Cite as

Matt Griffin, Brijesh Dongol, and Azalea Raad. IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 14:1-14:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{griffin_et_al:LIPIcs.ECOOP.2025.14,
  author =	{Griffin, Matt and Dongol, Brijesh and Raad, Azalea},
  title =	{{IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{14:1--14:30},
  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.14},
  URN =		{urn:nbn:de:0030-drops-233070},
  doi =		{10.4230/LIPIcs.ECOOP.2025.14},
  annote =	{Keywords: Binary Analysis Platform, Isabelle/HOL, Hoare Logic, Incorrectness Logic}
}
Document
DOI: 10.4230/OASIcs.VLUDS.2010.1
Finite Element Analysis for Linear Elastic Solids Based on Subdivision Schemes

Authors: Daniel Burkhart, Bernd Hamann, and Georg Umlauf

Published in: OASIcs, Volume 19, Visualization of Large and Unstructured Data Sets - Applications in Geospatial Planning, Modeling and Engineering (IRTG 1131 Workshop) (2011)

Abstract
Finite element methods are used in various areas ranging from mechanical engineering to computer graphics and bio-medical applications. In engineering, a critical point is the gap between CAD and CAE. This gap results from different representations used for geometric design and physical simulation. We present two different approaches for using subdivision solids as the only representation for modeling, simulation and visualization. This has the advantage that no data must be converted between the CAD and CAE phases. The first approach is based on an adaptive and feature-preserving tetrahedral subdivision scheme. The second approach is based on Catmull-Clark subdivision solids.
Cite as

Daniel Burkhart, Bernd Hamann, and Georg Umlauf. Finite Element Analysis for Linear Elastic Solids Based on Subdivision Schemes. In Visualization of Large and Unstructured Data Sets - Applications in Geospatial Planning, Modeling and Engineering (IRTG 1131 Workshop). Open Access Series in Informatics (OASIcs), Volume 19, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{burkhart_et_al:OASIcs.VLUDS.2010.1,
  author =	{Burkhart, Daniel and Hamann, Bernd and Umlauf, Georg},
  title =	{{Finite Element Analysis for Linear Elastic Solids Based on Subdivision Schemes}},
  booktitle =	{Visualization of Large and Unstructured Data Sets - Applications in Geospatial Planning, Modeling and Engineering (IRTG 1131 Workshop)},
  pages =	{1--10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-29-3},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{19},
  editor =	{Middel, Ariane and Scheler, Inga and Hagen, Hans},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.VLUDS.2010.1},
  URN =		{urn:nbn:de:0030-drops-30928},
  doi =		{10.4230/OASIcs.VLUDS.2010.1},
  annote =	{Keywords: Subdivision solids, Finite element method, Isogeometric analysis}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2011

  • Refine by Author
  • 1 Burkhart, Daniel
  • 1 Dongol, Brijesh
  • 1 Griffin, Matt
  • 1 Hamann, Bernd
  • 1 Raad, Azalea
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 1 Theory of computation → Program reasoning

  • Refine by Keyword
  • 1 Binary Analysis Platform
  • 1 Finite element method
  • 1 Hoare Logic
  • 1 Incorrectness Logic
  • 1 Isabelle/HOL
  • 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