Title :
Formal verification of the heavy hitter problem
Author :
Helali, G. ; Tahar, Sofiene ; Hasan, Osman
Author_Institution :
Dept. of Electr. & Comput. Eng., Concordia Univ., Montreal, QC, Canada
fDate :
April 29 2012-May 2 2012
Abstract :
The heavy hitter problem is used to assess the frequency of occurrence of an element in a given data stream. It is one of the most widely used combinatorial tools in many safety-critical domains including medicine, telecommunications and stock exchange markets. Traditionally, the heavy hitter problem is analyzed using paper-and-pencil proofs, simulation or computer algebra systems. These techniques are informal and thus may result in an inaccurate analysis, which poses a serious threat to the reliability of the underlying applications of the problem. To overcome this limitation, we present a formal probabilistic analysis approach for the heavy hitter problem using a higher-order-logic theorem prover (HOL). The paper presents the higher-order-logic model of an algorithm for the heavy hitter problem. This model is then utilized to formally verify some interesting probabilistic and statistical properties associated with the heavy hitter problem in HOL.
Keywords :
combinatorial mathematics; data analysis; formal logic; formal verification; pattern recognition; probability; statistical analysis; theorem proving; HOL; combinatorial tool; computer algebra system; data stream; formal probabilistic analysis approach; formal verification; heavy hitter problem; higher-order-logic model; higher-order-logic theorem prover; medicine; occurrence frequency assessment; paper-and-pencil proof; probabilistic property; safety-critical domain; simulation system; statistical property; stock exchange market; telecommunications; Algorithm design and analysis; Computational modeling; Computers; Educational institutions; Extraterrestrial measurements; Probabilistic logic; Random variables; Formal Verification; Heavy Hitter Problem; Higher-order Logic; Probability Theory; Theorem Proving;
Conference_Titel :
Electrical & Computer Engineering (CCECE), 2012 25th IEEE Canadian Conference on
Conference_Location :
Montreal, QC
Print_ISBN :
978-1-4673-1431-2
Electronic_ISBN :
0840-7789
DOI :
10.1109/CCECE.2012.6335035