關於程序分析領域的研究現狀和熱點趨勢？

01-29

大概是要入程序分析這個坑了，想向大牛們請教一下這個方向的研究現狀和熱點趨勢。
先說一下我自己的一點點宏觀上的了解：
程序分析這個領域很大，涉及編程語言理論（計算理論、類型系統、編譯原理、並行計算等），軟體安全，並發分析，軟體測試方法，形式化驗證，程序優化以及體系結構等等，可以相當理論，也可以偏工程。
我其實就是想在這個大領域裡找到一個比較熱門的適合自己的小方向，做下去。
曾大致瞄過POPL/PLDI/OSDI/SOSP/FSE/ICSE/ASPLOS這種相關的會議上最近兩三年的論文，奈何功底太淺（本人算是半路出家的碼農），很多也都是看得一知半解，只是模糊的感覺關於並發分析的論文貌似不少（？），比如並發bug檢測修復這種。由於功底比較薄弱，不知自己的判斷是否準確，所以心裡一直不怎麼踏實。另外還有哪些方向比較熱門，有哪些牛的研究小組，希望有了解這方面的大牛們指點一二，不勝感激！！！

ps: 不想搞特別理論的方向，太難了hold不住
pps: 本人搞過binary translation（做過相關項目，工程性的），對llvm也有一定的了解（讀過一部分源碼，知道整體架構，寫過簡單的pass）
ppps: 不要問我為什麼不去找導師，哎老闆一心開公司賺錢，項目風馬牛不相及，說起來都是淚，只求發夠論文順利畢業
pppps: 對了，符號執行貌似前幾年還挺熱，現在還行嗎？作為博士研究方向怎麼樣？

@姚培森說的那幾個researcher你多關注一下，特別是Tom Reps和Isil Dillig，基本上吃透他們的文章就吃透最有用的前沿技術了。這點我可以打包票，因為我把他們的很多演算法改進實現在自己的工具里，確實靠譜。

傳統的Symbolic Execution這幾年火就是因為Z3等SMT技術的進步煥發了青春。不過實話，symbolic execution被微軟的YOGI和SAGE項目提高了不少（他們的方案其實叫concolic execution），但處理framework intensive software的能力還是非常有限，同時concolic execution的coverage還是不夠好。CMU cylab的Veritesting算是動靜結合相互彌補不足的一個典範，可以看看他們的概述文章：http://users.ece.cmu.edu/~aavgerin/papers/veritesting-icse-2014.pdf。我目前的研究就是modular symbolic abstract interpretation，我覺得這個是未來的方向：既100% coverage，又通過modular方案可以處理very large code base，還可以通過symbolic-abstraction的trade-off調節精度和效率。

正在開APLAS"15，還有一些事情要處理，先回答到這兒。明天 Peter O』Hearn 做verification的invited talk。聽完之後再來更一下。

---9.29更新---

程序分析技術和應用範圍都很廣，本人水平有限，只對模型檢查、抽象解釋相關的了解一些。

個人關注下面幾個學術會議比較多，可以從中找程序分析相關的：

偏程序語言的POPL，PLDI，ICFP，OOPSLA等；

偏安全，USENIX Securiy, IEEE SP, ACM CCS, NDSS, CSF等也可關注；

其他比較「雜」的：LICS，CAV，ESOP， SAS，VMCAI，TACAS，FSE，ISSTA乃至ICALP等；

也有很多優秀的研究小組值得關註：Thomas Reps ，Mooly Sagiv，Tom Ball，Alex Aiken，Isil Dillig，Patrik Cousot，Summit Gulwani，Dirk Beyer，Ken Mcllian，Mayur Naik，Martin rinard，Neil Jones ，Jens Palsberg 等等.....有些可能比較「冷門」但也很有意思，比如Javier Esparza（數據流分析x模型檢查，數據流分析x牛頓法..），Roberto Giacobazzi...當然偏security/system/的也很多，不一一列舉...

希望有所幫助。

基本同意姚培森所說。從根本上來講，程序分析無非就是精度和效率的組合，雖然經過了很多年的發展，我覺得程序分析技術還是有一些顯著不足：

1. 抽象程度還不夠高。雖然有很多不同的抽象技術，但現有的抽象和人對程序的抽象理解方式還有很大差別，個人感覺還有很大提高空間。

2. 各種技術獨立發展很深，彼此之間互相不能溝通。搞指針分析的不懂模型檢查，搞符號執行的不懂上下文無關語言可達性。抽象解釋是往這個方面做的努力，但一方面普通人理解起來比較難，另一方面統一的內容還比較少。

