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

DOI10.29007/2S1QMaRDI QIDQ5222973zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

ACTLbounded model checkingcounterexampledeadlockECTLSATwitness

Mathematics Subject Classification ID

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

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

Cited in

(4)

• Supporting SAT based BMC on finite path models
• A new translation from ECTL* to SAT*
• Comparing SAT- and SMT- based bounded model checking for ECTL properties
• Improving the 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)