References
- Rice HG. Classes of recursively enumerable sets and their decision problems. Trans Am Math Soc. 1953;74(2):358–358. doi: 10.1090/S0002-9947-1953-0053041-6
- Miné A, Delmas D. Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software. International Conference on Embedded Software; Oct 4–9. Amsterdam: IEEE; 2015. p. 65–74.
- Nimmer JW, Ernst MD. Static verification of dynamically detected program invariants. Electron Notes Theor Comput Sci. 2001;55(2):255–276. doi: 10.1016/S1571-0661(04)00256-7
- Carr SA, Logozzo F, Payer M. Automatic contract insertion with CCBot. IEEE Trans Software Eng. 2017;PP(99): 1–1.
- Margoor A, Komondoor R. Two techniques to improve the precision of a demand-driven null-dereference verification approach. Sci Comput Program. 2015;98:645–679. doi: 10.1016/j.scico.2014.09.006
- Ma S, Jiao MY, Zhang SK, et al. Practical null pointer dereference detection via value-dependence analysis. IEEE International Symposium on Software Reliability Engineering Workshops; Oct 23–27. Ottawa: IEEE; 2016. p. 70–77.
- Manevich R, Sridharan M, Adams S, et al. PSE: explaining program failures via postmortem static analysis. ACM Sigsoft Twelfth International Symposium on Foundations of Software Engineering; Oct 31–Nov 5. Newport Beach (CA): ACM; 2004. Vol.29, p. 63–72.
- Buss MO. Summary-based pointer analysis framework for modular bug finding [PhD thesis]. Columbia University; 2008.
- Madhavan R, Komondoor R. Null dereference verification via over-approximated weakest pre-conditions analysis. Acm Sigplan Notices. 2011;46(10):1033–1052. doi: 10.1145/2076021.2048144
- Spoto F. Precise null-pointer analysis. Softw Sys Model. 2011;10(2):219–252. doi: 10.1007/s10270-009-0132-5
- Cousot P, Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages; Jan 14–16. Los Angeles (CA): ACM; 1977. p. 238–252.
- Dong Y. RSTVL: A sound abstract memory model for program static analysis. International Conference on Computational Intelligence and Communication Networks; 2015 May 16–17; Jeju Island: IEEE; 2016. p. 1358–1362.
- Dong Y. An approach for identifying detecting objects of null dereference. J Softw. 2014;9(11):2771–2777. doi: 10.4304/jsw.9.11.2771-2777
- Dong Y, Xing Y, Jin D, et al. An approach to fully recognizing addressable expression. International Conference on Quality Software. IEEE; 2013. Vol. 8137, p. 149–152.
- Hackett B, Rugina R. Region-based shape analysis with tracked locations. Acm Sigplan Notices. 2005;40(1):310–323. doi: 10.1145/1047659.1040331
- Xu Z, Kremenek T, Zhang J. A memory model for static analysis of C programs. Leveraging applications of formal methods, verification, and validation. Berlin: Springer; 2010. p. 535–548.
- Zhao Y, Wang Y, Gong Y, et al. STVL: Improve the precision of static defect detection with symbolic three-valued logic. 118th Asia-Pacific Software Engineering Conference; 2011 Dec 5–8; Vietnam: IEEE; 2012. p. 179–186.
- Dong YK, Hai JD, Zhan GY, et al. Static analysis of C programs via region-based memory model. J Softw. 2014;25(2):357–372.