Experience with Abstraction-carrying Code

AbstractAbstraction-carrying Code (ACC) certifies a general temporal property for a mobile program using an abstract interpretation of the mobile program. A client receiving the code and the certificate will first validate the abstraction and then run a model checker to verify the temporal property.In this paper, we report our experience in designing the ACC Evaluation Prototype Toolkit (ACCEPT) and the application of ACCEPT to simple concurrent programs and Linux device drivers. The toolkit is distinguished by an abstraction preserving compilation scheme that generates a Boolean program for an intermediate program compiled from the source program. Some common compiler optimizations are still possible. We report several applications of ACCEPT, including the reachability properties of industrial strength C programs. Preliminary results show that the size of a typical certificate is significantly smaller than the size of the intermediate program. Compared with traditional proof-based certification method, using ACC verification a client spends more time to verify the desired property. Our experience shows this penalty is often tolerable in practice