Methodology for Formal Verification of Hardware Safety Strategies Using SMT
The work
| Authors | Faure-Gignoux, Anthony; Delmas, Kevin; Gauffriau, Adrien; Pagetti, Claire |
|---|---|
| Editors | |
| Type | misc |
| Year | 2024 |
| Also known as | anon2024methodology |
| Citekey | fauregignoux2024methodology |
Where it appeared
| Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
|---|
Identifiers
| DOI | 10.1109/les.2024.3439859 |
|---|
Access
From unpaywall.
Abstract
Safety-critical embedded systems must maintain their functionality even in the presence of single permanent hardware failure. Naive redundancy of hardware is often unaffordable and impractical, therefore alternative strategies must be explored for minimal cost fault-tolerance. The objective of this paper is to propose a methodology to evaluate formally safety strategies using Satisfiability Modulo Theory solvers. Practically, the approach consists in providing a bounded model checking demonstration applied to the formal model of hardware. We show the capabilities of the approach on an efficient hardware accelerator designed to perform parallel computations of matrix multiplications and convolutions.
A copy is held
pdf, 374.2 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via unpaywall |
|---|---|
| Added | 2026-10-22 21:15 UTC |
| Approved by | a person 2026-10-22 22:41 UTC |
Cite it as
@misc{fauregignoux2024methodology,
title = {Methodology for Formal Verification of Hardware Safety Strategies Using SMT},
author = {Faure-Gignoux, Anthony and Delmas, Kevin and Gauffriau, Adrien and Pagetti, Claire},
year = {2024},
publisher = {Institute of Electrical and Electronics Engineers (IEEE)},
doi = {10.1109/les.2024.3439859},
}
This record lives at https://refs.drheap.org/fauregignoux2024methodology/ and will keep
doing so. It used to be called anon2024methodology, and those addresses still resolve to this one.