CTL Model Checking in Deduction Modulo

DOI10.1007/978-3-319-21401-6_20zbMath1465.68180OpenAlexW1455388678MaRDI QIDQ3454102

Kailiang Ji

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

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

zbMATH Keywords

model checkingdeduction moduloresolution modulo

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

CTL Model Checking in Deduction Modulo ⋮ Linear templates of ACTL formulas with an application to SAT-based verification

Uses Software

• iProver

Cites Work

• Unnamed Item
• Theorem proving modulo
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Polarized Resolution Modulo
• QBF Encoding of Temporal Properties and QBF-Based Verification
• CTL Model Checking in Deduction Modulo
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Embedding Deduction Modulo into a Prover
• Experimenting with Deduction Modulo

This page was built for publication: CTL Model Checking in Deduction Modulo