Chuan Jiang: PhD Preliminary Oral Defense

Chuan Jiang
Wednesday, January 17, 2018 - 2:00pm
223 Atanasoff
Event Type: 

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.