布爾可滿足性(Boolean satisfiability)的概念正在被用于確定軟件代碼中的“bug”，從而保證代碼基本上不存在bug，滿足編程者的愿望。

在2007年嵌入系統(tǒng)會(huì)議上，Coverity宣布了據(jù)稱是第一種基于布爾可滿足性(SAT)的源代碼分析引擎。Coverity公司的SAT引擎利用了它的軟件DNA圖譜，自動(dòng)、正確和精確地確定源代碼中的缺陷。該軟件DNA圖譜精確地代表人們已寫(xiě)出來(lái)的任何軟件。

Coverity在企業(yè)應(yīng)用領(lǐng)域是領(lǐng)導(dǎo)廠商。它的靜態(tài)分析軟件客戶包括財(cái)富500強(qiáng)上面57%的軟件公司和50%的電腦外設(shè)公司。它的主要產(chǎn)品是Prevent Software Quality System (SQS)，SQS通過(guò)在編譯時(shí)解析源代碼來(lái)使復(fù)雜軟件中的缺陷和安全漏洞檢測(cè)實(shí)現(xiàn)自動(dòng)化。

目前的靜態(tài)分析引擎依賴數(shù)據(jù)流分析和多個(gè)檢驗(yàn)程序來(lái)確定軟件缺陷。與此不同的是，SAT引擎基于布爾可滿足性，將能支持多個(gè)解算程序確定軟件缺陷。

這種新的軟件代碼分析方法，得益于Coverity正在申請(qǐng)專利的技術(shù)，該技術(shù)以精確到位(bit)的精度代表軟件系統(tǒng)，每個(gè)相關(guān)軟件運(yùn)算都被翻譯成布爾值真(true)與假(false)和布爾運(yùn)算符(Not邏輯非)、and(邏輯與)、or(邏輯或)。這允許利用基于SAT的解算程序?qū)υ创a進(jìn)行分析，這在商業(yè)電腦編程領(lǐng)域還是第一次。

300多家客戶已經(jīng)在依靠Coverity Prevent SQS來(lái)分析其應(yīng)用程序中的每個(gè)路徑。通過(guò)利用SAT，Prevent SQS不僅能夠分析每個(gè)路徑，而且能夠分析這些路徑之中每次計(jì)算中的每個(gè)值。Chelf表示，這樣徹底的靜態(tài)代碼分析，實(shí)現(xiàn)了業(yè)內(nèi)對(duì)關(guān)鍵性能和安全漏洞的最精確鑒定。

據(jù)Forrester Research的安全與風(fēng)險(xiǎn)管理部門(mén)的首席分析師Chenxi Wang，“可滿足性”原理用于硬件檢驗(yàn)已有一段時(shí)間，但以前從未用于軟件檢驗(yàn)。

Wang認(rèn)為，還有創(chuàng)新空間，具體而言是在嵌入軟件領(lǐng)域。“嵌入軟件通常在復(fù)雜性和狀態(tài)數(shù)量方面比普通應(yīng)用軟件受到的限制多一點(diǎn)，因此，SAT更可能在嵌入編程領(lǐng)域增強(qiáng)軟件驗(yàn)證的水平。”

Coverity的Chelf表示，“靜態(tài)分析方法一直成功地用于EDA產(chǎn)業(yè)。我們只是把電路設(shè)計(jì)工作中使用的同樣的軟件布爾原理用于軟件代碼領(lǐng)域。”

Coverity Prevent SQS的基礎(chǔ)技術(shù)是20世紀(jì)90年代在斯坦福大學(xué)電腦系統(tǒng)實(shí)驗(yàn)室開(kāi)發(fā)出來(lái)的，當(dāng)時(shí)在此工作的Ben Chelf和同事把該技術(shù)用于商業(yè)應(yīng)用。