CTL model checking in deduction modulo

DOI10.1007/978-3-319-21401-6_20MaRDI QIDQ3454102zbMATH OpenOpenAlexFDO

Authors 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

deduction modulomodel checkingresolution modulo

Mathematics Subject Classification ID

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

Recommendations

• A compositional approach to CTL^* verification
• A Sound and Complete Deductive System for CTL* Verification
• scientific article; zbMATH DE number 2090074
• scientific article; zbMATH DE number 1927551
• Rewrite rules for \(\mathrm{CTL}^\ast\)

Cites work

• CTL model checking in deduction modulo
• Embedding Deduction Modulo into a Prover
• Experimenting with deduction modulo
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Polarized Resolution Modulo
• QBF Encoding of Temporal Properties and QBF-Based Verification
• Theorem proving modulo
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo

Cited in

(6)

• A compositional approach to CTL^* verification
• Linear templates of ACTL formulas with an application to SAT-based verification
• Model Checking CTL is Almost Always Inherently Sequential
• Automated Termination in Model Checking Modulo Theories
• CTL model checking in deduction modulo
• A Sound and Complete Deductive System for CTL* Verification

Describes a project that uses

Uses Software

• iProver

This page was built for publication: CTL model checking in deduction modulo

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