14 November 2016: James Cheney Mechanized metatheory model-checking using alphaCheck Mechanized metatheory means formalizing and validating properties of languages (e.g. programming languages, logics, or other calculi). Theorem proving systems (Coq, Isabelle, Agda) have been used extensively for such formalization, but this is labor-intensive: even for well-understood paper proofs, performing a complete formalization is challenging. Complete formalization may not be worth the effort during the development of a system, when key definitions are still in flux and may not yet be correct. We advocate a complementary technique based on (bounded) model-checking: given a specification of a language as a logic program in alphaProlog [1], we search for counterexamples to key properties exhaustively up to some depth-bound. Searching for counterexamples does not guarantee the validity of the properties, but (we argue) does provide increased confidence ("sanity checking"), and can be automated, making it a plausible alternative to interactive theorem proving during the development of new systems. I'll present some of the underlying ideas [2] and recent optimizations [3] and demonstrate the system, with the aim of convincing some of you to try it out and see if it is helpful for your research. [1] https://github.com/aprolog-lang/aprolog/ [2] Mechanized Metatheory Model-Checking, James Cheney and Alberto Momigliano, PPDP 2007, p. 75-86. http://dx.doi.org/10.1145/1273920.1273931 [3] Advances in Property-Based Testing for alpha-Prolog, James Cheney, Alberto Momigliano and Matteo Pessina, TAP 2016, p. 37-56. http://dx.doi.org/10.1007/978-3-319-41135-4_3 http://arxiv.org/abs/1604.08345 Nov 14 2016 14.00 - 14.30 14 November 2016: James Cheney Mechanized metatheory model-checking using alphaCheck IF 4.31/4.33
14 November 2016: James Cheney Mechanized metatheory model-checking using alphaCheck Mechanized metatheory means formalizing and validating properties of languages (e.g. programming languages, logics, or other calculi). Theorem proving systems (Coq, Isabelle, Agda) have been used extensively for such formalization, but this is labor-intensive: even for well-understood paper proofs, performing a complete formalization is challenging. Complete formalization may not be worth the effort during the development of a system, when key definitions are still in flux and may not yet be correct. We advocate a complementary technique based on (bounded) model-checking: given a specification of a language as a logic program in alphaProlog [1], we search for counterexamples to key properties exhaustively up to some depth-bound. Searching for counterexamples does not guarantee the validity of the properties, but (we argue) does provide increased confidence ("sanity checking"), and can be automated, making it a plausible alternative to interactive theorem proving during the development of new systems. I'll present some of the underlying ideas [2] and recent optimizations [3] and demonstrate the system, with the aim of convincing some of you to try it out and see if it is helpful for your research. [1] https://github.com/aprolog-lang/aprolog/ [2] Mechanized Metatheory Model-Checking, James Cheney and Alberto Momigliano, PPDP 2007, p. 75-86. http://dx.doi.org/10.1145/1273920.1273931 [3] Advances in Property-Based Testing for alpha-Prolog, James Cheney, Alberto Momigliano and Matteo Pessina, TAP 2016, p. 37-56. http://dx.doi.org/10.1007/978-3-319-41135-4_3 http://arxiv.org/abs/1604.08345 Nov 14 2016 14.00 - 14.30 14 November 2016: James Cheney Mechanized metatheory model-checking using alphaCheck IF 4.31/4.33
Nov 14 2016 14.00 - 14.30 14 November 2016: James Cheney Mechanized metatheory model-checking using alphaCheck
