Automatic Generation of Temporal Logic Properties

When: Tuesday, January 29, 2019
Where: PGH 563
Time: 2:00 PM

Speaker: Prof. Görschwin Fey, Institute of Embedded Systems at Hamburg University of Technology 

Host: Prof. Albert Cheng

Design understanding approaches automatically derive knowledge from an unknown system implementation.  Useful applications are debugging, reverse engineering, security analysis, or specification mining.  In this paper, we propose syntax-guided enumeration to derive temporal logic properties from a sequential logic network.  Each property is a temporal logic formula which describes a relation between the primary inputs, the primary outputs, and the latches of the network over time.  We filter vacuously-satisfied and equivalent properties and rank the properties by their strength before presenting them to the user.  The approach is applicable to different temporal logics, but requires that efficient decision procedures for model-checking and satisfiability are available.

Bio:

Since September 2017 Görschwin Fey is a professor at the Institute of Embedded Systems at Hamburg University of Technology (TUHH). Görschwin Fey received his Diploma in Computer Science from Martin-Luther-University Halle-Wittenberg in 2001 and his Dr.-Ing. in Computer Science from University of Bremen in 2006, respectively. From 2012-2017 he headed the Department of Avionics Systems at the Institute of Space Systems of the German Aerospace Center (DLR) and the Group of Reliable Embedded Systems at the University of Bremen. His research interests in Electronic Design Automation (EDA) and automation of embedded system design focus on reliability, debugging, and design understanding