SpringerLink
Log in

Verified Model Checking for Conjunctive Positive Logic

  • Original Research
  • Published:
SN Computer Science Aims and scope Submit manuscript

Abstract

We formalize, in the Dafny language and verifier, a proof system PS for deciding the model checking problem of the fragment of first-order logic, denoted \(\mathcal {FO}(\forall ,\exists ,\wedge )\), known as conjunctive positive logic (CPL). We mechanize the proofs of soundness and completeness of PS ensuring its correctness. Our formalization is representative of how various popular verification systems can be used to verify the correctness of rule-based formal systems on the basis of the least fixpoint semantics. Further, exploiting Dafny’s automatic code generation, from the completeness proof we achieve a mechanically verified prototype implementation of a proof search mechanism that is a model checker for CPL. The model checking problem of \(\mathcal {FO}(\forall ,\exists ,\wedge )\) is equivalent to the quantified constraint satisfaction problem (QCSP), and it is PSPACE-complete. The formalized proof system decides the general QCSP and it can be applied to arbitrary formulae of CPL.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Germany)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18

Similar content being viewed by others

Notes

  1. Microsoft Visual Studio project.

  2. From now on, we colorize Dafny keywords with different colors similar to Visual Studio code editor.

  3. For easy reading, in the Dafny code snippets, we show the usual mathematical symbols, instead of real Dafny notation. For example, we show \(\bullet \) for :: (such that), \(\cup \) for union instead of +, \(\subseteq \) for set inclusion instead of \({\mathtt <=}\), also for the logical symbols and quantifiers, for example && is shown as \(\wedge \) and forall as \(\forall \), etc.

  4. Executable code is not generated for proofs.

  5. In Dafny code, one-line comments start by // and are coloured in green.

  6. In snippets, commented assertions are (true) assertions that Dafny automatically infers, hence Dafny does not need them as hints. They are included in proofs mainly for human-readability. The user could check the validity of each assert by uncommenting it. They are also very useful for re-using or refactoring proofs.

  7. In order to help the user in the process of constructing proofs, Dafny allows to introduce assumed assertions P. This allows the user to check whether P is the condition that Dafny needs to complete the proof. Dafny considers non-verified any proof with an assume clause.

