Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse

DOI10.29007/2S1QzbMATH Open1415.68149OpenAlexW2907427247MaRDI QIDQ5222973FDOQ5222973

Authors: Chuan Jiang, Gianfranco Ciardo 

Publication date: 4 July 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.29007/2s1q

Recommendations

• Theory and Applications of Models of Computation
• Improving saturation-based bounded model checking
• Formal Methods in Computer-Aided Design
• scientific article; zbMATH DE number 1670796
• Bounded model checking using satisfiability solving

zbMATH Keywords

SATcounterexamplebounded model checkingdeadlockwitnessACTLECTL

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cited In (2)

• Improving the translation from ECTL to SAT
• A new translation from ECTL* to SAT*

This page was built for publication: Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse

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