{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,15]],"date-time":"2025-07-15T03:32:20Z","timestamp":1752550340474,"version":"3.37.3"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T00:00:00Z","timestamp":1717200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T00:00:00Z","timestamp":1717200000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1007\/s10836-024-06123-9","type":"journal-article","created":{"date-parts":[[2024,6,28]],"date-time":"2024-06-28T04:03:28Z","timestamp":1719547408000},"page":"329-345","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of Universal Numbers using Theorem Proving"],"prefix":"10.1007","volume":"40","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9729-584X","authenticated-orcid":false,"given":"Adnan","family":"Rashid","sequence":"first","affiliation":[]},{"given":"Ayesha","family":"Gauhar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2562-2669","authenticated-orcid":false,"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1849-9316","authenticated-orcid":false,"given":"Sa\u2019ed","family":"Abed","sequence":"additional","affiliation":[]},{"given":"Imtiaz","family":"Ahmad","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,28]]},"reference":[{"key":"6123_CR1","unstructured":"Abdel-Hamid AT (2001) A hierarchical Verification of the IEEE-$$754$$ Table-driven Floating-point Exponential Function using HOL. PhD thesis, Concordia University"},{"key":"6123_CR2","doi-asserted-by":"crossref","unstructured":"Akbarpour B, Dekdouk A, Tahar S (2002) Formalization of Cadence SPW Fixed-Point Arithmetic in HOL. In: Integrated Formal Methods. LNCS, vol. 2335, pp 185\u2013204. Springer","DOI":"10.1007\/3-540-47884-1_11"},{"key":"6123_CR3","doi-asserted-by":"crossref","unstructured":"Barnat J, Beran J, Brim L, Kratochv\u00edla T, Ro\u010dkai P (2012) Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. In: Formal Methods for Industrial Critical Systems. Springer, pp 78\u201392","DOI":"10.1007\/978-3-642-32469-7_6"},{"key":"6123_CR4","doi-asserted-by":"crossref","unstructured":"Bentley B (2001) Validating the Intel Pentium 4 Microprocessor. In: Design Automation, pp 244\u2013248","DOI":"10.1145\/378239.378473"},{"key":"6123_CR5","doi-asserted-by":"crossref","unstructured":"Berg C (2001) Formal Verification of an IEEE Floating Point Adder. Master\u2019s Thesis, Saarland University, Germany","DOI":"10.1007\/3-540-44798-9_26"},{"key":"6123_CR6","doi-asserted-by":"crossref","unstructured":"Berg C, Jacobi C (2001) Formal Verification of the VAMP Floating-point Unit. In: Correct Hardware Design and Verification Methods. LNCS, vol. 2144. Springer, pp 325\u2013339","DOI":"10.1007\/3-540-44798-9_26"},{"key":"6123_CR7","doi-asserted-by":"crossref","unstructured":"Boldo S, Filli\u00e2tre J-C (2007) Formal verification of floating-point programs. In: Symposium on Computer Arithmetic. IEEE, pp 187\u2013194","DOI":"10.1109\/ARITH.2007.20"},{"issue":"2","key":"6123_CR8","doi-asserted-by":"publisher","first-page":"327","DOI":"10.3390\/electronics9020327","volume":"9","author":"Z Cao","year":"2020","unstructured":"Cao Z, Lv W, Huang Y, Shi J, Li Q (2020) Formal Analysis and Verification of Airborne Software Based on DO-333. Electronics 9(2):327","journal-title":"Electronics"},{"issue":"4","key":"6123_CR9","doi-asserted-by":"publisher","first-page":"1420","DOI":"10.1109\/TR.2018.2873260","volume":"67","author":"L Chaves","year":"2018","unstructured":"Chaves L, Bessa IV, Ismail H, Santos Frutuoso AB, Cordeiro L, Lima Filho EB (2018) DSVerifier-aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles. Trans Reliab 67(4):1420\u20131441","journal-title":"Trans Reliab"},{"key":"6123_CR10","doi-asserted-by":"crossref","unstructured":"Chung SY (2018) Provably Correct Posit Arithmetic with Fixed-point Big Integer. In: Next Generation Arithmetic, pp 1\u201310","DOI":"10.1145\/3190339.3190341"},{"issue":"4","key":"6123_CR11","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Wing JM (1996) Formal Methods: State of the Art and Future Directions. ACM Comput Surv 28(4):626\u2013643","journal-title":"ACM Comput Surv"},{"key":"6123_CR12","doi-asserted-by":"crossref","unstructured":"Cofer D (2012) Formal Methods in the Aerospace Industry: Follow the Money. In: Formal Engineering Methods. Springer, pp 2\u20133","DOI":"10.1007\/978-3-642-34281-3_2"},{"issue":"2","key":"6123_CR13","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1109\/TC.2008.209","volume":"58","author":"M Cornea","year":"2008","unstructured":"Cornea M, Harrison J, Anderson C, Tang PTP, Schneider E, Gvozdev E (2008) A Software Implementation of the IEEE 754R Decimal Floating-point Arithmetic using the Binary Encoding Format. Trans Comput 58(2):148\u2013162","journal-title":"Trans Comput"},{"key":"6123_CR14","doi-asserted-by":"crossref","unstructured":"Daumas M, Rideau L, Th\u00e9ry L (2001) A Generic Library for Floating-point Numbers and its Application to Exact Computing. In: Theorem Proving in Higher Order Logics. LNCS, vol. 2152. Springer, pp 169\u2013184","DOI":"10.1007\/3-540-44755-5_13"},{"issue":"1","key":"6123_CR15","doi-asserted-by":"publisher","first-page":"163","DOI":"10.3390\/electronics11010163","volume":"11","author":"AA Esmaeel","year":"2022","unstructured":"Esmaeel AA, Abed S, Mohd BJ, Fairouz AA et al (2022) POSIT vs. Floating Point in Implementing IIR Notch Filter by Enhancing Radix-4 Modified Booth Multiplier. Electronics 11(1):163","journal-title":"Electronics"},{"key":"6123_CR16","doi-asserted-by":"crossref","unstructured":"Fitzgerald J, Bicarregui J, Larsen PG, Woodcock J (2013) Industrial Deployment of Formal Methods: Trends and Challenges. In: Industrial Deployment of System Engineering Methods. Springer, pp 123\u2013143","DOI":"10.1007\/978-3-642-33170-1_10"},{"key":"6123_CR17","doi-asserted-by":"crossref","unstructured":"Gesellensetter L, Glesner S, Salecker E (2007) Formal Verification with Isabelle\/HOL in Practice: Finding a Bug in the GCC Scheduler. In: Formal Methods for Industrial Critical Systems. Springer, pp 85\u2013100","DOI":"10.1007\/978-3-540-79707-4_8"},{"key":"6123_CR18","unstructured":"Gustafson JL (2017) The End of Error: Unum Computing. CRC Press"},{"key":"6123_CR19","unstructured":"Gustafson JL (2017) Posit Arithmetic. Mathematica Notebook Describing the Posit Number System 30"},{"issue":"2","key":"6123_CR20","first-page":"71","volume":"4","author":"JL Gustafson","year":"2017","unstructured":"Gustafson JL, Yonemoto IT (2017) Beating floating point at its own game: Posit Arithmetic. Supercomput Front Innov 4(2):71\u201386","journal-title":"Supercomput Front Innov"},{"key":"6123_CR21","unstructured":"Harrison J (1996) Formalized Mathematics. Technical Report 36, Turku Centre for Computer Science, Finland"},{"key":"6123_CR22","doi-asserted-by":"crossref","unstructured":"Harrison J (1996) HOL Light: A Tutorial Introduction. In: Srivas M, Camilleri A (eds) Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201996). Lecture Notes in Computer Science, vol. 1166. Springer, pp. 265\u2013269","DOI":"10.1007\/BFb0031814"},{"key":"6123_CR23","doi-asserted-by":"crossref","unstructured":"Harrison J (1997) Floating Point Verification in HOL Light: the Exponential Function. In: Algebraic Methodology and Software Technology. Springer, pp 246\u2013260","DOI":"10.1007\/BFb0000475"},{"key":"6123_CR24","doi-asserted-by":"crossref","unstructured":"Harrison J (1999) A Machine-checked Theory of Floating Point Arithmetic. In: Theorem Proving in Higher Order Logics. Springer, pp 113\u2013130","DOI":"10.1007\/3-540-48256-3_9"},{"key":"6123_CR25","doi-asserted-by":"crossref","unstructured":"Harrison J (2000) Formal Verification of Floating Point Trigonometric Functions. In: Formal Methods in Computer-aided Design. Springer, pp 254\u2013270","DOI":"10.1007\/3-540-40922-X_14"},{"issue":"2","key":"6123_CR26","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1022973506233","volume":"22","author":"J Harrison","year":"2003","unstructured":"Harrison J (2003) Formal Verification of Square Root Algorithms. Formal Methods in System Design 22(2):143\u2013153","journal-title":"Formal Methods in System Design"},{"key":"6123_CR27","doi-asserted-by":"crossref","unstructured":"Harrison J (2006) Floating-point Verification using Theorem Proving. In: Formal Methods for the Design of Computer, Communication and Software Systems. Springer, pp 211\u2013242","DOI":"10.1007\/11757283_8"},{"key":"6123_CR28","doi-asserted-by":"crossref","unstructured":"Harrison J (2006) Towards self-verification of HOL Light. In: International Joint Conference on Automated Reasoning. Springer, pp 177\u2013191","DOI":"10.1007\/11814771_17"},{"key":"6123_CR29","doi-asserted-by":"crossref","unstructured":"Harrison J (2009) Handbook of Practical Logic and Automated Reasoning. Cambridge University Press","DOI":"10.1017\/CBO9780511576430"},{"key":"6123_CR30","unstructured":"Harrison J, Kubaska T, Story S et al (1999) The Computation of Transcendental Functions on the IA-64 Architecture. In: Intel Technology Journal. Citeseer"},{"key":"6123_CR31","unstructured":"https:\/\/github.com\/adrashid\/posits_verification"},{"key":"6123_CR32","unstructured":"https:\/\/shemesh.larc.nasa.gov\/fm\/fm-main-research.html"},{"key":"6123_CR33","unstructured":"https:\/\/shemesh.larc.nasa.gov\/fm\/fm-collins-intro.html"},{"key":"6123_CR34","unstructured":"Jacobi C (2002) Formal Verification of a Fully IEEE Compliant Floating Point Unit"},{"key":"6123_CR35","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.entcs.2015.10.010","volume":"317","author":"C Jacobsen","year":"2015","unstructured":"Jacobsen C, Solovyev A, Gopalakrishnan G (2015) A Parameterized Floating-point Formalizaton in HOL Light. Electron Notes Theor Comput Sci 317:101\u2013107","journal-title":"Electron Notes Theor Comput Sci"},{"key":"6123_CR36","doi-asserted-by":"crossref","unstructured":"Jaiswal MK, So HK-H (2018) Universal Number Posit Arithmetic Generator on FPGA. In: Design, Automation & Test in Europe. IEEE, pp 1159\u20131162","DOI":"10.23919\/DATE.2018.8342187"},{"key":"6123_CR37","doi-asserted-by":"crossref","unstructured":"Jaiswal MK, So HK-H (2018) Architecture Generator for Type-3 Unum Posit Adder\/Subtractor. In: Circuits and Systems. IEEE, pp 1\u20135","DOI":"10.1109\/ISCAS.2018.8351142"},{"key":"6123_CR38","doi-asserted-by":"publisher","first-page":"74586","DOI":"10.1109\/ACCESS.2019.2920936","volume":"7","author":"MK Jaiswal","year":"2019","unstructured":"Jaiswal MK, So HK-H (2019) Pacogen: A Hardware Posit Arithmetic Core Generator. ACCESS 7:74586\u201374601","journal-title":"ACCESS"},{"key":"6123_CR39","doi-asserted-by":"crossref","unstructured":"Johnson CW (2005) The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions. In: Formal Methods. Springer, pp 9\u201325","DOI":"10.1007\/11526841_3"},{"issue":"4","key":"6123_CR40","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1109\/54.936245","volume":"18","author":"RB Jones","year":"2001","unstructured":"Jones RB, O\u2019Leary JW, Seger C-J, Aagaard MD, Melham TF (2001) Practical Formal Verification in Microprocessor Design. Design & Test of Computers 18(4):16\u201325","journal-title":"Design & Test of Computers"},{"key":"6123_CR41","unstructured":"Kaivola R (2011) Intel CoreTM i7 Processor Execution Engine Validation in a Functional Language Based Formal Framework. In: Practical Aspects of Declarative Languages. Springer, pp 414\u2013429"},{"key":"6123_CR42","unstructured":"Kumar R (2016) Self-compilation and Self-verification. Technical report, University of Cambridge, Computer Laboratory"},{"key":"6123_CR43","doi-asserted-by":"crossref","unstructured":"Langroudi HF, Karia V, Gustafson JL, Kudithipudi D (2020) Adaptive Posit: Parameter Aware Numerical Format for Deep Learning Inference on the Edge. In: Computer Vision and Pattern Recognition, pp 726\u2013727","DOI":"10.1109\/CVPRW50498.2020.00371"},{"key":"6123_CR44","doi-asserted-by":"crossref","unstructured":"Langroudi SHF, Pandit T, Kudithipudi D (2018) Deep Learning Inference on Embedded Devices: Fixed-point Vs Posit. In: Energy Efficient Machine Learning and Cognitive Computing for Embedded Applications, pp 19\u201323. IEEE","DOI":"10.1109\/EMC2.2018.00012"},{"key":"6123_CR45","doi-asserted-by":"crossref","unstructured":"Leh\u00f3czky Z, Retzler A, T\u00f3th R, Szab\u00f3 \u00c1, Farkas B, Somogyi K (2018) High-level. NET Software Implementations of Unum Type I and Posit with Simultaneous FPGA Implementation using Hastlayer. In: Next Generation Arithmetic, pp 1\u20137","DOI":"10.1145\/3190339.3190343"},{"key":"6123_CR46","doi-asserted-by":"crossref","unstructured":"Miller S, Anderson E, Wagner L, Whalen M, Heimdahl M (2005) Formal Verification of Flight Critical Software. In: AIAA Guidance, Navigation, and Control Conference and Exhibit, p 6431","DOI":"10.2514\/6.2005-6431"},{"key":"6123_CR47","unstructured":"Miner PS (1995) Defining the IEEE-854 Floating-Point Standard in PVS"},{"key":"6123_CR48","doi-asserted-by":"crossref","unstructured":"Miner PS, Leathrum JF (1996) Verification of IEEE Compliant Subtractive Division Algorithms. In: Formal Methods in Computer-Aided Design. LNCS, vol. 1166. Springer, pp 64\u201378","DOI":"10.1007\/BFb0031800"},{"key":"6123_CR49","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"9","author":"JS Moore","year":"1998","unstructured":"Moore JS, Lynch TW, Kaufmann M (1998) A Mechanically Checked Proof of the AMD5K86TM Floating-point Division Program. IEEE Trans Comput 9:913\u2013926","journal-title":"IEEE Trans Comput"},{"key":"6123_CR50","unstructured":"M\u00fcller SM, Paul WJ (2013) Computer Architecture: Complexity and Correctness. Springer"},{"key":"6123_CR51","doi-asserted-by":"crossref","unstructured":"Murillo R, Del Barrio AA, Botella G (2020) Deep PeNSieve: A Deep Learning Framework based on the Posit Number System. Digit Signal Process 102762","DOI":"10.1016\/j.dsp.2020.102762"},{"key":"6123_CR52","doi-asserted-by":"crossref","unstructured":"Nellen J, Rambow T, Waez MTB, \u00c1brah\u00e1m E, Katoen J-P (2018) Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations. In: Formal Methods. Springer, pp 382\u2013398","DOI":"10.1007\/978-3-319-95582-7_23"},{"key":"6123_CR53","unstructured":"Narasimhan N, Kaivola R (2002) Formal Verification of the Pentium\u00ae 4 Floating-Point Multiplier. In: Design, Automation & Test in Europe. IEEE, pp 1\u20138"},{"key":"6123_CR54","unstructured":"O\u2019Leary J (2009) Theorem Proving in Intel Hardware Design"},{"issue":"1","key":"6123_CR55","first-page":"1","volume":"3","author":"J O\u2019Leary","year":"1999","unstructured":"O\u2019Leary J, Zhao X, Gerth R, Seger C-JH (1999) Formally Verifying IEEE Compliance of Floating-point Hardware. Intel Technol J 3(1):1\u201314","journal-title":"Intel Technol J"},{"key":"6123_CR56","doi-asserted-by":"crossref","unstructured":"Paulson L (1996) ML for the Working Programmer. Cambridge University Press","DOI":"10.1017\/CBO9780511811326"},{"key":"6123_CR57","doi-asserted-by":"crossref","unstructured":"Podobas A, Matsuoka S (2018) Hardware Implementation of POSITs and their Application in FPGAs. In: Parallel and Distributed Processing. IEEE, pp 138\u2013145","DOI":"10.1109\/IPDPSW.2018.00029"},{"key":"6123_CR58","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D Russinoff","year":"1998","unstructured":"Russinoff D (1998) A Mechanically Checked Proof of IEEE Compliance of a Register-transfer-level Specification of the AMD-K7 Floating-point Multiplication, Division, and Square Root Instructions. LMS J Comput Math 1:148\u2013200","journal-title":"LMS J Comput Math"},{"key":"6123_CR59","doi-asserted-by":"crossref","unstructured":"Slobodov\u00e1 A (2008) Formal Verification of Hardware Support for Advanced Encryption Standard. In: Formal Methods in Computer-Aided Design. IEEE, pp 1\u20134","DOI":"10.1109\/FMCAD.2008.ECP.12"},{"issue":"10","key":"6123_CR60","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/MAES.2004.1365014","volume":"19","author":"A Tribble","year":"2004","unstructured":"Tribble A, Miller S (2004) Safety Analysis of Software Intensive Systems. IEEE Aerosp Electron Syst 19(10):21\u201326","journal-title":"IEEE Aerosp Electron Syst"},{"key":"6123_CR61","doi-asserted-by":"crossref","unstructured":"Tribble AC, Lempia D, Miller SP (2002) Software Safety Analysis of a Flight Guidance System. In: Digital Avionics Systems Conference, vol. 2. IEEE, pp 13\u20131131","DOI":"10.1109\/DASC.2002.1053007"},{"key":"6123_CR62","doi-asserted-by":"crossref","unstructured":"Whalen M, Cofer D, Miller S, Krogh BH, Storm W (2007) Integration of Formal Analysis into a Model-based Software Development Process. In: Formal Methods for Industrial Critical Systems. Springer, pp 68\u201384","DOI":"10.1007\/978-3-540-79707-4_7"},{"key":"6123_CR63","unstructured":"Wiels V, Delmas R, Doose D, Garoche P-L, Cazin J, Durrieu G (2012) Formal Verification of Critical Aerospace Software. AerospaceLab 1(4)"},{"issue":"12","key":"6123_CR64","doi-asserted-by":"publisher","first-page":"0167168","DOI":"10.1371\/journal.pone.0167168","volume":"11","author":"H Xu","year":"2016","unstructured":"Xu H, Wang P (2016) Real-time Reliability Verification for UAV Flight Control System Supporting Airworthiness Certification. PloS ONE 11(12):0167168","journal-title":"PloS ONE"},{"key":"6123_CR65","unstructured":"Zhang F, Niu W et al (2019) A Survey on Formal Specification and Verification of System-level Achievements in Industrial Circles. Acad J Comput Inform Sci 2(1)"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-024-06123-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10836-024-06123-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-024-06123-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T23:12:15Z","timestamp":1732317135000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10836-024-06123-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6]]},"references-count":65,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["6123"],"URL":"https:\/\/doi.org\/10.1007\/s10836-024-06123-9","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"type":"print","value":"0923-8174"},{"type":"electronic","value":"1573-0727"}],"subject":[],"published":{"date-parts":[[2024,6]]},"assertion":[{"value":"8 December 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 June 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"There is no conflict of interest for our article entitled \u201cFormal Verification of Universal Numbers using Theorem Proving\u201d submitted in Journal of Electronic Testing.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of Interest"}}]}}