αCheck: A mechanized metatheory model checker

DOI10.1017/S1471068417000035zbMATH Open1379.68236arXiv1704.00617MaRDI QIDQ4593089FDOQ4593089

Authors: James Cheney, Alberto Momigliano 

Publication date: 9 November 2017

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1704.00617

Recommendations

• A formalization and proof checker for Isabelle's metalogic
• A proof theory for model checking: an extended abstract
• MCMT: a model checker modulo theories
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Model checking in the modal \(\mu \)-calculus and generic solutions
• Model Checking: From Tools to Theory
• Machine-checked proof-theory for propositional modal logics
• scientific article; zbMATH DE number 1905120
• Isabelle's metalogic: formalization and proof checker

zbMATH Keywords

model checkingnominal logiccounterexample searchnegation elimination

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• Automatic proof and disproof in Isabelle/HOL
• The Twelf Proof Assistant
• Ott: Effective tool support for the working semanticist
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Foundational property-based testing
• Theorem Proving in Higher Order Logics
• Binders unbound
• An overview of the K semantic framework
• Nominal sets. Names and symmetry in computer science
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax
• Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
• A new approach to abstract syntax with variable binding
• Nominal unification
• A two-level logic approach to reasoning about computations
• Concrete semantics. With Isabelle/HOL
• General bindings and alpha-equivalence in Nominal Isabelle
• Verifying termination and reduction properties about higher-order logic programs
• Title not available (Why is that?)
• Negation and constraint logic programming
• Tests and proofs. 10th international conference, TAP 2016, held as part of STAF 2016, Vienna, Austria, July 5--7, 2016. Proceedings
• Logic programming and negation: A survey
• A transformational approach to negation in logic programming
• Title not available (Why is that?)
• Types and programing languages
• About permutation algebras, (pre)sheaves and named sets
• Uniform proofs as a foundation for logic programming
• An efficient nominal unification algorithm
• A polynomial nominal unification algorithm
• Functional and logic programming. 12th international symposium, FLOPS 2014, Kanazawa, Japan, June 4--6, 2014. Proceedings
• Title not available (Why is that?)
• Semantics engineering with PLT Redex
• Explicit representation of terms defined by counter examples
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus
• Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming
• Completeness and Herbrand theorems for nominal logic
• Equivariant unification
• A simple sequent calculus for nominal logic
• Causal commutative arrows and their optimization
• Constraint Logic Programming with Hereditary Harrop formulas
• Orienting rewrite rules with the Knuth-Bendix order.
• Answer Set Programming: A Declarative Approach to Solving Search Problems
• Title not available (Why is that?)
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• Nominal narrowing
• On equivalence and canonical forms in the LF type theory
• Static typing for a faulty lambda calculus
• Modelling generic judgements
• Mechanizing the metatheory of LF
• Higher-order pattern complement and the strict \(\lambda\)-calculus
• Smart testing of functional programs in Isabelle
• Success and failure for hereditary Harrop formulae
• Functional and Logic Programming
• Title not available (Why is that?)
• Scrap your nameplate (functional pearl)

Cited In (5)

• Nominal unification with letrec and environment-variables
• On nominal syntax and permutation fixed points
• A case study in programming coinductive proofs: Howe's method
• POPLMark reloaded: mechanizing proofs by logical relations
• Towards substructural property-based testing

Uses Software

• Nitpick
• Ott
• Twelf
• Sledgehammer
• Bedwyr
• SmallCheck
• K tool
• PLT Redex
• PoplMark
• Nominal Isabelle
• PrologCheck
• K Prover

This page was built for publication: αCheck: A mechanized metatheory model checker

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4593089)