3 Search Results for "Cabodi, Gianpiero"

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/LITES-v005-i001-a004
A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits

Authors: Dmitry Burlyaev, Pascal Fradet, and Alain Girault

Published in: LITES, Volume 5, Issue 1 (2018). Leibniz Transactions on Embedded Systems, Volume 5, Issue 1

Abstract
We present a formal approach to minimize the number of voters in triple-modular redundant (TMR) sequential circuits. Our technique actually works on a single copy of the TMR circuit and considers a large class of fault mo dels of the form “at most 1 Single-Event Upset (SEU) or Single-Event Transient (SET) every k clock cycles”. Verification-based voter minimization guarantees that the resulting TMR circuit (i) is fault tolerant to the soft-errors defined by the fault model and (ii) is functionally equivalent to the initial TMR circuit. Our approach operates at the logic level and takes into account the input and output interface specifications of the circuit. Its implementation makes use of graph traversal algorithms, fixed-point iterations, and binary decision diagrams (BDD). Experimental results on the ITC’99 benchmark suite indicate that our method significantly decreases the number of inserted voters, yielding a hardware reduction of up to 55% and a clock frequency increase of up to 35% compared to full TMR. As our experiments show, if the SEU fault-model is replaced with the stricter fault-model of SET, it has a minor impact on the number of removed voters. On the other hand, BDD-based modelling of SET effects represents a more complex task than the modelling of an SEU as a bit-flip. We propose solutions for this task and explain the nature of encountered problems. We address scalability issues arising from formal verification with approximations and assess their efficiency and precision.
Cite as

Dmitry Burlyaev, Pascal Fradet, and Alain Girault. A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits. In LITES, Volume 5, Issue 1 (2018). Leibniz Transactions on Embedded Systems, Volume 5, Issue 1, pp. 04:1-04:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{burlyaev_et_al:LITES-v005-i001-a004,
  author =	{Burlyaev, Dmitry and Fradet, Pascal and Girault, Alain},
  title =	{{A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:26},
  ISSN =	{2199-2002},
  year =	{2018},
  volume =	{5},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v005-i001-a004},
  URN =		{urn:nbn:de:0030-drops-192753},
  doi =		{10.4230/LITES-v005-i001-a004},
  annote =	{Keywords: Digital Circuits, Fault-tolerance, Optimization, Static Analysis, Triple Modular Redundancy}
}
Document
DOI: 10.4230/LIPIcs.CPM.2016.11
A 7/2-Approximation Algorithm for the Maximum Duo-Preservation String Mapping Problem

Authors: Nicolas Boria, Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, and Stefano Quer

Published in: LIPIcs, Volume 54, 27th Annual Symposium on Combinatorial Pattern Matching (CPM 2016)

Abstract
This paper presents a simple 7/2-approximation algorithm for the Maximum Duo-Preservation String Mapping (MPSM) problem. This problem is complementary to the classical and well studied min common string partition problem (MCSP), that computes the minimal edit distance between two strings when the only operation allowed is to shift blocks of characters. The algorithm improves on the previously best-known 4-approximation algorithm by computing a simple local optimum.
Cite as

Nicolas Boria, Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, and Stefano Quer. A 7/2-Approximation Algorithm for the Maximum Duo-Preservation String Mapping Problem. In 27th Annual Symposium on Combinatorial Pattern Matching (CPM 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 54, pp. 11:1-11:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{boria_et_al:LIPIcs.CPM.2016.11,
  author =	{Boria, Nicolas and Cabodi, Gianpiero and Camurati, Paolo and Palena, Marco and Pasini, Paolo and Quer, Stefano},
  title =	{{A 7/2-Approximation Algorithm for the Maximum Duo-Preservation String Mapping Problem}},
  booktitle =	{27th Annual Symposium on Combinatorial Pattern Matching (CPM 2016)},
  pages =	{11:1--11:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-012-5},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{54},
  editor =	{Grossi, Roberto and Lewenstein, Moshe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2016.11},
  URN =		{urn:nbn:de:0030-drops-60875},
  doi =		{10.4230/LIPIcs.CPM.2016.11},
  annote =	{Keywords: Polynomial approximation, Max Duo-Preservation String Mapping Problem, Min Common String Partition Problem, Local Search}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2018
  • 1 2016

  • Refine by Author
  • 1 Boria, Nicolas
  • 1 Burlyaev, Dmitry
  • 1 Cabodi, Gianpiero
  • 1 Camurati, Paolo
  • 1 Dongol, Brijesh
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 1 Hardware → Model checking
  • 1 Hardware → Redundancy
  • 1 Theory of computation → Program reasoning

  • Refine by Keyword
  • 1 Binary Analysis Platform
  • 1 Digital Circuits
  • 1 Fault-tolerance
  • 1 Hoare Logic
  • 1 Incorrectness Logic
  • 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