Automatic C program verification based on mixed axiomatic semantics

Gamma, E., Helm, R., Johnson, R., and Vlissides, J., Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley, 1994.

Kondratyev, D.A. and Promsky, A.V., Complex approach to error localization at C-program verification, Sist. Inform., 2013, no. 1, pp. 79–96.

Nepomnyaschy, V.A., Anureev, I.S., Mikhaylov, I.N., and Promsky, A.V., C-light language oriented on verification, in Sistemnaya informatika: Sbornik nauchnykh trudov. Vyp. 9: Formalnye metody i modeli informatiki (System Informatics: Coll. Sci. Papers. Part. 9. Formal Methods and Models of Informatics), Novosibirsk: Sibir. Otd. Ross. Akad. Nauk, 2004, pp. 51–134.

Anureev, I.S., Maryasov, I.V., and Nepomniaschy, V.A., C-programs verification based on mixed axiomatic semantics, Autom. Control Compt. Sci., 2011, vol. 45, pp. 485–500.

Anureev, I., Maryasov, I., and Nepomniaschy, V., Revised mixed axiomatic semantics method of C program verification, Proc. 3rd Workshop “PSSV: Theory and Applications” Nizhni Novgorod, 2012, pp. 16–23.

Baudin, P., Cuoq, P., Filliatre, J.-C., Marché, C., Monate, B., Moy, Y., and Prevosto, V., ACSL: ANSI/ISO C Specification Language. http://frama-c.com/download/acsl-1.4.pdf

Bormer, T., Brockschmidt, M., Distefano, D., Ernst, G., Filliatre, J.-C., Grigore, R., Huisman, M., Klebanov, V., Marché, C., Monahan, R., Mostowski, W., Polikarpova, N., Scheben, C., Schellhorn, G., Tofan, B., Tschannen, J., and Ulbrich, M., The COST IC0701 verification competition 2011, Revised Selected Papers of Int. Conf. FoVeOOS, Lect. Notes Compt. Sci., 2011, vol. 7421, pp. 3–21.

Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., and Tobies, S., VCC: A practical system for verifying voncurrent C, Proc. 22nd Int. Conf. TPHOLs. Lect. Notes Compt. Sci., 2009, vol. 5674, pp. 23–42.

Detlefs, D., Nelson, G., and Saxe, J.B., Simplify: A Theorem Prover for Program Checking. HP Tech. Rep. HPL-2003-148, Palo Alto, 2003. http://www.hpl.hp.com/techreports/2003/HPL-2003-148.pdf

Filliatre, J.-C. and Marché, C., Multi-prover verification of C programs, Proc. of 6th ICFEM, Lect. Notes Compt. Sci., 2004, vol. 3308, pp. 15–29.

Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., and Wei, B., The 1st verified software competition: Experience report, Proc. 17th Int. Symp. on Formal Methods. Lect. Notes Compt. Sci., 2011, vol. 6664, pp. 154–168.

Leino, K.R.M., Dafny: an automatic program verifier for functional correctness, Revised Selected Papers of 16th Int. Conf. LPAR-16, Lect. Notes Compt. Sci., 2010, vol. 6355, pp. 348–370.

Maryasov, I.V., Nepomniaschy, V.A., Promsky, A.V., and Kondratyev, D.A., Automatic C program verification based on mixed axiomatic semantics, Proc. of 4th Workshop “PSSV: Theory and Applications”, Ekaterinburg, 2013, pp. 50–59.

Moura, L. de and Bjørner, N., Z3: An efficient SMT solver, Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2008), Lect. Notes Compt. Sci., 2008, vol. 4963, pp. 337–340.

Nepomniaschy, V.A., Anureev, I.S., Atuchin, M.M., Maryasov, I.V., Petrov, A.A., and Promsky, A.V., C program verification in SPECTRUM multilanguage system, Autom. Control Compt. Sci., 2011, vol. 45, pp. 413–420.

Promsky, A.V., A Formal Approach to the Error Localization, Preprint Sib. Branch Inst. Inform. System Russ. Acad. Sci., Novosibirsk, 2012, No. 169.