Model Checking with Multi-threaded IC3 Portfolios

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9583
• 期：1
• 页码：517-535
• 全文大小：727 KB
• 参考文献：1.Albarghouthi, A., Kumar, R., Nori, A.V., Rajamani, S.K.: Parallelizing top-down interprocedural analyses. In: Vitek, J., Lin, H., Tip, F. (eds.) Proceedings of the ACM SIGPLAN 2012 Conference on Programming Language Design and Implementation (PLDI 2012), pp. 217–228. Association for Computing Machinery, Beijing, China, June 2012
  2.Ansel, J., Kamil, S., Veeramachaneni, K., Ragan-Kelley, J., Bosboom, J., O’Reilly, U., Amarasinghe, S.P.: OpenTuner: an extensible framework for program autotuning. In: Amaral, J.N., Torrellas, J. (eds.) Proceedings of the 23rd International Conference on Parallel Architectures and Compilation (PACT 2014), pp. 303–316. Association for Computing Machinery, Edmonton, AB, Canada, August 2014
  3.Barnat, J., et al.: DiVinE 3.0 - an explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV. Lecture Notes in Computer Science, vol. 8044, pp. 863–868. Springer, Saint Petersburg (2013)CrossRef
  4.Bingham, B., Bingham, J., Erickson, J., de Paula, F.M., Reitblatt, M., Singh, G.: Industrial strength distributed explicit state model checking. In: Proceedings of the 9th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2010), Twente, The Netherlands, September-October 2010
  5. Blom, S., van de Pol, J., Weber, M.: LTSmin : distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010) CrossRef
  6. Bradley, A.R.: SAT-Based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011) CrossRef
  7.Chaki, S., Karimi, D.: Model Checking with Multi-Threaded IC3 Portfolios (2016), Extended version of this paper. http://​www.​contrib.​andrew.​cmu.​edu/​~schaki/​publications/​VMCAI-2016-Extended.​pdf
  8. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012) CrossRef
  9. Ditter, A., Ceska, M., Lüttgen, G.: On parallel software verification using boolean equation systems. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 80–97. Springer, Heidelberg (2012) CrossRef
  10.Eén, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proceedings of the 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2011), pp. 125–134. IEEE Computer Society, Austin, TX, October-November 2011
  11. de Haan, L., Ferreira, A.: Extreme Value Theory: An Introduction. Springer, New York (2006) CrossRef
  12. Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012) CrossRef
  13. Holzmann, G.J.: Parallelizing the spin model checker. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 155–171. Springer, Heidelberg (2012) CrossRef
  14. Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 454–469. Springer, Heidelberg (2011) CrossRef
  15. Lopes, N.P., Rybalchenko, A.: Distributed and predictable software model checking. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 340–355. Springer, Heidelberg (2011) CrossRef
  16. Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Boosting sequential solver portfolios: knowledge sharing and accuracy prediction. In: Nicosia, G., Pardalos, P. (eds.) LION 7. LNCS, vol. 7997, pp. 153–167. Springer, Heidelberg (2013) CrossRef
  17. Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G.C.: Parallel and distributed model checking in eddy. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 108–125. Springer, Heidelberg (2006) CrossRef
  18. Palikareva, H., Cadar, C.: Multi-solver support in symbolic execution. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 53–68. Springer, Heidelberg (2013) CrossRef
  19.Ppfolio website. http://​www.​cril.​univ-artois.​fr/​~roussel/​ppfolio
  20.Weibull, W.: A statistical distribution function of wide applicability. ASME J. Appl. Mech. 18(3), 293–297 (1951)MATH
  21. Wintersteiger, C.M., Hamadi, Y., de Moura, L.: A concurrent portfolio approach to SMT solving. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 715–720. Springer, Heidelberg (2009) CrossRef
  22.Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. (JAIR) 32, 565–606 (2008)MATH
  
• 作者单位：Sagar Chaki (15)
  Derrick Karimi (15) (16)
  
  15. Software Engineering Institute, Carnegie Mellon University, Pittsburgh, USA
  16. Carnegie Robotics, Pittsburgh, USA
  
• 丛书名：Verification, Model Checking, and Abstract Interpretation
• ISBN：978-3-662-49122-5
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Three variants of multi-threaded ic3 are presented. Each variant has a fixed number of ic3s running in parallel, and communicating by sharing lemmas. They differ in the degree of synchronization between threads, and the aggressiveness with which proofs are checked. The correctness of all three variants is shown. The variants have unpredictable runtime. On the same input, the time to find the solution over different runs varies randomly depending on the thread interleaving. The use of a portfolio of solvers to maximize the likelihood of a quick solution is investigated. Using the Extreme Value theorem, the runtime of each variant, as well as their portfolios is analyzed statistically. A formula for the portfolio size needed to achieve a verification time with high probability is derived, and validated empirically. Using a portfolio of 20 parallel ic3s, speedups over 300 are observed compared to the sequential ic3 on hardware model checking competition examples. The use of parameter sweeping to implement a solver that performs well over a wide range of problems with unknown “hardness” is investigated.