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