Télécharger

Texte intégral

• Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 39-55. Springer, Heidelberg (2012)
• Arlt, S., Schäf, M.: Joogie: Infeasible Code Detection for Java. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 767-773. Springer, Heidelberg (2012)
• Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. SIGSOFT Softw. Eng. Notes 31, 82-87 (2005)
• Bertolini, C., Schäf, M., Schweitzer, P.: Infeasible Code Detection. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 310-325. Springer, Heidelberg (2012)
• Christ, J., Hoenicke, J., Schäf, M.: Towards Bounded Infeasible Code Detection. CoRR, abs/1205.6527 (2012)
• de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg (2008)
• Dijkstra, E.W.: A discipline of programming / Edsger W. Dijkstra. Prentice-Hall, Englewood Cliffs (1976)
• Dillig, I., Dillig, T., Aiken, A.: Static error detection using semantic inconsistency inference. In: PLDI, pp. 435-445 (2007)
• Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 351-368. Springer, Heidelberg (2011)
• Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: a general approach to inferring errors in systems code. In: SOSP, pp. 57-72 (2001)
• Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. SIGPLAN Not., 234-245 (2002)
• Grigore, R., Charles, J., Fairmichael, F., Kiniry, J.: Strongest postcondition of unstructured programs. In: FTfJP, pp. 6:1-6:7 (2009)
• Hoenicke, J., Leino, K.R.M., Podelski, A., Schäf, M., Wies, T.: It's Doomed; We Can Prove It. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 338-353. Springer, Heidelberg (2009)
• Hoenicke, J., Leino, K.R.M., Podelski, A., Schäf, M., Wies, T.: Doomed Program Points. Formal Methods in System Design (2010)
• Hovemeyer, D., Pugh, W.: Finding bugs is easy. In: OOPSLA, pp. 132-136 (2004)
• Janota, M., Grigore, R., Moskal, M.: Reachability analysis for annotated code. In: SAVCBS, pp. 23-30 (2007)
• Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett., 281-288 (2005)
• Leino, K.R.M., Millstein, T., Saxe, J.B.: Generating error traces from verificationcondition counterexamples. Sci. Comput. Program, 209-226 (2005)
• Leino, K.R.M., Rümmer, P.: A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312-327. Springer, Heidelberg (2010)
• Rümmer, P.: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol. 5330, pp. 274-289. Springer, Heidelberg (2008)
• Tomb, A., Flanagan, C.: Detecting inconsistencies via universal reachability analysis. In: ISSTA, pp. 287-297 (2012)