1、隨著軟件的廣泛應(yīng)用，用戶在追求滿足越來(lái)越復(fù)雜的邏輯功能的同時(shí)也在追求高安全、高可靠的軟件。數(shù)組越界錯(cuò)誤是一類常見的運(yùn)行時(shí)錯(cuò)誤，已經(jīng)成為影響程序正常運(yùn)行的重大隱患。
　　數(shù)組本質(zhì)上可看作是下標(biāo)變量到數(shù)組元素的映射。基于這一思想，本文將數(shù)組越界問(wèn)題轉(zhuǎn)換為程序變量值范圍分析問(wèn)題。抽象解釋為程序靜態(tài)分析提供了理論基礎(chǔ)，可在編譯時(shí)自動(dòng)分析出程序中變量的取值范圍?；谠摷夹g(shù)，本文建立了支持?jǐn)?shù)組越界檢查的數(shù)值程序靜態(tài)分析框架。該框架包括前端預(yù)處

2、理、抽象域庫(kù)和不動(dòng)點(diǎn)求解器三個(gè)模塊，其中面向數(shù)組分析的抽象域的設(shè)計(jì)是實(shí)現(xiàn)數(shù)組越界檢查的關(guān)鍵，也是本文的重點(diǎn)工作。
　　為了支持面向數(shù)組的分析，本文從不同精度與可擴(kuò)展性需要出發(fā)，設(shè)計(jì)并實(shí)現(xiàn)了兩類面向數(shù)組分析的抽象域:
　　1、基于合并語(yǔ)義的抽象域arrayMerge。為了獲得高可擴(kuò)展性，本文把整個(gè)數(shù)組抽象成一個(gè)單獨(dú)的區(qū)間變量來(lái)處理，設(shè)計(jì)并開發(fā)了相應(yīng)抽象域arrayMerge;
　　2、基于分離語(yǔ)義的抽象域arraySma