COMBINING ABDUCTION AND MODEL CHECKING TECHNIQUES FOR REPAIR OF CONCURRENT PROGRAMS (EXTENDED ABSTRACT)

Abstract

We investigate the combination of AI techniques with model checking, which is a suc- cessful approach to verification of particular concurrent systems. We present the system repair problem and as an application the problem of repairing (i.e. correcting) concurrent programs. Moreover, we describe optimization techniques for reducing the search space of a repair, which use the concept of counterexample.