但話說回來，作為沒有老闆支持的學生我不鼓勵探索這些大的問題，那樣可能很多年都沒有論文。可以考慮一些新的發展點。前面說的符號執行我反倒是覺得是一個很好的點，符號執行發展時間較短，其實可以探索的點還有很多。我感覺可能簡單的把模型檢查中的一些技術拿過來就可以起作用。

我自己寫的論文閱讀筆記。是關於並行程序分析的。老師出國了，誰都問不到。

@熊英飛我到現在都不知道BMC和predicate abstraction 有什麼區別。

隨著多核處理器的高速發展，為充分發揮多核處理器的強大計算能力，並發程序應用得越來越廣泛。並發系統會根據實際運行情況，通過消息隊列或者共享內存的通訊方式，動態的調度處理多個任務做並發處理。然而，在並發軟體中任何潛在在的缺陷或錯誤都可能導致系統運行狀態異常，甚至崩潰。為了防止這些問題，一種有效方式是採用模型檢驗工具來分析此類系統安全性。

公司裡面現在有大量的項目是用Java語言寫成，希望有一種工具可以對Java代碼中的可達性，指針指向問題模型檢測，在代碼提交階段就檢測出可能存在的問題。

模型檢測[1][2]是通過對模型狀態空間做窮舉搜索，檢測整個模型內是否具有滿足規約的屬性，若不滿足的話則提供一個反例作為錯誤報告，此過程能夠自動地進行驗證。

Thomas R， Susan H和Mooly S把單線程遞歸程序的數據流一大類問題，轉換為IFDS (interprocedural, finite, distributive, subset problems) 框架，並把語句和謂詞轉換為圖內結點，並用圖可達演算法在多項式時間內解決程序可達性問題[3]。之後Thomas R等又基於自動機理論把用下推自動機高效重新定義了這個問題[4]。

然而當並發模型包含遞歸過程調用時，如果系統有上下文切換，其可達性問題是不可判定[5]。為了繞過不可判定性,提出了種種方法。

Jhala等人[9]根據IFDS模型，提出基於消息計數器限界的方法，把非同步程序的數據流問題轉換為AIFDS模型，但是他們的演算法不能處理遞歸程序。Jhala等人已經把他們的演算法用於BLAST程序[9]。

通過限定不同進程切換時的堆棧狀態。也可以繞過不可判定性。Sen K[7]和La Torre[8]提出了良序消息隊列(well-queuing)要求：即僅當進程的局部棧為空時，進程才能從消息隊列中讀取消息，並且進程間不共享內存，這樣的系統是可判定的[8]。

並發程序的狀態可達的可判定的演算法，這種演算法對非同步程序通訊結構需要種種限制（不能使用共享內存，線程之間必須要通過消息傳遞,進程的局部堆棧也有規定）[8]。

Qadeer等人提出並發系統的上下文定界分析[6] (bounded-context analysis BCA)，對於基於共享變數通信的遞歸布爾程序上，限定上下文切換次數，可以設計出一個半可定的過程內，判定程序的狀態是否正確。這個過程可以理解為如果限定在k次上下文切換內，程序狀態已經錯誤，那麼程序必定會運行錯誤，如果某些狀態不可達，那麼他們是否正確還是不可判定的。這個方法已經可以在一個很小的上下文切換下，檢測出程序錯誤。

Thomas R等人通過把上下問定界分析（context-bounded analysis CBA）和和利用下推自動機（pushdown system PDS）模型，給出了一種把並發程序序列化的方法[20]。

La Torre等人通過把上下問定界分析和下推自動機結合起來，提出k-round多棧可見下推自動機[22](k-round multi-stack visibly pushdown automaton)，再進一步提出了了階段限定匹配關係多棧下推自動機[23](scope-Bounded Matching Relations multi-stack visibly pushdown automaton)。這些自動機的closure properties和decision problems都是可判定的。

Omar Inverso基於上下問定界分析和Thomas R 的序列化方法[20]，把一個多線程C語言程序轉換為非確定的序列化的C語言代碼，在給定輪訓限定次數k，這個代碼能保留了k個輪詢調度[24]。這些序列化代碼，可以被其他後端分析程序使用。並且他實現了一個C語言版本的多線程程序序列化程序，這個程序獲得了SV-COMP14金牌[25]。

基於有界模型檢測技術(bounded model-checking)開發的程序有JMoped[11]，BLITZ[12]，CBMC[13]，ESBMC[14]，LLBMC[15]。

