A proof theory for model checking
From MaRDI portal
Publication:2331070
DOI10.1007/s10817-018-9475-3zbMath1468.03078OpenAlexW2809678222MaRDI QIDQ2331070
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
Specification and verification (program logics, model checking, etc.) (68Q60) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Related Items
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
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
