Refinement Selection
详细信息    查看全文
  • 刊名：Lecture Notes in Computer Science
  • 出版年：2015
  • 出版时间：2015
  • 年：2015
  • 卷：9232
  • 期：1
  • 页码：20-38
  • 全文大小：594 KB
  • 参考文献：1.Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63–109 (2014)CrossRef
    2. Apel, S., Beyer, D., Friedberger, K., Raimondi, F., von Rhein, A.: Domain types: abstract-domain selection based on variable usage. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 262–278. Springer, Heidelberg (2013) CrossRef
    3. Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004) CrossRef
    4.Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011)CrossRef
    5.Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) POPL 2002. pp. 1–3. ACM, New York (2002)
    6. Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401–416. Springer, Heidelberg (2015)
    7.Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5–6), 505–525 (2007)CrossRef
    8.Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: ASE 2008, pp. 29–38. IEEE (2008)
    9. Beyer, D., Keremoglu, M.E.: CPAchecker : a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011) CrossRef
    10.Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD 2010, pp. 189–197. FMCAD, IEEE (2010)
    11. Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varró, D. (eds.) FASE 2013 (ETAPS 2013). LNCS, vol. 7793, pp. 146–162. Springer, Heidelberg (2013) CrossRef
    12.Beyer, D., Löwe, S., Wendler, P.: Benchmarking and resource measurement. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, pp. 160–178. Springer, Heidelberg (2015)
    13. Beyer, D., Löwe, S., Wendler, P.: Sliced path prefixes: an effective method to enable refinement selection. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 228–243. Springer, Heidelberg (2015) CrossRef
    14.Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Cytron, R., Gupta, R. (eds.) PLDI 2003, pp. 196–207. ACM, New York (2003)
    15. Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol : an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012) CrossRef
    16. Cimatti, A., Griggio, A., Sebastiani, R.: A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 334–339. Springer, Heidelberg (2007) CrossRef
    17.Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNet CrossRef
    18.Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)MATH MathSciNet CrossRef
    19.Demyanova, Y., Veith, H., Zuleger, F.: On the concept of variable roles and its use in software analysis. In: FMCAD 2013, pp. 226–230. IEEE (2013)
    20. D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129–145. Springer, Heidelberg (2010) CrossRef
    21. Graf, S., Saïdi, H.: Construction of abstract state graphs with Pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997) CrossRef
    22.Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) POPL 2004. pp. 232–244. ACM, New York (2004)
    23.Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Launchbury, J., Mitchell, J.C. (eds.) POPL 2002. pp. 58–70. ACM, New York (2002)
    24.Jhala, R., Majumdar, R.: Path slicing. In: Sarkar, V., Hall, M.W. (eds.) PLDI 2005. pp. 38–47. ACM, New York (2005)
    25. Khoroshilov, A., Mutilin, V., Petrenko, A., Zakharov, V.: Establishing linux driver verification process. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 165–176. Springer, Heidelberg (2010) CrossRef
    26. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) CrossRef
    27.Rümmer, P., Subotic, P.: Exploring interpolants. In: FMCAD 2013. pp. 69–76. IEEE (2013)
    28.Sajaniemi, J.: An empirical analysis of roles of variables in novice-level procedural programs. In: HCC 2002. pp. 37–39. IEEE (2002)
    29.van Deursen, A., Moonen, L.: Understanding COBOL systems using inferred types. In: IWPC 1999. pp. 74–81. IEEE (1999)
  • 作者单位：Dirk Beyer (15)
    Stefan Löwe (15)
    Philipp Wendler (15)

    15. University of Passau, Passau, Germany
  • 丛书名：Model Checking Software
  • ISBN：978-3-319-23404-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