References

  1. Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen D, editor. Logics of programs. Berlin: Springer; 1982. p. 52–71. https://doi.org/10.1007/BFb0025774.

    Chapter  Google Scholar 

  2. Queille JP, Sifakis J. Specification and verification of concurrent systems in cesar. In: Dezani-Ciancaglini M, Montanari U, editors, International Symposium on Programming; 1982. Berlin: Springer, p. 337–351. https://doi.org/10.1007/3-540-11494-7_22.

  3. Stockmeyer LJ. The Complexity of Decision Problems in Automata Theory and Logic. Project MAC: MAC TR. Massachusetts Institute of Technology; 1974.

  4. Vardi MY. The complexity of relational query languages. STOC ’82. New York: Association for Computing Machinery; 1982. p. 137–46. https://doi.org/10.1145/800070.802186.

    Book  Google Scholar 

  5. Martin B. Dichotomies and duality in first-order model checking problems. CoRR. 2006. http://arxiv.org/abs/cs/0609022.

  6. Creignou N, Khanna S, Sudan M. Complexity classifications of Boolean constraint satisfaction problems, volume 7 of SIAM monographs on discrete mathematics and applications. Philadelphia: Society for Industrial and Applied Mathematics; 2001. https://doi.org/10.1137/1.9780898718546.

    Book  MATH  Google Scholar 

  7. Dechter R. Constraint processing. Burlington: Morgan Kaufmann Publishers Inc.; 2003. https://doi.org/10.1016/B978-1-55860-890-0.X5000-2.

    Book  MATH  Google Scholar 

  8. Chen H. A rendezvous of logic, complexity, and algebra. ACM Comput Surv. 2009;42(1):21–232. https://doi.org/10.1145/1592451.1592453.

    Article  Google Scholar 

  9. Schaefer TJ. The complexity of satisfiability problems. In: Proceedings of the Tenth Annual ACM Symposium on Theory of Computing, STOC ’78; 1978. New York: ACM, p. 216–226. https://doi.org/10.1145/800133.804350.

  10. Grohe M. The complexity of homomorphism and constraint satisfaction problems seen from the other side. J ACM. 2007;54:1–24.

    Article  MathSciNet  Google Scholar 

  11. Marx D. Tractable hypergraph properties for constraint satisfaction and conjunctive queries. J ACM. 2013;. https://doi.org/10.1145/2535926.

    Article  MathSciNet  MATH  Google Scholar 

  12. Martin B. First-order model checking problems parameterized by the model. In: Beckmann A, Dimitracopoulos C, Löwe B, editors. Logic and theory of algorithms. Berlin: Springer; 2008. p. 417–27. https://doi.org/10.1007/978-3-540-69407-6_45.

    Chapter  Google Scholar 

  13. Martin B. Quantified constraints in twenty seventeen. In: Krokhin A, Zivny S, editors. The constraint satisfaction problem: complexity and approximability, volume 7 of Dagstuhl follow-ups; 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, p. 327–346. https://doi.org/10.4230/DFU.Vol7.15301.327.

  14. Egly U, Eiter T, Tompits H, Woltran S. Solving advanced reasoning tasks using quantified boolean formulas. In: Kautz HA, Porter BW, editors. In: Proceedings of the 17th national conference on artificial intelligence and 12th conf. on innovative applications of artificial intelligence; 2000. AAAI Press/The MIT Press, p. 417–422. http://www.aaai.org/Library/AAAI/2000/aaai00-064.php.

  15. Rintanen J. Constructing conditional plans by a theorem-prover. J Artif Intell Res. 1999;10(1):323–52 http://dl.acm.org/citation.cfm?id=1622859.1622870.

  16. Buning HK, Karpiński M, Flogel A. Resolution for quantified Boolean formulas. Inf Comput. 1995;117(1):12–8. https://doi.org/10.1006/inco.1995.1025.

    Article  MathSciNet  MATH  Google Scholar 

  17. Cadoli M, Schaerf M, Giovanardi A, Giovanardi M. An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. J Autom Reason. 2002;28(2):101–42. https://doi.org/10.1023/A:1015019416843.

    Article  MathSciNet  MATH  Google Scholar 

  18. Giunchiglia E, Narizzano M, Tacchella A. Backjum** for quantified Boolean logic satisfiability. Artif Intell. 2003;145(1–2):99–120. https://doi.org/10.1016/S0004-3702(02)00373-9.

    Article  MathSciNet  MATH  Google Scholar 

  19. Williams R. Algorithms for quantified boolean formulas. In: Proceedings of the thirteenth annual ACM-SIAM symposium on discrete algorithms, SODA ’02; 2002. Society for Industrial and Applied Mathematics, p. 299–307. http://dl.acm.org/citation.cfm?id=545381.545421.

  20. Bordeaux L, Monfroy E. Beyond NP: arc-consistency for quantified constraints. In: Van Hentenryck P, editor. Principles and practice of constraint programming-CP. Berlin: Springer; 2002. p. 371–86. https://doi.org/10.1007/3-540-46135-3_25.

    Chapter  Google Scholar 

  21. Gent IP, Nightingale P, Rowley A, Stergiou K. Solving quantified constraint satisfaction problems. Artif Intell. 2008;172(6):738–71. https://doi.org/10.1016/j.artint.2007.11.003.

    Article  MathSciNet  MATH  Google Scholar 

  22. Mamoulis N, Stergiou K. Algorithms for quantified constraint satisfaction problems. In: Proceedings of CP’04, volume 3258 of LNCS, 2004. Springer, p. 752–756.

  23. Abuin A, Chen H, Hermo M, Lucio P. Towards the automatic verification of QCSP tractability results. In: Proceedings of the XVII Jornadas sobre Programación y Lenguajes (PROLE 2017). 2017. http://hdl.handle.net/11705/PROLE/2017/017.

  24. Chen H. Beyond Q-resolution and prenex form: a proof system for quantified constraint satisfaction. Logic Methods Comput Sci. 2014;. https://doi.org/10.2168/LMCS-10(4:14)2014.

    Article  MathSciNet  MATH  Google Scholar 

  25. Balabanov V, Jiang J-HR. Unified QBF certification and its applications. Formal Methods Syst Des. 2012;41(1):45–65. https://doi.org/10.1007/s10703-012-0152-6.

    Article  MATH  Google Scholar 

  26. Zhang L, Malik S. Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of the 2002 IEEE/ACM international conference on computer-aided design (ICCAD’02); 2002. p. 442–449. https://doi.org/10.1145/774572.774637.

  27. Van Gelder A. Contributions to the theory of practical quantified boolean formula solving. In: Milano M, editor. Principles and Practice of Constraint Programming-18th International Conference, CP 2012, Proceedings, volume 7514 of lecture notes in computer science, 2012. Springer, p. 647–663. https://doi.org/10.1007/978-3-642-33558-7_47.

  28. Balabanov V, Widl M, Jiang J-HR. QBF resolution systems and their proof complexities. In: Sinz C, Egly U, editors. Theory and applications of satisfiability testing-SAT 2014. Cham: Springer International Publishing; 2014. p. 154–69.

    Chapter  Google Scholar 

  29. Bove A, Dybjer P, Norell U. A brief overview of Agda—a functional language with dependent types. In: Proceedings of the 22nd international conference on theorem proving in higher order logics. TPHOLs’09; 2009. Springer, p. 73–78. https://doi.org/10.1007/978-3-642-03359-9_6.

  30. The Coq Development Team. The Coq proof assistant. https://coq.inria.fr.

  31. Nipkow T, Paulson LC, Wenzel M. Isabelle/HOL—a proof assistant for higher-order logic, volume 2283 of LNCS. Berlin: Springer; 2002.

    MATH  Google Scholar 

  32. Gordon M, Milner R, Wadsworth CP. Edinburgh LCF: a mechanised logic of computation, volume of 78 lecture notes in computer science. Berlin: Springer; 1979.

    Book  Google Scholar 

  33. Schulz S. System description: E 1.8. In: McMillan KL, Middeldorp A, Voronkov A, editors, Logic for programming, artificial intelligence, and reasoning-19th international conference, LPAR-19, Proceedings, volume 8312 of lecture notes in computer science; 2013. Springer, p. 735–743. https://doi.org/10.1007/978-3-642-45221-5_49.

  34. Weidenbach C, Dimova D, Fietzke A, Kumar R, Suda M, Wischnewski P. SPASS version 3.5. In: Schmidt RA, editor, Automated Deduction-CADE-22, 22nd International Conference on Automated Deduction, Proceedings, volume 5663 of lecture notes in computer science; 2009. Springer, p. 140–145. https://doi.org/10.1007/978-3-642-02959-2_10.

  35. Riazanov A, Voronkov A. The design and implementation of VAMPIRE. AI Commun. 2002;15(2–3):91–110 http://content.iospress.com/articles/ai-communications/aic259.

  36. de Moura L, Bjørner N. Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J, editors. Tools and algorithms for the construction and analysis of systems, 14th international conference, TACAS 2008, volume 4963 of lecture notes in computer science; 2008. Springer, p. 337–340.

  37. Blanchette JC. Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In: Mahboubi A, Myreen MO, editors. Proceedings of the 8th ACM SIGPLAN international conference on certified programs and proofs, CPP. ACM; 2019. p. 1–13. https://doi.org/10.1145/3293880.3294087

  38. Ringer T, Palmskog K, Sergey I, Gligoric M, Tatlock Z. QED at large: a survey of engineering of formally verified software. Found Trends Program Lang. 2019;5(2–3):102–281. https://doi.org/10.1561/2500000045.

    Article  Google Scholar 

  39. Blanchette JC, Fleury M, Weidenbach C. A verified SAT solver framework with learn, forget, restart, and incrementality. In: Proceedings of the twenty-sixth international joint conference on artificial intelligence, IJCAI-17; 2017. p. 4786–4790. https://doi.org/10.24963/ijcai.2017/667.

  40. Schlichtkrull A. Formalization of the resolution calculus for first-order logic. J Autom Reason. 2018;61(1–4):455–84. https://doi.org/10.1007/s10817-017-9447-z.

    Article  MathSciNet  MATH  Google Scholar 

  41. Esparza J, Lammich P, Neumann R, Nipkow T, Schimpf A, Smaus J-G. A fully verified executable LTL model checker. In: Sharygina N, Veith H, editors. Computer aided verification. Berlin: Springer; 2013. p. 463–78.

    Chapter  Google Scholar 

  42. Fleury M. Optimizing a verified SAT solver. In: Badger JM, Rozier KY, editors. NASA Formal Methods-11th International Symposium, NFM 2019, Proceedings, volume 11460 of lecture notes in computer science; 2019. Springer, p. 148–165. https://doi.org/10.1007/978-3-030-20652-9_10.

  43. Maric F. Formal verification of a modern SAT solver by shallow embedding into Isabelle/Hol. Theor. Comput. Sci. 2010;411(50):4333–56. https://doi.org/10.1016/j.tcs.2010.09.014.

    Article  MathSciNet  MATH  Google Scholar 

  44. Oe D, Stump A, Oliver C, Clancy K. versat: a verified modern SAT solver. In: Kuncak V, Rybalchenko A, editors. Verification, Model Checking, and Abstract Interpretation-13th International Conference, VMCAI 2012, Proceedings, volume 7148 of lecture notes in computer science; 2012. Springer, p. 363–378. https://doi.org/10.1007/978-3-642-27940-9_24.

  45. Schlichtkrull A, Blanchette JC, Traytel D. A verified prover based on ordered resolution. In: Proceedings of the 8th ACM SIGPLAN international conference on certified programs and proofs (CPP 2019); 2019. Association for Computing Machinery, p. 152–165. https://doi.org/10.1145/3293880.3294100.

  46. Kaufmann M, Manolios P, Moore JS. Computer-aided reasoning: an approach. Advance formal methods. Dordrecht: Kluwer Academic Publishers; 2000. https://doi.org/10.1007/978-1-4615-4449-4.

    Book  Google Scholar 

  47. Cohen E, Dahlweid M, Hillebrand M, Leinenbach D, Moskal M, Santen T, Schulte W, Tobies S. VCC: a practical system for verifying concurrent C. In: Berghofer S, Nipkow T, Urban C, Wenzel M, editors. Proceedings of theorem proving in higher order logics: 22nd international conference, TPHOLs, Munich, Germany, August 17-20; 2009. Springer, p. 23–42. https://doi.org/10.1007/978-3-642-03359-9_2.

  48. Swamy N, Chen J, Fournet C, Strub P-Y, Bhargavan K, Yang J. Secure distributed programming with value-dependent types. J Funct Programm. 2013;23(4):402–51. https://doi.org/10.1017/S0956796813000142.

    Article  MathSciNet  MATH  Google Scholar 

  49. Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F. VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru MG, Havelund K, Holzmann GJ, Joshi R, editors. NASA Formal Methods. Berlin: Springer; 2011. p. 41–55. https://doi.org/10.1007/978-3-642-20398-5_4.

    Chapter  Google Scholar 

  50. Filliâtre J-C, Paskevich A. Why3—where programs meet provers. In: Felleisen M, Gardner P, editors. Programming languages and systems—22nd European Symposium on Programming, ESOP 2013, volume 7792 of lecture notes in computer science; 2013. Springer, p. 125–128. https://doi.org/10.1007/978-3-642-37036-6_8.

  51. Rustan K, Leino M. Dafny: an automatic program verifier for functional correctness. In: Clarke EM, Voronkov A, editors. Logic for programming, artificial intelligence, and reasoning, volume 6355 of lecture notes in computer science. Berlin: Springer; 2010. p. 348–70.

    MATH  Google Scholar 

  52. Clochard M, Filliâtre J-C, Marché J-C, Paskevich A. Formalizing Semantics with an Automatic Program Verifier. Berlin: Springer International Publishing; 2014. p. 37–51. https://doi.org/10.1007/978-3-319-12154-3_3.

    Book  Google Scholar 

  53. Bobot F, Filliâtre J-C, Marché C, Paskevich A. Let’s verify this with Why3. Softw Tools Technol Transf (STTT). 2015;17(6):709–27. https://doi.org/10.1007/s10009-014-0314-5.

    Article  Google Scholar 

  54. Rustan K, Leino M. Well-founded functions and extreme predicates in Dafny: a tutorial. In: Konev B, Schulz S, Simon L, editors. IWIL-2015. 11th international workshop on the implementation of logics, volume 40 of EPiC series in computing; 2016. EasyChair, p. 52–66. https://doi.org/10.29007/v2m3.

  55. Tarski A. A lattice-theoretical fixpoint theorem and its applications. Pac J Math. 1955;5(2):285–309 https://projecteuclid.org:443/euclid.pjm/1103044538.

  56. Rustan K, Leino M, Polikarpova N. Verified calculations. In: Cohen E, Rybalchenko A, editors. Verified software: theories, tools, experiments—5th international conference, VSTTE 2013, revised selected papers, volume 8164 of lecture notes in computer science; 2014. Springer, p. 170–190. https://doi.org/10.1007/978-3-642-54108-7_9.

  57. Backhouse R, editor. The calculational method, volume 53 of information processing letters. New York: Elsevier; 1995. https://doi.org/10.1016/0020-0190(94)00212-H.

    Book  Google Scholar 

  58. Rustan K, Leino M. Compiling Hilbert’s epsilon operator. In: Fehnker A, McIver A, Sutcliffe G, Voronkov A, editors. LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning-Short Presentations, volume 35 of EPiC Series in Computing; 2015. EasyChair, p. 106–118. https://doi.org/10.29007/rkxm.

  59. Rustan K, Leino M. Dafny power user: iterating over a collection. manuscript krml 275; 2020. https://leino.science/papers/krml275.html.

  60. Rustan K, Leino M, Wüstholz V. The Dafny integrated development environment. In: Dubois C, Giannakopoulou D, Méry D, editors. Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, volume 149 of electronic proceedings in theoretical computer science; 2014. Open Publishing Association, p. 3–15. https://doi.org/10.4204/eptcs.149.2.

  61. Rustan K, Leino M, Matichuk D. Modular verification scopes via export sets and translucent exports. In: Principled software development-essays dedicated to arnd Poetzsch–Heffter on the Occasion of his 60th Birthday; 2018. p. 185–202. https://doi.org/10.1007/978-3-319-98047-8_12.

  62. Thiemann R, Sternagel C. Certification of termination proofs using CeTA. In: Berghofer S, Nipkow T, Urban C, Wenzel M, editors, Theorem proving in higher order logics, 22nd international conference, TPHOLs 2009, proceedings, volume 5674 of lecture notes in computer science; 2009. Springer, p. 452–468. https://doi.org/10.1007/978-3-642-03359-9_31.

  63. Lochbihler A, Bulwahn L. Animating the formalised semantics of a Java-Like language. In Marko C, van Eekelen JD, Geuvers H, Schmaltz J, Wiedijk F, editors. Interactive theorem proving-second international conference, ITP 2011, proceedings, volume 6898 of lecture notes in computer science; 2011. Springer, p. 216–232. https://doi.org/10.1007/978-3-642-22863-6_17.

