Instrumenting a weakest precondition calculus for counterexample generation. (English) Zbl 1395.68097

Summary: A major issue in the activity of deductive program verification is to understand why automated provers fail to discharge a proof obligation. To help the user understand the problem and decide what needs to be fixed in the code or the specification, it is essential to provide means to investigate such a failure. We present our approach for the design and the implementation of counterexample generation, exhibiting values for the variables of the program where a given part of the specification fails to be validated. To produce a counterexample, we exploit the ability of SMT solvers to propose, when a proof of a formula is not found, a counter-model. Turning such a counter-model into a counterexample for the initial program is not trivial because of the many transformations leading from a particular piece of code and its specification to a set of proof goals given to external provers.


68N99 Theory of software
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] Dijkstra, E. W., A discipline of programming, Series in Automatic Computation, (1976), Prentice Hall Int. · Zbl 0368.68005
[2] Leino, K. R.M.; Wüstholz, V., The dafny integrated development environment, (Dubois, C.; Giannakopoulou, D.; Méry, D., Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014, Electronic Proceedings in Theoretical Computer Science, vol. 149, (2014)), 3-15
[3] Cok, D. R., Openjml: software verification for Java 7 using JML, openjdk, and eclipse, (Dubois, C.; Giannakopoulou, D.; Méry, D., Proceedings 1st Workshop on Formal Integrated Development Environment, EPTCS, vol. 149, (2014)), 79-92
[4] Bobot, F.; Filliâtre, J.-C.; Marché, C.; Paskevich, A., Let’s verify this with why3, Int. J. Softw. Tools Technol. Transf., 17, 6, 709-727, (2015), see also
[5] Bobot, F.; Conchon, S.; Contejean, E.; Iguernelala, M.; Lescuyer, S.; Mebsout, A., The alt-ergo automated theorem prover, (2008)
[6] Barrett, C.; Conway, C. L.; Deters, M.; Hadarean, L.; Jovanović, D.; King, T.; Reynolds, A.; Tinelli, C., Cvc4, (Proceedings of the 23rd International Conference on Computer Aided Verification, CAV’11, (2011), Springer-Verlag Berlin, Heidelberg), 171-177
[7] de Moura, L.; Bjørner, N., Z3, an efficient SMT solver, (TACAS, Lecture Notes in Computer Science, vol. 4963, (2008), Springer), 337-340
[8] Filliâtre, J.-C.; Paskevich, A., Why3 — where programs meet provers, (Felleisen, M.; Gardner, P., Proceedings of the 22nd European Symposium on Programming, Lecture Notes in Computer Science, vol. 7792, (2013), Springer), 125-128
[9] Filliâtre, J.-C.; Marché, C., The why/krakatoa/caduceus platform for deductive program verification, (Damm, W.; Hermanns, H., 19th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 4590, (2007), Springer Berlin, Germany), 173-177
[10] Kosmatov, N.; Marché, C.; Moy, Y.; Signoles, J., Static versus dynamic verification in why3, frama-C and SPARK 2014, (Margaria, T.; Steffen, B., 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA, Lecture Notes in Computer Science, vol. 9952, (2016), Springer Corfu, Greece), 461-478
[11] Bobot, F.; Filliâtre, J.-C.; Marché, C.; Paskevich, A., Why3: shepherd your herd of provers, (Boogie 2011: First International Workshop on Intermediate Verification Languages, Wrocław, Poland, (2011)), 53-64
[12] Barnett, M.; DeLine, R.; Jacobs, B.; Chang, B.-Y. E.; Leino, K. R.M., Boogie: a modular reusable verifier for object-oriented programs, (de Boer, F. S.; Bonsangue, M. M.; Graf, S.; de Roever, W.-P., Formal Methods for Components and Objects: 4th International Symposium, Lecture Notes in Computer Science, vol. 4111, (2005)), 364-387
[13] Hauzar, D.; Marché, C.; Moy, Y., Counterexamples from proof failures in SPARK, (Software Engineering and Formal Methods, (2016)), 215-233
[14] Flanagan, C.; Saxe, J. B., Avoiding exponential explosion: generating compact verification conditions, (Principles of Programming Languages, (2001), ACM), 193-205 · Zbl 1323.68372
[15] Leino, K. R.M., Efficient weakest preconditions, Inf. Process. Lett., 93, 6, 281-288, (2005) · Zbl 1173.68563
[16] Belo Lourenço, C.; Frade, M. J.; Sousa Pinto, J., Formalizing single-assignment program verification: an adaptation-complete approach, (Thiemann, P., 25th European Symposium on Programming, (2016), Springer), 41-67 · Zbl 1335.68044
[17] Barrett, C.; Stump, A.; Tinelli, C., The SMT-LIB standard: version 2.0, (Gupta, A.; Kroening, D., Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, England, (2010))
[18] Dross, C.; Conchon, S.; Kanig, J.; Paskevich, A., Adding decision procedures to SMT solvers using axioms with triggers, J. Autom. Reason., 56, 4, 387-457, (2016) · Zbl 1356.68187
[19] Barnes, J., Programming in ada 2012, (2014), Cambridge University Press
[20] McCormick, J. W.; Chapin, P. C., Building high integrity applications with SPARK, (2015), Cambridge University Press · Zbl 1328.68009
[21] Chapman, R.; Schanda, F., Are we there yet? 20 years of industrial theorem proving with SPARK, (Klein, G.; Gamboa, R., Interactive Theorem Proving - Proceedings of the 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Lecture Notes in Computer Science, vol. 8558, (2014), Springer), 17-26 · Zbl 06341471
[22] Schanda, F.; Brain, M., Using answer set programming in the development of verified software, (Technical Communications of the 28th Int. Conf. on Logic Programming, LIPIcs, vol. 17, (2012), Leibniz-Zentrum fuer Informatik), 72-85 · Zbl 1281.68083
[23] Alloy
[24] Groce, A.; Kroening, D.; Lerda, F., Understanding counterexamples with explain, (Alur, R.; Peled, D., CAV, Lecture Notes in Computer Science, vol. 3114, (2004), Springer), 453-456 · Zbl 1103.68620
[25] Blanchette, J. C.; Nipkow, T., Nitpick: a counterexample generator for higher-order logic based on a relational model finder, (Kaufmann, M.; Paulson, L. C., Interactive Theorem Proving, First International Conference, Lecture Notes in Computer Science, vol. 6172, (2010), Springer), 131-146 · Zbl 1291.68326
[26] Leino, K. R.M.; Millstein, T.; Saxe, J. B., Generating error traces from verification-condition counterexamples, Sci. Comput. Program., 55, 13, 209-226, (2005) · Zbl 1075.68018
[27] Cok, D. R., Improved usability and performance of SMT solvers for debugging specifications, Int. J. Softw. Tools Technol. Transf., 12, 6, 467-481, (2010)
[28] Le Goues, C.; Leino, K. R.M.; Moskal, M., The boogie verification debugger, (Barthe, G.; Pardo, A.; Schneider, G., Software Engineering and Formal Methods - 9th International Conference, SEFM, Lecture Notes in Computer Science, vol. 7041, (2011), Springer), 407-414
[29] Cohen, E.; Dahlweid, M.; Hillebrand, M.; Leinenbach, D.; Moskal, M.; Santen, T.; Schulte, W.; Tobies, S., VCC: a practical system for verifying concurrent C, (Theorem Proving in Higher Order Logics, TPHOLs, Lecture Notes in Computer Science, vol. 5674, (2009), Springer)
[30] Müller, P.; Ruskiewicz, J. N., Using debuggers to understand failed verification attempts, (Butler, M. J.; Schulte, W., 17th International Symposium on Formal Methods, Lecture Notes in Computer Science, vol. 6664, (2011), Springer), 73-87
[31] Jacobs, B.; Smans, J.; Philippaerts, P.; Vogels, F.; Penninckx, W.; Piessens, F., Verifast: a powerful, sound, predictable, fast verifier for C and Java, (Bobaru, M. G.; Havelund, K.; Holzmann, G. J.; Joshi, R., NASA Formal Methods, Lecture Notes in Computer Science, vol. 6617, (2011), Springer), 41-55
[32] Hentschel, M.; Hähnle, R.; Bubel, R., Deductive software verification — the key book, 383-413, (2016), Springer
[33] Christakis, M.; Leino, K. R.M.; Müller, P.; Wüstholz, V., Integrated environment for diagnosing verification errors, (22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’16, (2016), Springer), 424-441
[34] Petiot, G.; Kosmatov, N.; Botella, B.; Giorgetti, A.; Julliand, J., Your proof fails? testing helps to find the reason, (Tests and Proofs - 10th International Conference, Lecture Notes in Computer Science, vol. 9762, (2016), Springer), 130-150
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.