基于SVM的多項(xiàng)式循環(huán)程序秩函數(shù)生成
作者：李軼; 蔡天訓(xùn); 樊建峰; 吳文淵; 馮勇 中國科學(xué)院重慶綠色智能技術(shù)研究院自動(dòng)推理與認(rèn)知重慶市重點(diǎn)實(shí)驗(yàn)室; 重慶400714; 薩基姆通訊(深圳)有限公司; 廣東深圳518000; 中國科學(xué)院大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院; 北京100093
摘要：程序終止性問題是自動(dòng)程序驗(yàn)證領(lǐng)域中的一個(gè)研究熱點(diǎn)。秩函數(shù)探測是進(jìn)行終止性分析的主要方法。針對單重?zé)o條件分支的多項(xiàng)式循環(huán)程序,將其秩函數(shù)計(jì)算問題歸結(jié)為二分類問題,從而可利用支持向量機(jī)(SVM)算法來計(jì)算程序的秩函數(shù)。與基于量詞消去技術(shù)的秩函數(shù)計(jì)算方法不同,該方法能在可接受的時(shí)間范圍內(nèi)探測到更為復(fù)雜的秩函數(shù)。
注：因版權(quán)方要求，不能公開全文，如需全文，請咨詢雜志社
相關(guān)熱門期刊