Download references

Acknowledgements

We are greatly indebted to Rustan Leino for the time and effort he has kindly devoted to us. This work has been carried out thanks to his thoughtful and stimulating suggestions and his considerable research assistance. Our work did specially benefit from his in-person tutorial of the inductive-predicate features and his advice for how to formulate the definitions in Dafny. We would also like to thank Hubie Chen for his support during the early developments of this work. We are also very grateful to the anonymous reviewers for their many helpful comments and suggestions that led to substantial improvements in the presentation of the paper.

Funding

This research has been supported by the European Union (FEDER funds) under grant TIN2017-86727-C2-2-R, and by the University of the Basque Country under Project LoRea GIU18-182.

Author information

Authors and Affiliations

  1. Computer Languages and Systems, University of the Basque Country, San Sebastián, Spain

    Montserrat Hermo & Paqui Lucio

  2. Dependable Embedded Systems, Ikerlan Research Center, Mondragón, Spain

    Alex Abuin & Unai Diaz de Cerio

Authors
  1. Alex Abuin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Unai Diaz de Cerio
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Montserrat Hermo
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Paqui Lucio
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Paqui Lucio.

Ethics declarations

Conflict of interest

The authors declare that they have no conflict of interest.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Abuin, A., de Cerio, U.D., Hermo, M. et al. Verified Model Checking for Conjunctive Positive Logic. SN COMPUT. SCI. 2, 344 (2021). https://doi.org/10.1007/s42979-020-00417-3

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s42979-020-00417-3

Keywords

Search

Navigation