Formalized Probability Theory and Applications Using Theorem Proving

Formalized Probability Theory and Applications Using Theorem Proving

Osman Hasan (National University of Sciences and Technology, Pakistan) and Sofiène Tahar (Concordia University, Canada)
Indexed In: SCOPUS
Release Date: March, 2015|Copyright: © 2015 |Pages: 298
ISBN13: 9781466683150|ISBN10: 1466683155|EISBN13: 9781466683167|DOI: 10.4018/978-1-4666-8315-0


Scientists and engineers often have to deal with systems that exhibit random or unpredictable elements and must effectively evaluate probabilities in each situation. Computer simulations, while the traditional tool used to solve such problems, are limited in the scale and complexity of the problems they can solve.

Formalized Probability Theory and Applications Using Theorem Proving discusses some of the limitations inherent in computer systems when applied to problems of probabilistic analysis, and presents a novel solution to these limitations, combining higher-order logic with computer-based theorem proving. Combining practical application with theoretical discussion, this book is an important reference tool for mathematicians, scientists, engineers, and researchers in all STEM fields.

Topics Covered

The many academic areas covered in this publication include, but are not limited to:

  • Formal Probabilistic Analysis
  • Higher-Order Logic
  • Information Theory
  • Lebesgue Integration
  • Markov chains
  • Measure Theory
  • Probability theory
  • Theorem Proving

Reviews and Testimonials

Hasan and Tahar present students, academics, and professionals working in a variety of contexts with an examination of the limitations of computer systems in probabilistic analysis, putting forth a combination of higher-order logic and computer-based theorem proving as a possible solution to these limitations. The authors have organized the main body of their text in fourteen chapters devoted to probabilistic analysis, formal verification methods, probabilistic analysis using theorem proving, and a wide variety of other related subjects. Osman Hasan is a faculty member of the National University of Sciences and Technology, Pakistan.

– ProtoView Book Abstracts (formerly Book News, Inc.)

Table of Contents and List of Contributors

Search this Book:

Author(s)/Editor(s) Biography

Osman Hasan received the BEng (Hons) degree from the N-W.F.P University of Engineering and Technology, Pakistan in 1997, and the MEng and PhD degrees from Concordia University, Montreal, Quebec, Canada, in 2001 and 2008 respectively. He worked as a postdoctoral fellow at the Hardware Verification Group (HVG) of Concordia University for one year until August 2009. Currently, he is an Assistant Professor in the School of Electrical Engineering and Computer Science, National University of Science and Technology (NUST), Islamabad, Pakistan. He is the founder and director of System Analysis and Verification (SAVe) Lab at NUST, which main focuses on the design and formal verification of embedded systems. Dr. Hasan is a Senior member of IEEE, member of Association for Automated Reasoning (AAR) and member of the Pakistan Engineering Council.
Sofiène Tahar received the Diploma degree in computer engineering from the University of Darmstadt, Germany in 1990, and the Ph.D. degree with "Distinction" in computer science from the University of Karlsruhe, Germany in 1994. Currently he is Professor in the Department of Electrical and Computer Engineering at Concordia University, Montreal, Quebec, Canada, where he is holding a Senior Research Chair in Formal Verification of System-on-Chip. Prof. Tahar is founder and director of the Hardware Verification Group at Concordia University, which focuses on developing verification technologies in the fields of microelectronics, telecommunications, security, aviation, etc. He has received several awards and distinctions, including a National Discovery Award in 2010, given to Canada's top 100 researchers in engineering and natural sciences. Prof. Tahar is Senior member of IEEE, Senior member of ACM and member of the Order of Engineers of Quebec, IEEE Computer and IEEE Communications Societies.