Automated specification inference in a combined domain via user-defined predicates

شناخت ویژگی های برنامه به صورت خودکار برای برنامه های دستکاری شده، به دلیل پیچیدگی آلیاژی و تغییر پذیری ساختارهای داده، یک کار چالش برانگیز است. این وظیفه به وسیله یک دامنه بیانگر ترکیبی از اطلاعات شکل، عددی و کیسه ای پیچیده می شود. در این مقاله، ما یک چارچوب تجزیه و تحلیل ترکیب بندی ارائه می دهیم که خلاصه را برای هر روش در دامنه انتزاعی بیانگر مستقل از تماس گیرندگان خود می گیرد. ما پیشنهاد یک روش انتزاعی جدید با تکنیک بی حادثه در زمینه ترکیبی برای کشف پیش و پس از شرایطی که قبل از آن نمی توان به طور خودکار پیش بینی کرد. این تجزیه و تحلیل نه تنها ویژگی های ایمنی حافظه را در بر می گیرد، بلکه روابط بین حوزه های خالص و شکل را نسبت به صحت عملکرد کامل برنامه ها پیدا می کند. یک نمونه از چارچوب اجرا شده است و آزمایش های اولیه نشان داده اند که رویکرد ما می تواند خواص جالبی را برای برنامه های بی اهمیت بیابد.