Key points are not available for this paper at this time.
تتمثل المهمة المركزية لتحليل البرامج في كيفية العثور بكفاءة على تجريد للبرنامج يحتفظ فقط بالمعلومات ذات الصلة لإثبات الخصائص المهمة. نقدم نهجًا جديدًا للعثور على مثل هذه التجريدات لتحليلات البرامج المكتوبة في Datalog. يعتمد نهجنا على تحسين التجريد الموجه بواسطة أمثلة مضادة: عندما يفشل تشغيل تحليل Datalog باستخدام تجريد، يسعى لتعميم سبب الفشل على تجريدات أخرى، واختيار تجريد جديد يتجنب فشلًا مشابهًا. تستخدم حلا لدينا صياغة منطقية ثنائية دقيقة تكون عامة وكاملة وأمثل: فهي مستقلة عن محلل Datalog، وتعمم فشل التجريد على أكبر عدد ممكن من التجريدات الأخرى، وتحدد أرخص تجريد محسَّن للتجربة التالية. نعرض أداء نهجنا على تحليل المؤشرات وتحليل حالة النوع، على ثمانية برامج benchmark حقيقية بلغة Java.
درس Zhang وآخرون (الثلاثاء) هذا السؤال.