1215 ورقة بحثية
تؤسس هذه الورقة نظرية استحالة فوقية تثبت أنه لا يمكن لأي محمول بنيوي قابل للتحقق بكفاءة أن يحدد بدقة جبهة القابلية للاستدلال فيما يتعلق بشهادة الصلة الدقيقة، حيث تفرض قوانين الإغلاق المعيارية الاتفاق على عائلات عوائق محددة لا يمكن إلا للشهود الأفينيين المستقلين عن الفعل التمييز بينها.
تقدم هذه الورقة تقنيتين متكاملتين للتحليل الساكن تحددان الألوان المتكافئة وتستبعدان الألوان غير القابلة للوصول لتقليص حجم شبكات بيتري الملونة (Colored Petri nets) المنبسطة بشكل كبير، مما يتفوق على الأدوات الحالية في كل من إيجاز الشبكة ومعدلات نجاح التحقق من النموذج.
تقدم هذه الورقة تقنيات تلقائية لاستخلاص الحدود العليا والدنيا للتعقيد المتوازي لإعادة كتابة المصطلحات ذات التداخل المتوازي عبر الاستفدادة من أساليب التعقيد المتسلسل وإرساء معايير كافية للتقارب، وهو إطار عمل تم التحقق من صحته من خلال توسيع أداة AProVE وتجارب قياسية واسعة النطاق.
توحد هذه الورقة بين مفاهيم التوسعات (unfoldings) والبادئات النهائية الكاملة (complete finite prefixes) لتعريف وبناء بادئات نهائية كاملة للتوسعات الرمزية لشبكات بتري عالية المستوى، مما يعمم الخوارزميات الحالية للشبكات الآمنة ويمد المنهجية للتعامل مع الشبكات ذات العلامات القابلة للوصول اللانهائية من خلال معيار قطع (cut-off criterion) مُعدل.
تقدم هذه الورقة إطاراً للتحليل الصوري وتوليف المعلمات لشبكات "بتري" الزمنية ذات المعلمات مع أقواس المثبط، يتسم بالصحة والكمال من خلال تعريف دلالات منطق إعادة الكتابة المتوافقة مع "ماود" (Maude) وحل "الرضا عن قابلية الإرضاء" (SMT)، مما يتيح قدرات تحقق متقدمة ويتفوق غالباً على الأدوات الحالية مثل "روميو" (Romeo).
يُعد Cobblestone إطار عمل فعال من حيث التكلفة، يعتمد على استراتيجية "فرق تسد"، ويستفيد من النماذج اللغوية الكبيرة لتفكيك والتحقق من البراهين الصورية في Coq بشكل تكراري، مما ينجح في أتمتة التحقق من النظريات المعقدة مع ضمان السلامة رغم الاعتماد على مكونات ذكاء اصطناعي قد تكون غير سليمة.
تقترح هذه الورقة إطاراً موحداً لتكافؤات الاختبار الاحتمالية في الأنظمة المتزامنة من خلال تقديم دلالات جديدة قائمة على التوزيع ونهج اختبار قائم على المحمول، مما ينتج عنه توصيفات داخلية وخارجية تعمم التكافؤات الكلاسيكية، ويُثبت أنها علاقات تطابق، وتتم مقارنتها بشكل شامل مع التماثلات الاحتمالية.
تقدم هذه الورقة شبه شبكات كتل مالتسيف (جبرات SMB)، وتقدم براهين جديدة تثبت أن جميع هذه الجبرات تستحث قوالب مسألة إرضاء القيود (CSP) سهلة الحل، وتحلل أوجه التشابه الهيكلية بين البرهينين الرئيسيين لنظرية ثنائية المسألة (Dichotomy Theorem) في مسألة إرضاء القيود عند تطبيقها على هذه الفئة.
تقدم هذه الورقة أول صياغة رسمية معروفة لنظرية ناجاتا في مجال التفكك (Nagata's factoriality theorem) في لغة Lean 4، والتي تثبت أن النطاق النويثري (Noetherian domain) يكون نطاقاً فريد التفكك (UFD) إذا كان تموضعُه عند تحت-مجموعة مونويد مولدة من أعداد أولية هو نطاق فريد التفكك، وتطبق هذه النتيجة لإثبات أن حقول كثيرات الحدود فوق النطاقات النويثرية فريدة التفكك هي أيضاً فريدة التفكك.
تقدم الورقة البحثية PROMISE، وهو إطار عمل مدرك للبنية يعمل على تحسين التوليد الآلي للبراهين للتحقق الرسمي من خلال إعادة صياغة المهمة كبحث حالة فوق انتقالات حالة البرهان وتعدين الأنماط الهيكلية للتكيف التكراري، محققاً مكاسب أداء كبيرة مقارنة بالطرق الحالية في معيار seL4.