Speaker:Chuan Jiang

Major Professor: Ciardo, Gianfranco

Committee Member 1: Basu, Samik

Committee Member 2: Miner, Andrew

Committee Member 3: Lutz, Jack

Committee Member 4: Zhang, Wensheng

Status: Ph.D. Preliminary Oral Defense

Date: Wed, 2018-01-17

Time: 2:00PM

Title: Witness Generation for CTL

Abstract: Proof by witness and disproof by counterexample is an ancient and classic mathematical concept. In formal verification, witnesses and counterexamples provide engineers important debugging information and are helpful to understand system behaviors. One advantage of model checking is the ability to generate witnesses and counterexamples. In the scope of computation tree logic (CTL), we will review two witness generation approaches using decision diagrams and SAT, respectively, and introduce an approach using additive edge-valued decision diagrams to generate minimum witnesses. Future work includes resolving the performance bottlenecks and investigating the possibility of SAT-based approach for minimum witness generation.