[1] ALBARGHOUTHI A,GURFINKEL A,CHECHIK M.From under-approximations to over-approximations and back[A].Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)[C].Berlin:Springer,2012.157-172.
[2] BIERE A,CIMATTI A,CLARKE E M,et al.Bounded model checking[J].Advances in Computers,2003,58(11):117-148.
[3] FLANAGAN C,QADEER S.Predicate abstraction for software verification[A].ACM SIGPLAN Notices[C].NewYork:ACM.2002,37(1):191-202.
[4] RAJAMANI S K,GULAVANI B.Counterexample driven refinement for abstract interpretation[P].US Patent 7509534.2009-3-24.
[5] 魏欧,石玉峰,徐丙凤,等.软件模型检测中的抽象模型研究综述[J].计算机研究与发展,2015,52(7):1580-1603. WEI O,SHI Y,XU B,et al.Abstract modeling formalisms in software model checking[J].Journal of Computer Research and Development,2015,52(7):1580-1603.(in Chinese)
[6] SHVED P,MANDRYKIN M,MUTILIN V.Predicate analysis with BLAST 2.7[A].Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)[C].Berlin:Springer,2012.525-527.
[7] BALL T J,BOUNIMOVA E O,LEVIN V A,et al.Program analysis through predicate abstraction and refinement[P].US Patent 8402444.2013-3-19.
[8] FRIEDBERGER K.CPA-BAM:Block-abstraction memoization with value analysis and predicate analysis[A].Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016)[C].Berlin:Springer,2016.912-915.
[9] WONISCH D.Block abstraction memoization for CPAchecker[A].Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)[C].Berlin:Springer,2012.531-533.
[10] MCMILLAN K L.Interpolation:Proofs in the service of model checking[A].Handbook of Model-Checking[M].Berlin:Springer,2014.
[11] FEDYUKOVICH G,HYVARINEN A E J,SHARYGINA N.Interpolation-based model checking for efficient incremental analysis of software[A].Proceedings of IEEE 16th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS 2013)[C].IEEE,2013.8-9.
[12] VIZEL Y,GURFINKEL A,MALIK S.Fast interpolating BMC[A].Proceedings of International Conference on Computer Aided Verification (CAV 2015)[C].Cham:Springer,2015.641-657.
[13] BEYER D,LOWE S.Interpolation for value analysis[A].Proceedings of Software Engineering & Management[C].Bonn:Gesellschaft für Informatik,2015.73-74.
[14] 段钊,田聪,段振华.基于CEGAR的C程序空指针解引用检测[J].计算机研究与发展,2016,53(1):155-164. DUAN Z,TIAN C,DUAN Z.CEGARbased null-pointer dereference checking in C programs[J].Journal of Computer Research and Development,2016,53(1):155-164.(in Chinese)
[15] CIMATTI A,GRIGGIO A.Software model checking via IC3[A].Proceedings of International Conference on Computer Aided Verification (CAV 2012)[C].Berlin:Springer,2012.277-293.
[16] BEYER D,LOWE S.Explicit-state software model checking based on CEGAR and interpolation[A].Proceedings of International Conference on Fundamental Approaches to Software Engineering (FASE 2013)[C].Berlin:Springer,2013.146-162.
[17] Beyer D,Löwe S.Explicit-state software model checking based on CEGAR and interpolation[A].Proceedings of International Conference on Fundamental Approaches to Software Engineering (FASE 2013)[C].Berlin:Springer,2013.146-162.
[18] BEYER D,KEREMOGLU M E.CPAchecker:A tool for configurable software verification[A].Proceedings of International Conference on Computer Aided Verification (CAV 2011)[C].Berlin:Springer,2011.184-190. |