×

\(\alpha\mathrm{Check}\): a mechanized metatheory model checker. (English) Zbl 1379.68236

Summary: The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem of searching for errors in such formalizations has attracted comparatively little attention. In this article, we present \(\alpha\)Check, a bounded model checker for metatheoretic properties of formal systems specified using nominal logic. In contrast to the current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the case that a flaw is detected. We present two implementations of this technique, one based on negation-as-failure and one based on negation elimination, along with experimental results showing that these techniques are fast enough to be used interactively to debug systems as they are developed.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] AmaralC., FloridoM. and Santos CostaV.2014. PrologCheck: Property-based testing in Prolog. In Functional and Logic Programming, vol. 8475, M.Codish and E.Sumii, Eds. Lecture Notes in Computer Science, Springer International Publishing, 1-17.10.1007/978-3-319-07151-0 · Zbl 1291.68015 · doi:10.1007/978-3-319-07151-0
[2] AptK. R. and BolR. N.1994. Logic programming and negation: A survey. The Journal of Logic Programming19, 9-71. · Zbl 0942.68518
[3] Ayala-RincónM., FernándezM. and Nantes-SobrinhoD.2016. Nominal narrowing. In Proc. of 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 11:1-11:17. · Zbl 1387.68142
[4] AydemirB. E., BohannonA., FairbairnM., FosterJ. N., PierceB. C., SewellP., VytiniotisD., WashburnG., WeirichS. and ZdancewicS.2005. Mechanized metatheory for the masses: The PoplMark Challenge. In TPHOLs, vol. 3603, J.Hurd and T. F.Melham, Eds. Lecture Notes in Computer Science, Springer, 50-65. · Zbl 1152.68516
[5] BaeldeD., GacekA., MillerD., NadathurG. and TiuA.2007. The Bedwyr system for model checking over syntactic expressions. In CADE, vol. 4603, F.Pfenning, Ed. Lecture Notes in Computer Science, Springer, 391-397.
[6] BarbutiR., MancarellaP., PedreschiD. and TuriniF.1990. A transformational approach to negation in logic programming. Journal of Logic Programming8, 201-228.10.1016/0743-1066(90)90023-X · Zbl 0796.68056 · doi:10.1016/0743-1066(90)90023-X
[7] BlanchetteJ. C., BulwahnL. and NipkowT.2011. Automatic proof and disproof in Isabelle/HOL. In FroCoS, vol. 6989, C.Tinelli and V.Sofronie-Stokkermans, Eds. Lecture Notes in Computer Science, Springer, 12-27.
[8] BlanchetteJ. C. and NipkowT.2010. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In ITP 2010, vol. 6172, M.Kaufmann and L.Paulson, Eds. LNCS, Springer, 131-146. · Zbl 1291.68326
[9] BojańczykM., KlinB., KurzA. and PittsA. M.2013. Nominal computation theory (Dagstuhl Seminar 13422). Dagstuhl Reports3, 10, 58-71.
[10] BruscoliP., LeviF., LeviG. and MeoM. C.1994. Compilative constructive negation in constraint logic programs. In Proc. Trees in Algebra and Programming - CAAP’94, 19th International Colloquium, S.Tison, Ed. Lecture Notes in Computer Science, Springer, vol. 787. 52-76.
[11] BulwahnL.2012a. The new Quickcheck for Isabelle - random, exhaustive and symbolic testing under one roof. In CPP, vol. 7679, C.Hawblitzel and D.Miller, Eds. Lecture Notes in Computer Science, Springer, 92-108. · Zbl 1383.68071
[12] BulwahnL.2012b. Smart testing of functional programs in Isabelle. In LPAR, vol. 7180, N.Bjørner and A.Voronkov, Eds. Lecture Notes in Computer Science, Springer, 153-167. · Zbl 1352.68039
[13] CalvèsC. and FernándezM.2008. A polynomial nominal unification algorithm. Theoretical Computer Science403, 2-3, 285-306.10.1016/j.tcs.2008.05.012 · Zbl 1154.68108 · doi:10.1016/j.tcs.2008.05.012
[14] CheneyJ.2005a. Relating nominal and higher-order pattern unification. In Proc. of the 19th International Workshop on Unification (UNIF 2005), L.Vigneron, Ed., LORIA Research Report A05-R-022, 104-119.
[15] CheneyJ.2005b. Scrap your nameplate (functional pearl). In Proc. of the 10th International Conference on Functional Programming (ICFP 2005), B.Pierce, Ed. ACM, Tallinn, Estonia, 180-191. · Zbl 1302.68056
[16] CheneyJ.2006. Completeness and Herbrand theorems for nominal logic. Journal of Symbolic Logic71, 1, 299-320.10.2178/jsl/1140641176 · Zbl 1100.03016 · doi:10.2178/jsl/1140641176
[17] CheneyJ.2010. Equivariant unification. Journal of Automated Reasoning45, 3, 267-300.10.1007/s10817-009-9164-3 · Zbl 1207.68368 · doi:10.1007/s10817-009-9164-3
[18] CheneyJ.2016. A simple sequent calculus for nominal logic. Journal of Logic and Computation26, 2, 699-726.10.1093/logcom/exu024 · Zbl 1403.03049 · doi:10.1093/logcom/exu024
[19] CheneyJ. and MomiglianoA.2007. Mechanized metatheory model-checking. In PPDP, M.Leuschel and A.Podelski, Eds. ACM, 75-86.10.1145/1273920 · doi:10.1145/1273920
[20] CheneyJ., MomiglianoA. and PessinaM.2016. Advances in property-based testing for αProlog. In Proc. of the 10th International Conference on Tests and Proofs (TAP 2016), B. K.Aichernig and C. A.Furia, Eds. Lecture Notes in Computer Science, vol. 9762. Springer, Vienna, Austria, 37-56.
[21] CheneyJ. and UrbanC.2008. Nominal logic programming. ACM Transactions on Programming Languages and Systems30, 5, 26.
[22] ClaessenK. and HughesJ.2000. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proc. of the 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP 2000). ACM, Montreal, Canada, 268-279.
[23] ClarkeE. M., GrumbergO. and PeledD. A.2000. Model Checking. MIT Press.
[24] DybjerP., HaiyanQ. and TakeyamaM.2004. Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Information & Software Technology46, 15, 1011-1025.10.1016/j.infsof.2004.07.002 · doi:10.1016/j.infsof.2004.07.002
[25] FelleisenM., FindlerR. B. and FlattM.2009. Semantics Engineering with PLT Redex. The MIT Press.
[26] FernándezM. and GabbayM.2005. Nominal rewriting with name generation: Abstraction versus locality. In PPDP, P.Barahona and A. P.Felty, Eds. ACM, 47-58.
[27] FetscherB., ClaessenK., PalkaM. H., HughesJ. and FindlerR. B.2015. Making random judgments: Automatically generating well-typed terms from the definition of a type-system. In Proc. of ESOP 2015, vol. 9032, J.Vitek, Ed. Lecture Notes in Computer Science, Springer, 383-405.
[28] FindlerR. B., KleinC. and FetscherB.2015. Redex: Practical semantics engineering. URL: http://docs.racket-lang.org/redex. [Accessed on 25/04/2017]
[29] GabbayM.2007. Fresh logic: Proof-theory and semantics for FM and nominal techniques. Journal of Applied Logic5, 2, 356-387.10.1016/j.jal.2005.10.012 · Zbl 1124.03010 · doi:10.1016/j.jal.2005.10.012
[30] GabbayM. J.2011. Foundations of nominal techniques: Logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic17, 2, 161-229.10.2178/bsl/1305810911S1079898600000536 · Zbl 1253.03059 · doi:10.2178/bsl/1305810911
[31] GabbayM. J. and CheneyJ.2004. A sequent calculus for nominal logic. In Proc. of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004). IEEE Computer Society, Turku, Finland, 139-148.
[32] GabbayM. J. and PittsA. M.2002. A new approach to abstract syntax with variable binding. Formal Aspects of Computing13, 341-363.10.1007/s001650200016 · Zbl 1001.68083 · doi:10.1007/s001650200016
[33] GacekA.2010. Relating nominal and higher-order abstract syntax specifications. In PPDP, T.Kutsia, W.Schreiner, and M.Fernández, Eds. ACM, 177-186.
[34] GacekA., MillerD. and NadathurG.2012. A two-level logic approach to reasoning about computations. Journal of Automated Reasoning49, 2, 241-273.10.1007/s10817-011-9218-1 · Zbl 1290.68088 · doi:10.1007/s10817-011-9218-1
[35] GadducciF., MiculanM. and MontanariU.2006. About permutation algebras, (pre)sheaves and named sets. Higher-Order and Symbolic Computation19, 2-3, 283-304.10.1007/s10990-006-8749-3 · Zbl 1105.68083 · doi:10.1007/s10990-006-8749-3
[36] HarlandJ.1993. Success and failure for hereditary Harrop formulae. Journal of Logic Programming17, 1, 1-29.10.1016/0743-1066(93)90007-4 · Zbl 0781.68037 · doi:10.1016/0743-1066(93)90007-4
[37] HarperR. and PfenningF.2005. On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic6, 1, 61-101.10.1145/1042038.1042041 · Zbl 1367.03055 · doi:10.1145/1042038.1042041
[38] HeathQ. and MillerD.2015. A framework for proof certificates in finite state exploration. In Proc. 4th Workshop on Proof eXchange for Theorem Proving, PxTP 2015, C.Kaliszyk and A.Paskevich, Eds. EPTCS, vol. 186. 11-26. Open Publishing Association, Berlin, Germany.
[39] KleinC., ClementsJ., DimoulasC., EastlundC., FelleisenM., FlattM., McCarthyJ. A., RafkindJ., Tobin-HochstadtS. and FindlerR. B.2012a. Run your research: On the effectiveness of lightweight mechanization. In Proc. of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’12. ACM, New York, NY, USA, 285-296.
[40] KleinC., FlattM. and FindlerR. B.2012b. The Racket virtual machine and randomized testing. Higher-Order and Symbolic Computation25, 2-4, 209-253.10.1007/s10990-013-9091-1 · doi:10.1007/s10990-013-9091-1
[41] LakinM. R. and PittsA. M.2009. Resolving inductive definitions with binders in higher-order typed functional programming. In Proc. the 18th European Symposium on Programming (ESOP 2009), Springer, York, UK, 47-61.
[42] LassezJ.-L. and MarriottK.1987. Explicit representation of terms defined by counter examples. Journal of Automated Reasoning3, 3, 301-318. · Zbl 0641.68124
[43] LeachJ., NievaS. and Rodríguez-ArtalejoM.2001. Constraint logic programming with hereditary Harrop formulas. TPLP1, 4, 409-445. · Zbl 1091.68522
[44] LevyJ. and VillaretM.2010. An efficient nominal unification algorithm. In Proc. of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, Springer, Edinburgh, Scottland, UK, 209-226.
[45] LevyJ. and VillaretM.2012. Nominal unification from a higher-order perspective. ACM Transactions on Computational Logic13, 2, 10:1-10:31. · Zbl 1352.03017
[46] LiuH., ChengE. and HudakP.2009. Causal commutative arrows and their optimization. SIGPLAN Notices44, 9, 35-46. · Zbl 1302.68064
[47] MancarellaP. and PedreschiD.1988. An algebra of logic programs. In Proc. of the 5th International Conference and Symposium on Logic Programming, R. A.Kowalski and K. A.Bowen, Eds. ALP, IEEE, The MIT Press, Seatle, 1006-1023.
[48] MillerD., NadathurG., PfenningF. and ScedrovA.1991. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic51, 125-157.10.1016/0168-0072(91)90068-W · Zbl 0721.03037 · doi:10.1016/0168-0072(91)90068-W
[49] MomiglianoA.2000. Elimination of negation in a logical framework. In CSL, vol. 1862, P.Clote and H.Schwichtenberg, Eds. Lecture Notes in Computer Science, Springer, 411-426. · Zbl 0973.68039
[50] MomiglianoA.2012. A supposedly fun thing I may have to do again: A HOAS encoding of Howe’s method. In Proc. of the 7th International Workshop on Logical Frameworks and Meta-languages, Theory and Practice. LFMTP ’12. ACM, New York, NY, USA, 33-42.
[51] MomiglianoA. and PfenningF.2003. Higher-order pattern complement and the strict lambda-calculus. ACM Transactions on Computational Logic4, 4, 493-529.10.1145/937555.937559 · Zbl 1365.68155 · doi:10.1145/937555.937559
[52] MontanariU. and PistoreM.2005. History-dependent automata: An introduction. In Advanced Lectures of the 5th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-Moby 2005), M.Bernardo and A.Bogliolo, Ed., vol. 3465 of LNCS, Springer, 1-28.
[53] Moreno-NavarroJ. J. and Muñoz-HernándezS.2000. How to incorporate negation in a Prolog compiler. In PADL 2000, vol. 1753, E.Pontelli and V. S.Costa, Eds. LNCS, Springer, 124-140.
[54] Muñoz-HernándezS., MariñoJ. and Moreno-NavarroJ. J.2004. Constructive intensional negation. In FLOPS, vol. 2998, Y.Kameyama and P. J.Stuckey, Eds. Lecture Notes in Computer Science, Springer, 39-54. · Zbl 1122.68382
[55] NaishL.1997. A declarative debugging scheme. Journal of Functional and Logic Programming1997, 3, 3-29. · Zbl 0924.68125
[56] NiemeläI.2006. Answer set programming: A declarative approach to solving search problems. In JELIA, vol. 4160, M.Fisher, W.van der Hoek, B.Konev, and A.Lisitsa, Eds. Lecture Notes in Computer Science, Springer, 15-18. · Zbl 1152.68415
[57] NipkowT. and KleinG.2014. Concrete Semantics - With Isabelle/HOL. Springer.
[58] OwreS.2006. Random testing in PVS. In Workshop on Automated Formal Methods (AFM). Informatl proceedings, available at http://fm.csl.sri.com/AFM06/ [Accessed on 25/04/2017].
[59] ParaskevopoulouZ., HritcuC., DénèsM., LampropoulosL. and PierceB. C.2015. Foundational property-based testing. In Proc. of the 6th International Conference on Interactive Theorem Proving (ITP 2015), vol. 9236, C.Urban and X.Zhang, Eds. Lecture Notes in Computer Science, Springer, 325-343.
[60] PientkaB.2005. Verifying termination and reduction properties about higher-order logic programs. Journal of Automated Reasoning34, 2, 179-207.10.1007/s10817-005-6534-3 · Zbl 1102.68648 · doi:10.1007/s10817-005-6534-3
[61] PierceB. C.2002. Types and Programming Languages. MIT Press.
[62] PierceB. C., de AmorimA. A., CasinghinoC., GaboardiM., GreenbergM., HriţcuC., SjöbergV. and YorgeyB.2016. Software Foundations. Electronic textbook. Version 4.0. URL: http://www.cis.upenn.edu/ bcpierce/sf. [Accessed on 25/04/2017]
[63] PittsA.2016. Nominal techniques. ACM SIGLOG News3, 1, 57-72.
[64] PittsA. M.2003. Nominal logic, a first order theory of names and binding. Information and Computation183, 165-193.10.1016/S0890-5401(03)00021-X · Zbl 1054.68079 · doi:10.1016/S0890-5401(03)00021-X
[65] PittsA. M.2013. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press. · Zbl 1297.68008
[66] RamakrishnanC. R., RamakrishnanI. V., SmolkaS. A., DongY., DuX., RoychoudhuryA. and VenkatakrishnanV. N.2000. XMC: A logic-programming-based verification toolset. In CAV 2000. Springer-Verlag, London, UK, 576-580. · Zbl 0974.68571
[67] RobersonM., HarriesM., DargaP. T. and BoyapatiC.2008. Efficient software model checking of soundness of type systems. In OOPSLA, G. E.Harris, Ed. ACM, 493-504.
[68] RoşuG. and ŞerbănuţăT. F.2010. An overview of the K semantic framework. Journal of Logic and Algebraic Programming79, 6, 397-434.10.1016/j.jlap.2010.03.012 · Zbl 1214.68188 · doi:10.1016/j.jlap.2010.03.012
[69] RuncimanC., NaylorM. and LindbladF.2008. Smallcheck and lazy SmallCheck: Automatic exhaustive testing for small values. In Haskell Workshop, A.Gill, Ed. ACM, 37-48.10.1145/1411286 · doi:10.1145/1411286
[70] SchöppU.2007. Modelling generic judgements. Electronic Notes in Theoretical Computer Science174, 5, 19-35. · Zbl 1278.03065
[71] Schroeder-HeisterP.1993. Definitional reflection and the completion. In Proc. of the 4th International Workshop on Extensions of Logic Programming (ELP’93), R.Dyckhoff, Ed. Lecture Notes in Computer Science, vol. 798. Springer, St. Andrews, UK, 333-347.
[72] SchürmannC.2009. The Twelf proof assistant. In TPHOLs, vol. 5674, S.Berghofer, T.Nipkow, C.Urban, and M.Wenzel, Eds. Lecture Notes in Computer Science, Springer, 79-83. · Zbl 1252.68263
[73] SewellP., NardelliF. Z., OwensS., PeskineG., RidgeT., SarkarS. and StrnisaR.2010. Ott: Effective tool support for the working semanticist. Journal of Functional Programming20, 1, 71-122.10.1017/S0956796809990293S0956796809990293 · Zbl 1185.68201 · doi:10.1017/S0956796809990293
[74] StuckeyP. J.1995. Negation and constraint logic programming. Information and Computation118, 1, 12-33.10.1006/inco.1995.1048 · Zbl 0827.68022 · doi:10.1006/inco.1995.1048
[75] TiuA. and MillerD.2010. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Transactions on Computers Logic11, 2 (January), 13:1-13:35. · Zbl 1351.68186
[76] UrbanC., CheneyJ. and BerghoferS.2011. Mechanizing the metatheory of LF. ACM Transactions on Computational Logic12, 2, Article 15. · Zbl 1351.68250
[77] UrbanC. and KaliszykC.2012. General bindings and alpha-equivalence in Nominal Isabelle. Logical Methods in Computer Science8, 2, 1-35. · Zbl 1242.68283
[78] UrbanC., PittsA. M. and GabbayM. J.2004. Nominal unification. Theoretical Computer Science323, 1-3, 473-497.10.1016/j.tcs.2004.06.016 · Zbl 1078.68140 · doi:10.1016/j.tcs.2004.06.016
[79] VolpanoD., IrvineC. and SmithG.1996. A sound type system for secure flow analysis. Journal of Computer Security4, 2-3, 167-187.10.3233/JCS-1996-42-304 · doi:10.3233/JCS-1996-42-304
[80] WalkerD., MackeyL., LigattiJ., ReisG. A. and AugustD. I.2006. Static typing for a faulty lambda calculus. In ICFP ’06: Proc. of the 11th ACM SIGPLAN International Conference on Functional Programming. ACM Press, New York, NY, USA, 38-49.
[81] WeirichS., YorgeyB. A. and SheardT.2011. Binders unbound. In Proc. of the 16th ACM SIGPLAN International Conference on Functional Programming. ICFP ’11. ACM, New York, NY, USA, 333-345.
[82] WinskelG.1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge, MA, USA. · Zbl 0919.68082
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.