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)
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., 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)