Chuan Jiang: PhD Preliminary Oral Defense

Event
Speaker: 
Chuan Jiang
Wednesday, January 17, 2018 - 2:00pm
Location: 
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.

Category: