Publications
[1] O.Hasan and S. Tahar. Probabilistic Analysis using Theorem Proving - A Higher-Order-Logic Based Approach. VDM Verlag Dr. Mueller e.K., November, 2008. ISBN: 978-3639094725 [164 pages]
|
|
|
Journals
[1] O. Hasan and S. Tahar, Reasoning about Conditional
Probabilities in a Higher-order-Logic Theorem Prover,
Journal
of Applied Logic, Elsevier, Vol 9, No. 1, 2011, January 2011, pp.23 - 40.
[2] O. Hasan and S. Tahar," Formally Analyzing Expected Time Complexity of
Algorithms using Theorem Proving", Journal of Computer Science
and Technology, Springer, Vol 25, No. 6, September 2010, pp.1305-1320.
[3] O. Hasan, S. Tahar, N. Abassi: "Formal
Reliability Analysis using Theorem Proving", IEEE Transactions on
Computers, Vol. 59, No. 5, IEEE, May 2010, pp. 579-592.
[4] O.Hasan and S. Tahar. Probabilistic Analysis of Wireless Systems using Theorem Proving. Electronic Notes in Theoretical Computer Science , Vol. 242, No. 2, Elsevier, July 2009, pp. 43-58.
[5] O.Hasan and S. Tahar.
Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover. Mathematical
Methods in The Applied Sciences, Vol. 32, no. 4, Wiley Interscience,
March 2009, pp. 480-504.
[6] O.Hasan and S. Tahar. Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL. Journal of Automated Reasoning, Vol. 42, No. 1, Springer Verlag, January 2009, pp. 1-33.
[7] O.Hasan and S. Tahar. Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning, Vol. 41, No. 3-4, Springer Verlag, November 2008, pp. 295-323.
[8] O.Hasan and S. Tahar. Formalization of the Standard Uniform Random Variable. Theoretical Computer Science, Vol.
382, No. 1, Elsevier, 2007, pp. 71-83.
Conferences
[1] T. Mhamdi,O. Hasan and S. Tahar, On the
Formalization of the Lebesgue Integration Theory in
HOL, In: M.. Kauffman and L. Paulson (Eds.) Interactive Theorem Proving,
Lecture Notes in Computer Science 6172 , Springer Verlag,
2010, pp. 387-402. [Proc. International Conference on Interactive Theorem Proving(ITP-10),
[2] N. Abbasi,O. Hasan, and S. Tahar, Formal
Lifetime Reliability Analysis Using Continuous Random Variables; In: A. Dawar and R. de Queiroz (Eds.),
Logic, Language, Information and Computation, Lecture Notes in Computer Science
6188 , Springer Verlag, 2010, pp. 84-97. [Proc.
International Workshop on Logic, Language,
Information and Computation (WOLLIC-2010),
[3] O. Hasan,J. Patel, and S. Tahar, On the Accurate Reliability Analysis of Combinational Circuits Using Theorem Proving, IEEE International Northeastern Workshop on Circuits and Systems (NEWCAS-10), pp. 273-276, Montreal, Canada, June 2010.
[4] J.B. Hassan, O. Hasan, T. Sadani
and S. Tahar: Performance
Analysis of Real-Time Rewriting Models, ACS/IEEE International Conference
on Computer Systems and Applications (AICCSA-10), Hammamet,
Tunisia, May 2010.
[5] O. Hasan and S. Tahar: Formal
Probabilistic Analysis: A Higher-OrderLogic Based Approach; In: M. Frappier
et al. (Ed.), ASM, Alloy, B and Z, Lecture Notes in Computer Science 5977 ,
Springer Verlag, 2010, pp. 2-19. [Proc.
International Conference on ASM, Alloy, B and Z (ABZ-2010), Orford,
[6] O. Hasan, N. Abbasi,
B. Akbarpour, S. Tahar, and
R. Akbarpour: Formal Reasoning
about Expectation Properties for Continuous Random Variables; In: A. Cavalcanti and D. Dams (Eds.), Formal Methods, Lecture
Notes in Computer Science 5850, Springer Verlag,
2009, pp. 435-450. [Proc. International Symposium on Formal Methods (FM'09),
[7] O. Hasan, S.K. Afshar
and S. Tahar: Formal
Analysis of Optical Waveguides in HOL ; In: S. Berghofer
et al. (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in
Computer Science 5674, Springer Verlag, 2009, pp.
228-243. [Proc. International Conference on Theorem Proving
in Higher-Order Logics (TPHOLs'09),
[8] O. Hasan, N. Abbasi, B. Akbarpour, and S. Tahar: Formal Probabilistic Analysis using Theorem Proving;
Proc. 77th ACFAS Symposium (ACFAS'09),
[9] O. Hasan, N. Abbasi and S. Tahar: Formal
Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays;
In: M. Leuschel and H. Wehrheim
(Eds.), Integrated Formal Methods, Lecture Notes in Computer
Science 5423, Springer Verlag,
2009, pp. 277-291. [Proc. International Conference on Integrated
Formal Methods (IFM'09),
[10] O. Hasan and S. Tahar: Performance Analysis of Wireless Systems using Theorem Proving; In: Jens Chr. Godskesen and Massimo Merro (Eds.), First International Workshop on Formal Methods for Wireless Systems (FMWS'2008), Toronto, ON, Canada, August 2008, pp. 3-18, ISSN 1600-6100, ISBN 978-87-7949-183-0.
[11] O. Hasan. Probabilistic
Analysis using Theorem Proving; In: O. Ait
Mohammed, C. Munoz and S. Tahar (Eds.)
International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'08),
Emerging Trend Proceedings, Montreal
[12] O. Hasan and S. Tahar: Performance Analysis of ARQ Protocols using a Theorem Prover; In IEEE International Symposium on Performance Analysis of Systems and Software (ISPASS'08), IEEE Computer Society, Austin, Texas, USA, April 2008, pp. 85-94.
[13] O. Hasan and S. Tahar:
Verification
of Tail Distribution Bounds in a Theorem Prover;
In: T.E.Simos, G. Psihoyios and Ch. Tsitouras (Eds.), Numerical
Analysis and Applied Mathematics, AIP Conference Proceedings Volume 936,
2007, pp. 259-262. [Proc. International Conference of Numerical Analysis and
Applied Mathematics (ICNAAM`07),
[14] O. Hasan and S. Tahar:
Verification
of Expectation Properties for Discrete Random Variables in HOL; In: K.Schneider and J.Brandt (Eds.), Theorem
Proving in Higher-Order Logics, Lecture Notes in Computer Science 4732,
Springer Verlag, 2007, pp.
119-134. [Proc. International Conference on Theorem
Proving in Higher-Order Logics (TPHOLs'07),
[15] O.Hasan
and S. Kort. Automated Formal Synthesis of Wallace Tree Multipliers. In 50th IEEE Int'l Midwest Symposium
on Circuits & Systems, pp. 293 - 296.
[16] O. Hasan and S. Tahar:
Formalization
of Continuous Probability Distributions; In: F. Pfenning (Ed.),
Automated Deduction, Lecture Notes in Computer Science 4603, Springer Verlag, 2007, pp. 2-18. [Proc.
21st Conference on Automated Deduction (CADE-21),
[17] O. Hasan and S. Tahar:
Verification
of Probabilistic Properties in the HOL Theorem Prover; In: J. Davies and J. Gibbons (Eds.), Integrated
Formal Methods, Lecture Notes in Computer Science 4591, Springer Verlag, 2007, pp. 333-352. [Proc.
International Conference on Integrated Formal Methods (IFM'07),
Technical Reports
[1 O. Hasan, J.
Patel and S. Tahar, Accurate
Reliability Analysis of Combinational Circuits using Theorem Proving.Technical Report,
Department of Electrical and Computer Engineering, Concordia University,
January 2010. [13 Pages]
[2] O. Hasan
and S. Tahar. Formal
Verification of Expectation and Variance for Discrete Random Variables; Technical
Report,
[3] O.Hasan
and S. Tahar. Formalization
of Continuous Probability Distributions; Technical Report,
[4] O.Hasan and S. Tahar. Standard
Uniform Distribution Theory in HOL-4; Technical Report,
[5] O.Hasan and S. Tahar. Formalization of the Standard Uniform Random Variable in HOL; Technical Report,
PhD Thesis
O. Hasan. Formal
Probabilistic Analysis using Theorem Proving