A proof theory for model checking

DOI10.1007/s10817-018-9475-3zbMath1468.03078OpenAlexW2809678222MaRDI QIDQ2331070

Quentin Heath, Dale A. Miller

Publication date: 25 October 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01814006/file/hal.pdf

zbMATH Keywords

fixed pointslinear logicproof theorymodel checkingfocused proof systems

Mathematics Subject Classification ID

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

Related Items (5)

The undecidability of proof search when equality is a logical connective ⋮ When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Non-well-founded deduction for induction and coinduction ⋮ Integrating induction and coinduction via closure operators and proof cycles

Uses Software

• Bedwyr

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Proof and refutation in MALL as a game
• Focusing and polarization in linear, intuitionistic, and classical logics
• Encoding transition systems in sequent calculus
• Cut-elimination for a logic with definitions and induction
• A semantic framework for proof evidence
• Petri nets, Horn programs, linear logic and vector games
• Cut elimination for a logic with induction and co-induction
• A two-level logic approach to reasoning about computations
• Extracting Proofs from Tabled Proof Search
• Proof search specifications of bisimulation and modal logics for the π-calculus
• The Beginning of Model Checking: A Personal Perspective
• Temporal Verification of Reactive Systems: Response
• Incorporating Tables into Proofs
• A new constructive logic: classic logic
• Logic Programming with Focusing Proofs in Linear Logic
• Foundational Proof Certificates in First-Order Logic
• A proof theory for generic judgments
• Reasoning with higher-order abstract syntax in a logical framework
• A formulation of the simple theory of types
• Least and Greatest Fixed Points in Linear Logic

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