Formal Analysis of Soft Errors using Theorem Proving

The work

AuthorsNaeem Abbasi; Osman Hasan; Sofiène Tahar
Editors
Typearticle
Year2013
Citekeyabbasi2013formal

Where it appeared

Published inElectronic Proceedings in Theoretical Computer Science
Volume122
Pages75--84

Identifiers

arXiv1307.8213 from its landing_page_url
DOI10.4204/eptcs.122.7

Related

Distinct fromkhalid2022forasec
Distinct frommishagli2024statistical
Distinct fromrashid2020fasim
Distinct fromwaddoups2025probabilistic

From bibtex.

Abstract

Modeling and analysis of soft errors in electronic circuits has traditionally been done using computer simulations. Computer simulations cannot guarantee correctness of analysis because they utilize approximate real number representations and pseudo random numbers in the analysis and thus are not well suited for analyzing safety-critical applications. In this paper, we present a higher-order logic theorem proving based method for modeling and analysis of soft errors in electronic circuits. Our developed infrastructure includes formalized continuous random variable pairs, their Cumulative Distribution Function (CDF) properties and independent standard uniform and Gaussian random variables. We illustrate the usefulness of our approach by modeling and analyzing soft errors in commonly used dynamic random access memory sense amplifier circuits.

A copy is held

pdf, 225.5 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-09-18 03:03 UTC
Approved bya person 2026-10-05 21:13 UTC

Filed under

eptcs hasan

Cite it as

@article{abbasi2013formal,
  title        = {Formal Analysis of Soft Errors using Theorem Proving},
  author       = {Naeem Abbasi and Osman Hasan and Sofiène Tahar},
  year         = {2013},
  journal      = {Electronic Proceedings in Theoretical Computer Science},
  volume       = {122},
  pages        = {75--84},
  doi          = {10.4204/eptcs.122.7},
}

This record lives at https://refs.drheap.org/abbasi2013formal/ and will keep doing so.