Program Testing with PAC Guarantees

在本篇論文中，我們介紹並實作了兩個針對線性程式實施軟體測試與模型合成的方法，分別基於學習與抽樣。利用這兩個全新的方式，我們希望能夠在提供一個量化的保證與合理的資源耗用下，減低軟體測試與正規驗證之間的分別。 本篇論文中，基於學習機制的方式的進行，是從學習一個程式所有可行的執行軌跡之集合開始，得出一模擬此集合的模型，再利用測試來觀察此模型是否包含了錯誤的行為。準確的學習演算法需要保證模型與程式的完全相似，而此問題基本上是無法決定的。因此，我們的學習機制利用了Probably Approximately Correct (PAC)學習架構，其特色為應用抽樣來解決模型與程式是否相同的問題，並且利用名為錯誤率(error probability)與信心水平(confidence level)的參數來提供正確性的保證。除此之外，我們的基於學習機制之方式也會將模擬程式行為的模型輸出，此模型也保有上述之正確性保證。 我們並提出了另外一個基於取樣來實作的方式。此法也是根據PAC學習機制來提供正確性的保證。我們利用了具象符號測試(Concolic Testing)工具來作為我們的取樣者，並從程式中抽取特定數量的執行軌跡。最終，再從已抽取之執行軌跡的集合中分析，來提供關於正確性的保證，從中找到錯誤執行軌跡，或是因為計算資源的不足而無法完成分析。 我們實作了一個稱為Pac-Man 的工具，此工具提供兩種運行模式，分別實作了上述所提及之兩種機制。除此之外，我們在實驗中所獲得的初步結果中，Pac-Man的表現相當優異，在某些範例上甚至超越了一些已經成熟的軟體驗證工具。因此，我們將Pac-Man 提交至2016年軟體驗證競賽(Software Verification Competition)。在競賽中的遞迴(Recursive)項目中我們獲得了第五名，而在陣列可到達性 (Array-reach)項項目中我們則是得到了第四名。另外，我們將一篇描述了基於學習機制的方式之論文提交至2016年國際軟體工程會議(International Conference on Software Engineering)，並且成功地被採用。In this work, we introduce two novel techniques for software testing and model synthesis of sequential programs, the learning-based and the sampling-based techniques. With these two techinques, we hope to diminish the distinctions between software testing and formal verification by providing a statistical guarantee while being scalable. Our learning-based technique is based on learning a regular model of the set of feasible paths in a program, and testing whether this model contains an incorrect behavior. Exact learning algorithms require checking equivalence between the model and the program, which is in general undecidable. Our learning procedure is therefore based on the framework of probably approximately correct (PAC) learning, which uses sampling instead and provides correctness guarantees expressed using the terms error probability and confidence level. In addition, our procedure also outputs the model with the said correctness guarantees. Another technique we propose is the sampling-based approach, which is also based on the guarantees provided by PAC learning. We utilized concolic testers as samplers to obtain samples of execution traces of the program-under-tests, then conclude whether the programs contain feasible error traces, are free from error with PAC guarantee, or are of unknown results due to insufficient computational resources. We implemented the abovementioned two techniques with a prototype called Pac-Man. Furthermore, obtained preliminary experiments show encouraging results, in some cases even outperforming mature software verifiers. As a result, we submitted Pac-Man''s implementation of the sampling-based techinque to participate in Software Verification Competition (SV-COMP) 2016. We ranked 5th in the recursive subcategory, and 4th in the array-reach subcategory. Moreover, we submitted a paper illustrating the learning-based procedure to the International Conference on Software Engineering (ICSE) 2016, and was successfully accepted