Browsing Waterloo Research by Subject "symbolic model checking"

Now showing items 1-2 of 2

Extracting Counterexamples from Transitive-Closure-Based Model Checking

Kember, Mitchell; Tran, Lynn; Gao, George; Day, Nancy (IEEE, 2019)

We address the problem of how to extract counterexamples for the transitive-closure-based model checking (TCMC) technique. TCMC is a representation of the CTLFC (CTL with fairness constraints) model checking problem in ...
Transitive-closure-based model checking (TCMC) in Alloy

Farheen, Sabria; Day, Nancy A.; Vakili, Amirhossein; Abbassi, Ali (Springer, 2020-01-03)

We present transitive-closure-based model checking (TCMC): a symbolic representation of the semantics of computational tree logic with fairness constraints (CTLFC) for finite models in first-order logic with transitive ...