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

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

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

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

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

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

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

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

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

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