基於謂詞抽象（predicate abstraction），不合理反例引導精化抽象(Counter Example Guided Abstraction Refinement, CEGAR)[17]的思想，做模型驗證，例如SATABS[18]， CPAchecker[19]。

[1]Clarke E M. Model checking[M]. MIT Press, 2001.

[2]Baier C, Katoen J P. Principles of Model Checking[J]. Mit Press, 2008.

[3]Reps T, Horwitz S, Sagiv M. Precise Interprocedural Dataflow Analysis via Graph Reachability.[C]// ACM Sigplan-Sigact Symposium on Principles of Programming Languages. 1995:49-61.

[4]Reps T, Schwoon S, Jha S, et al. Weighted pushdown systems and their application to interprocedural dataflow analysis ☆[J]. Science of Computer Programming, 2005, 58(1–2):206-263.

[5] Ramalingam G. Context-Sensitive Synchronization-Sensitive Analysis is Undecidable[J]. Acm Transactions on Programming Languages Systems, 1999, 22(2):2000.

[6] Qadeer S, Rehof J. Context-Bounded Model Checking of Concurrent Software[M]// Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2005:93-107.

[7] Sen K, Viswanathan M. Model Checking Multithreaded Programs with Asynchronous Atomic Methods[C]// Proceedings of the 18th international conference on Computer Aided Verification. Springer-Verlag, 2006:300-314.

[8] La Torre S, Madhusudan P, Parlato G. Context-Bounded Analysis of Concurrent Queue Systems[C]// International Conference on Theory Practice of Software. Springer, 2008:299-314.

[9] Jhala R, Majumdar R. Interprocedural analysis of asynchronous programs[J]. Acm Sigplan Notices, 2007, 42(1):339-350.

[10] La Torre S, Madhusudan P, Parlato G. A Robust Class of Context-Sensitive Languages[C]// Proceedings - Symposium on Logic in Computer Science. 2007:161-170.

[11] Suwimonteerabuth D, Esparza J, Schwoon S. Symbolic Context-Bounded Analysis of Multithreaded Java Programs[C]// Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings. 2008:270-287.

[12] Cho C Y, D"Silva V, Song D. BLITZ: Compositional bounded model checking for real-world programs[C]// Ieee/acm International Conference on Automated Software Engineering. 2013:136-146.

[13] Clarke E, Kroening D, Lerda F. A Tool for Checking ANSI-C Programs[M]// Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2004:168-176.

[14] Cordeiro L, Fischer B, Marques-Silva J. SMT-Based Bounded Model Checking for Embedded ANSI-C Software[J]. IEEE Transactions on Software Engineering, 2011, 38(4):957-974.

[15] Merz F, Falke S, Sinz C. LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR.[C]// Verified Software: Theories, Tools, Experiments - International Conference, Vstte 2012, Philadelphia, Pa, Usa, January 28-29, 2012. Proceedings. 2012:146-161.

[16] Beyer D, Keremoglu M E. CPAchecker : A Tool for Configurable Software Verification[J]. Lecture Notes in Computer Science, 2011, 6806:184-190.

[17] Clarke E, Grumberg O, Jha S, et al. Counterexample-Guided Abstraction Refinement[M]// Computer Aided Verification. Springer Berlin Heidelberg, 2000:154-169.

[18] Clarke E, Kroening D, Sharygina N, et al. SATABS: SAT-Based Predicate Abstraction for ANSI-C.[C]// International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2005:570-574.

[19] Beyer D, Keremoglu M E. CPAchecker : A Tool for Configurable Software Verification[J]. Lecture Notes in Computer Science, 2011, 6806:184-190.

[20] Torre S L, Madhusudan P, Parlato G. The Language Theory of Bounded Context-Switching[M]// LATIN 2010: Theoretical Informatics. Springer Berlin Heidelberg, 2010:96-107.

[21] Lal A, Reps T. Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis[J]. Formal Methods in System Design, 2008, 35(1):73-97.

[22] Torre S L, Madhusudan P, Parlato G. The Language Theory of Bounded Context-Switching[M]// LATIN 2010: Theoretical Informatics. Springer Berlin Heidelberg, 2010:96-107.

[23] Torre S L, Napoli M, Parlato G. Scope-Bounded Pushdown Languages[C]// International Conference on Developments in Language Theory. 2014:116-128.

[24] Inverso O, Tomasco E, Fischer B, et al. Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization[C]// Int"l Conference on Computer Aided Verification. 2014:585-602.

[25] Beyer D. Status Report on Software Verification (Competition Summary SV-COMP 2014)[C]// International Conference on TOOLS and Algorithms for the Construction and of Analysis Systems. 2014.