@techreport(abbasi_10_pair_rv_verification_tr, author = "N{.} Abbasi and O{.} Hasan and S{.} Tahar", year = "2011", title = "{F}ormal {A}nalysis of {S}oft {E}rrors using {T}heorem {P}roving", type = "Technical {R}eport", institution = "Department of Electrical \& Computer Engineering, Concordia University, Canada.", url = "http://hvg.ece.concordia.ca/Publications/TECH_REP/SERTP_TR11", ) @article(Ref7:Masudaet.al., author = "H.~Masuda et. al.", year = "1980", title = "A 5 V-only 64K dynamic RAM based on high S/N design.", journal = "IEEE Journal of Solid-State Circuits", volume = "SC-15", number = "5", pages = "846 -- 853", doi = "10.1109/JSSC.1980.1051481", ) @article(pauline09, author = "P{.} Audebaud and C{.} Paulin-Mohring", year = "2009", title = "Proofs of {R}andomized {A}lgorithms in {C}oq", journal = "Science of Computer Programming", volume = "74", number = "8", pages = "568--589", doi = "10.1016/j.scico.2007.09.002", ) @article(BoxMuller, author = "G.~E.~P. Box and Mervin~E. Muller", year = "1958", title = "A Note on the Generation of Random Normal Deviates", journal = "Annals of Mathematical Statistics", volume = "29", number = "2", pages = "610--611", doi = "10.1214/aoms/1177706645", url = "http://projecteuclid.org/euclid.aoms/1177706645", ) @inproceedings(gordon_89, author = "M{.}J{.}C{.} Gordon", year = "1989", title = "Mechanizing {P}rogramming {L}ogics in {H}igher-{0}rder {L}ogic", booktitle = "Current {T}rends in {H}ardware {V}erification and {A}utomated {T}heorem {P}roving", publisher = "Springer", pages = "387--439", doi = "10.1007/978-1-4612-3658-0_10", ) @inproceedings(HarrisonJ_1_2005, author = "J.~Harrison", year = "2005", title = "A {HOL} {T}heory of {E}uclidean {S}pace", booktitle = "Proceedings of the 18th international conference on Theorem Proving in Higher Order Logics", series = "LNCS", volume = "3603", publisher = "Springer", pages = "114--129", doi = "10.1007/11541868_8", ) @phdthesis(hasan_phd_08, author = "O{.} Hasan", year = "2008", title = "Formal {P}robabilistic {A}nalysis using {T}heorem {P}roving", type = "Ph{D} {T}hesis", school = "Concordia {U}niversity", address = "Montreal, QC, Canada", url = "http://spectrum.library.concordia.ca/975852/", ) @inproceedings(FM_PAPER_09, author = "O{.} {H}asan and N{.} Abbasi and B{.} {A}kbarpour and S{.} {T}ahar and R{.} {A}kbarpour", year = "2009", title = "Formal {R}easoning about {E}xpectation {P}roperties for {C}ontinuous {R}andom {V}ariables", booktitle = "Formal {M}ethods", series = "LNCS", volume = "5850", publisher = "Springer", pages = "435--450", doi = "10.1007/978-3-642-05089-3_28", ) @inproceedings(johannes_tphol_11, author = "J{.} H{\"o}lzl and A{.} Heller", year = "2011", title = "Three Chapters of Measure Theory in {Isabelle/HOL}", booktitle = "Interactive Theorem Proving", series = "LNCS", volume = "6898", publisher = "Springer", pages = "135--151", doi = "10.1007/978-3-642-22863-6", ) @phdthesis(hurd_02, author = "J{.} Hurd", year = "2002", title = "Formal {V}erification of {P}robabilistic {A}lgorithms", type = "Ph{D} {T}hesis", school = "University of Cambridge", address = "Cambridge, UK", url = "http://www.gilith.com/research/papers/thesis.pdf", ) @book(DRAMBook, author = "B.~Keeth", year = "2008", title = "DRAM Circuit Design: Fundamentals and High-Speed Topics", publisher = "IEEE", ) @article(Ref4:RWKeyes, author = "R.~W. Keyes", year = "1975", title = "Effect of {R}andomness in the {D}istribution of {I}mpurity {I}ons on FET {T}hresholds in {I}ntegrated {E}lectronics.", journal = "IEEE Journal of Solid-State Circuits", volume = "SC-10", number = "5", pages = "245 -- 247", doi = "10.1109/JSSC.1975.1050600", ) @book(khazanie_76, author = "R{.} Khazanie", year = "1976", title = "Basic {P}robability {T}heory and {A}pplications", publisher = "Goodyear", ) @article(MainSoftErrorModelLaymanChamberlain, author = "P.~A. Layman and S.~G. Chamberlain", year = "1989", title = "A {C}ompact {T}hermal {M}odel for {I}nvestigation of {S}oft {E}rror {R}ates in {MOS} {VLSI} {D}igital {C}ircutis", journal = "IEEE Journal of Solid-State Circuits", volume = "24", number = "1", pages = "79 -- 89", doi = "10.1109/4.16305", ) @article(Ref8:MayWoods, author = "T.~C. May and M.~H. Woods", year = "1979", title = "Alpha-particle-induced {S}oft {E}rrors in {D}ynamic {M}emories", journal = "IEEE Transactions on Electron Devices", volume = "ED-26", number = "1", pages = "2 -- 9", doi = "10.1109/T-ED.1979.19370", ) @article(MONTE_CARLO_SER_TOOLS_5_1949, author = "N.~Metropolis and S.~Ulam", year = "1949", title = "The Monte Carlo Method", journal = "Journal of the American Statistical Association", volume = "44", number = "247", pages = "335--341", doi = "10.1080/01621459.1949.10483310", url = "http://www.jstor.org/stable/2280232", ) @inproceedings(mhamdi_tphol_2010, author = "T{.} Mhamdi and O{.} Hasan and S{.} Tahar", year = "2010", title = "On the {F}ormalization of the {L}ebesgue {I}ntegration {T}heory in {HOL}", booktitle = "{I}nteractive {T}heorem {P}roving", series = "LNCS", volume = "6172", publisher = "Springer", pages = "387--402", doi = "10.1007/978-3-642-14052-5_27", ) @inproceedings(mhamdi_tphol_11, author = "T{.} Mhamdi and O{.} Hasan and S{.} Tahar", year = "2011", title = "{F}ormalization of {E}ntropy {M}easures in {HOL}", booktitle = "{I}nteractive {T}heorem {P}roving", series = "LNCS", volume = "6898", publisher = "Springer", pages = "233--248", doi = "10.1007/978-3-642-22863-6_18", ) @article(OkazakiS_ShidamaY_2009, author = "H.~Okazaki and Y.~Shidama", year = "2009", title = "Probability on Finite Set and Real-Valued Random Variables", journal = "Formalized Mathematics", volume = "17", number = "1-4", pages = "129--136", doi = "10.2478/v10037-009-0014-x", url = "http://versita.metapress.com/content/D3073K63W370G262", )