A proof theory for model checking: an extended abstract

MaRDI QIDQ5014803zbMATH OpenFDO

Authors Quentin Heath, Dale Miller

Publication date 8 December 2021

Full work available at URL https://arxiv.org/abs/1701.04915, http://eptcs.web.cse.unsw.edu.au/paper.cgi?LINEARITY2016.1

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A proof theory for model checking
• scientific article; zbMATH DE number 1744956
• scientific article; zbMATH DE number 1499079
• scientific article; zbMATH DE number 5148400
• Tableau-based model checking in the propositional mu-calculus

Cites work

• A new constructive logic: classic logic
• A proof search specification of the -calculus
• A proof theory for generic judgments
• Cut elimination for a logic with induction and co-induction
• Cut-elimination for a logic with definitions and induction
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Petri nets, Horn programs, linear logic and vector games
• Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus
• The Beginning of Model Checking: A Personal Perspective
• Untersuchungen über das logische Schliessen. I

Cited in

(15)

• ProofWatch: watchlist guidance for large theories in E
• A generalized semantics of PROMELA for abstract model checking
• A proof theory for model checking
• Universal guards, relativization of quantifiers, and failure models in model checking modulo theories
• scientific article; zbMATH DE number 5148400 (Why is no real title available?)
• Machine Checking Proof Theory: An Application of Logic to Logic
• On the convergence of reduction-based and model-based methods in proof theory
• scientific article; zbMATH DE number 1088222 (Why is no real title available?)
• scientific article; zbMATH DE number 1538014 (Why is no real title available?)
• scientific article; zbMATH DE number 1765670 (Why is no real title available?)
• αCheck: A mechanized metatheory model checker
• scientific article; zbMATH DE number 1884382 (Why is no real title available?)
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• CONCUR 2005 – Concurrency Theory

Describes a project that uses

Uses Software

• Bedwyr

This page was built for publication: A proof theory for model checking: an extended abstract

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