CEGAR-based EF Synthesis of Boolean functions with an Application to Circuit Rectification

Thursday, 2 February 2017 at 11:00 in room INF 328

Heinz Riener, Institute of Space Systems, German Aerospace Center (DLR), Bremen, Germany

 

Abstract:

The Exists-Forall (EF) synthesis problem deals with finding parameters such that for all input assignments a correctness specification is met.  Many standard problems from computer-aided design and verification can be formulated as an instance of EF synthesis when a function template with holes --- parameters to be synthesized --- is provided.

In this talk, the idea of EF synthesis is generalized in the context of Boolean logic by allowing existential quantification over the domain of Boolean functions (rather than Boolean variables).  A bounded synthesis approach guided by counterexamples is presented to generate the Boolean functions using techniques from Boolean learning.  As an application, circuit rectification is introduced as an EF synthesis problem and the presented approach is applied to incrementally synthesize patches for digital circuits with multiple seeded faults.

About the speaker:

Heinz Riener received his Dipl.-Ing. degree in Telematics by the Graz University of Technology, Austria.  He is a researcher in the Institute of Space Systems of the German Aerospace Center (DLR), Bremen, Germany, in the group of Avionics Systems and a Ph.D. candidate at the University of Bremen.  His research interests are formal methods for the design and verification of hardware and software systems.