Formalization of Cadence SPW Fixed-Point Arithmetic in HOL. - Behzad Akbarpour; Abdelkader Dekdouk; Sofiène Tahar (IFM, 2002)

The Application of Formal Verification to SPW Designs. - Behzad Akbarpour; Sofiène Tahar (DSD, 2003)

Modeling System C Fixed-Point Arithmetic in HOL. - Behzad Akbarpour; Sofiène Tahar (ICFEM, 2003)

A Methodology for the Formal Verification of FFT Algorithms in HOL. - Behzad Akbarpour; Sofiène Tahar (FMCAD, 2004)

Error Analysis of Digital Filters Using Theorem Proving. - Behzad Akbarpour; Sofiène Tahar (TPHOLs, 2004)

Formalization of Fixed-Point Arithmetic in HOL. - Behzad Akbarpour; Sofiène Tahar; Abdelkader Dekdouk (Formal Methods Syst. Des., 2005)

Formal Analysis and Verification of an OFDM Modem Design using HOL. - Abu Nasser Mohammed Abdullah; Behzad Akbarpour; Sofiène Tahar (FMCAD, 2006)

An approach for the formal verification of DSP designs using Theorem proving. - Behzad Akbarpour; Sofiène Tahar (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2006)

Extending a Resolution Prover for Inequalities on Elementary Functions. - Behzad Akbarpour; Lawrence C. Paulson (LPAR, 2007)

Error analysis of digital filters using HOL theorem proving. - Behzad Akbarpour; Sofiène Tahar (J. Appl. Log., 2007)

MetiTarski: An Automatic Prover for the Elementary Functions. - Behzad Akbarpour; Lawrence C. Paulson (AISC/MKM/Calculemus, 2008)

Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving. - Abu Nasser Mohammed Abdullah; Behzad Akbarpour; Sofiène Tahar (FMWS@CONCUR, 2008)

Formal Reasoning about Expectation Properties for Continuous Random Variables. - Osman Hasan; Naeem Abbasi; Behzad Akbarpour; Sofiène Tahar; Reza Akbarpour (FM, 2009)

Formal verification of analog designs using MetiTarski. - William Denman; Behzad Akbarpour; Sofiène Tahar; Mohamed H. Zaki; Lawrence C. Paulson (FMCAD, 2009)

Applications of MetiTarski in the Verification of Control and Hybrid Systems. - Behzad Akbarpour; Lawrence C. Paulson (HSCC, 2009)

Formal verification of analog circuits in the presence of noise and process variation. - Rajeev Narayanan; Behzad Akbarpour; Mohamed H. Zaki; Sofiène Tahar; Lawrence C. Paulson (DATE, 2010)

Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. - Behzad Akbarpour; Amr Talaat Abdel-Hamid; Sofiène Tahar; John Harrison 001 (Comput. J., 2010)

MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. - Behzad Akbarpour; Lawrence C. Paulson (J. Autom. Reason., 2010)