Search

Your search keyword '"Akbarpour, Behzad"' showing total 27 results
Start Over Author "Akbarpour, Behzad"
27 results on '"Akbarpour, Behzad"'

1. Formal Reasoning about Expectation Properties for Continuous Random Variables

Author

Hasan, Osman, Abbasi, Naeem, Akbarpour, Behzad, Tahar, Sofiène, Akbarpour, Reza, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Cavalcanti, Ana, editor, and Dams, Dennis R., editor

Published
2009
Full Text
View/download PDF

2. Applications of MetiTarski in the Verification of Control and Hybrid Systems

Author

Akbarpour, Behzad, Paulson, Lawrence C., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Majumdar, Rupak, editor, and Tabuada, Paulo, editor

Published
2009
Full Text
View/download PDF

5. A Methodology for the Formal Verification of FFT Algorithms in HOL

Author

Akbarpour, Behzad, Tahar, Sofiène, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Hu, Alan J., editor, and Martin, Andrew K., editor

Published
2004
Full Text
View/download PDF

6. Error Analysis of Digital Filters Using Theorem Proving

Author

Akbarpour, Behzad, Tahar, Sofiène, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Slind, Konrad, editor, Bunker, Annette, editor, and Gopalakrishnan, Ganesh, editor

Published
2004
Full Text
View/download PDF

25. Extending a Resolution Prover for Inequalities on Elementary Functions.

Author

Carbonell, Jaime G., Siekmann, Jörg, Dershowitz, Nachum, Voronkov, Andrei, Akbarpour, Behzad, and Paulson, Lawrence C.

Abstract

Experiments show that many inequalities involving exponentials and logarithms can be proved automatically by combining a resolution theorem prover with a decision procedure for the theory of real closed fields (RCF). The method should be applicable to any functions for which polynomial upper and lower bounds are known. Most bounds only hold for specific argument ranges, but resolution can automatically perform the necessary case analyses. The system consists of a superposition prover (Metis) combined with John Harrison's RCF solver and a small amount of code to simplify literals with respect to the RCF theory. [ABSTRACT FROM AUTHOR]

Published
2007
Full Text
View/download PDF

26. A Methodology for the Formal Verification of FFT Algorithms in HOL.

Author

Hu, Alan J., Martin, Andrew K., Akbarpour, Behzad, and Tahar, Sofiène

Abstract

This paper addresses the formal specification and verification of fast Fourier transform (FFT) algorithms at different abstraction levels based on the HOL theorem prover. We make use of existing theories in HOL on real and complex numbers, IEEE standard floating-point, and fixed-point arithmetics to model the FFT algorithms. Then, we derive, by proving theorems in HOL, expressions for the accumulation of roundoff error in floating- and fixed-point FFT designs with respect to the corresponding ideal real and complex numbers specification. The HOL formalization and proofs are found to be in good agreement with the theoretical paper-and-pencil counterparts. Finally, we use a classical hierarchical proof approach in HOL to prove that the FFT implementations at the register transfer level (RTL) implies the corresponding high level fixed-point algorithmic specification. [ABSTRACT FROM AUTHOR]

Published
2004

27. Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL.

Author

AKBARPOUR, BEHZAD, ABDEL-HAMID, AMR T., TAHAR, SOFIÈNE, and HARRISON, JOHN

Subjects
*FLOATING-point arithmetic, *ARITHMETIC, *ALGORITHMS, *EXPONENTIAL functions, *MATHEMATICS
Abstract

Deep datapath and algorithm complexity have made the verification of floating-point units a very hard task. Most simulation and reachability analysis verification tools fail to verify a circuit with a deep datapath like most industrial floating-point units. Theorem proving, however, offers a better solution to handle such verification. In this paper, we have hierarchically formalized and verified a hardware implementation of the IEEE-754 table-driven floating-point exponential function algorithm using the higher-order logic (HOL) theorem prover. The high ability of abstraction in the HOL verification system allows its use for the verification task over the whole design path of the circuit, starting from gate-level implementation of the circuit up to a high-level mathematical specification. [ABSTRACT FROM PUBLISHER]

Published
2010
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results