文摘
Counterexample-guided abstraction refinement (CEGAR) is a property-directed approach for the automatic construction of an abstract model for a given system. The approach learns information from infeasible error paths in order to refine the abstract model. We address the problem of selecting which information to learn from a given infeasible error path. In previous work, we presented a method that enables refinement selection by extracting a set of sliced prefixes from a given infeasible error path, each of which represents a different reason for infeasibility of the error path and thus, a possible way to refine the abstract model. In this work, we (1) define and investigate several promising heuristics for selecting an appropriate precision for refinement, and (2) propose a new combination of a value analysis and a predicate analysis that does not only find out which information to learn from an infeasible error path, but automatically decides which analysis should be preferred for a refinement. These contributions allow a more systematic refinement strategy for CEGAR-based analyses. We evaluated the idea on software verification. We provide an implementation of the new concepts in the verification framework and make it publicly available. In a thorough experimental study, we show that refinement selection often avoids state-space explosion where existing approaches diverge, and that it can be even more powerful if applied on a higher level, where it decides which analysis of a combination should be favored for a refinement. Page %P Close Plain text Look Inside Chapter Metrics Provided by Bookmetrix Reference tools Export citation EndNote (.ENW) JabRef (.BIB) Mendeley (.BIB) Papers (.RIS) Zotero (.RIS) BibTeX (.BIB) Add to Papers Other actions About this Book Reprints and Permissions Share Share this content on Facebook Share this content on Twitter Share this content on LinkedIn Supplementary Material (0) References (29) References1.Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63–109 (2014)CrossRef2. Apel, S., Beyer, D., Friedberger, K., Raimondi, F., von Rhein, A.: Domain types: abstract-domain selection based on variable usage. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 262–278. Springer, Heidelberg (2013) CrossRef3. Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004) CrossRef4.Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68–76 (2011)CrossRef5.Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) POPL 2002. pp. 1–3. ACM, New York (2002)6. Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401–416. Springer, Heidelberg (2015) 7.Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5–6), 505–525 (2007)CrossRef8.Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: ASE 2008, pp. 29–38. IEEE (2008)9. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011) CrossRef10.Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD 2010, pp. 189–197. FMCAD, IEEE (2010)11. Beyer, D., Löwe, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varró, D. (eds.) FASE 2013 (ETAPS 2013). LNCS, vol. 7793, pp. 146–162. Springer, Heidelberg (2013) CrossRef12.Beyer, D., Löwe, S., Wendler, P.: Benchmarking and resource measurement. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, pp. 160–178. Springer, Heidelberg (2015)13. Beyer, D., Löwe, S., Wendler, P.: Sliced path prefixes: an effective method to enable refinement selection. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 228–243. Springer, Heidelberg (2015) CrossRef14.Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Cytron, R., Gupta, R. (eds.) PLDI 2003, pp. 196–207. ACM, New York (2003)15. Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012) CrossRef16. Cimatti, A., Griggio, A., Sebastiani, R.: A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 334–339. Springer, Heidelberg (2007) CrossRef17.Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetCrossRef18.Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)MATHMathSciNetCrossRef19.Demyanova, Y., Veith, H., Zuleger, F.: On the concept of variable roles and its use in software analysis. In: FMCAD 2013, pp. 226–230. IEEE (2013)20. D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129–145. Springer, Heidelberg (2010) CrossRef21. Graf, S., Saïdi, H.: Construction of abstract state graphs with Pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997) CrossRef22.Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Jones, N.D., Leroy, X. (eds.) POPL 2004. pp. 232–244. ACM, New York (2004)23.Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Launchbury, J., Mitchell, J.C. (eds.) POPL 2002. pp. 58–70. ACM, New York (2002)24.Jhala, R., Majumdar, R.: Path slicing. In: Sarkar, V., Hall, M.W. (eds.) PLDI 2005. pp. 38–47. ACM, New York (2005)25. Khoroshilov, A., Mutilin, V., Petrenko, A., Zakharov, V.: Establishing linux driver verification process. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 165–176. Springer, Heidelberg (2010) CrossRef26. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) CrossRef27.Rümmer, P., Subotic, P.: Exploring interpolants. In: FMCAD 2013. pp. 69–76. IEEE (2013)28.Sajaniemi, J.: An empirical analysis of roles of variables in novice-level procedural programs. In: HCC 2002. pp. 37–39. IEEE (2002)29.van Deursen, A., Moonen, L.: Understanding COBOL systems using inferred types. In: IWPC 1999. pp. 74–81. IEEE (1999) About this Chapter Title Refinement Selection Book Title Model Checking Software Book Subtitle 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings Pages pp 20-38 Copyright 2015 DOI 10.1007/978-3-319-23404-5_3 Print ISBN 978-3-319-23403-8 Online ISBN 978-3-319-23404-5 Series Title Lecture Notes in Computer Science Series Volume 9232 Series ISSN 0302-9743 Publisher Springer International Publishing Copyright Holder Springer International Publishing Switzerland Additional Links About this Book Topics Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Industry Sectors Pharma Automotive Biotechnology Electronics IT & Software Telecommunications Consumer Packaged Goods Aerospace Oil, Gas & Geosciences Engineering eBook Packages Computer Science Editors Bernd Fischer (13) Jaco Geldenhuys (14) Editor Affiliations 13. Stellenbosch University 14. Stellenbosch University Authors Dirk Beyer (15) Stefan Löwe (15) Philipp Wendler (15) Author Affiliations 15. University of Passau, Passau, Germany Continue reading... To view the rest of this content please follow the download PDF link above.

© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号

地址：北京市海淀区学院路29号 邮编：100083

电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700