1086 पेपर
यह शोध पत्र कार्नाप (Carnap) प्रूफ़ असिस्टेंट फ्रेमवर्क पर एक दशक लंबे अनुभव की रिपोर्ट प्रस्तुत करता है जिसका उपयोग 45,000 से अधिक छात्रों द्वारा किया गया है, जो उन प्रमुख सफलताओं और चुनौतियों की पहचान करता है जिन्होंने एक उच्च-प्रदर्शन वाले mm0-zig सत्यापन कर्नेल (verifier kernel) और बेहतर वेब-आधारित प्रूफ़ लेखन के लिए ऑफ़बौ (Aufbau) बाइटकोड कंपाइलर वाले बॉटम-अप पुनर्गठन को प्रेरित किया।
यह शोधपत्र यह प्रदर्शित करता है कि मानक ट्यूरिंग मॉडल में, कोई भी एकसमान स्वीकार्य विधि (uniform admissible method) P बनाम NP या वन-वे फंक्शन्स जैसी गैर-तुच्छ (non-trivial) गुणों के लिए सिमेंटिक प्रमाण पत्र (semantic certificates) उत्पन्न नहीं कर सकती, क्योंकि आवश्यक एकरूपता (uniformity) अंतर्निहित रूप से एक निर्णय प्रक्रिया (decision procedure) को प्रेरित करती है जिसे राइस का प्रमेय (Rice's theorem) असंभव सिद्ध करता है।
LAP टूलसेट एक जावा-आधारित, डिपेंडेंसी-मुक्त कमांड-लाइन सुइट है जिसे मानक प्रपोजिशनल और फर्स्ट-ऑर्डर लॉजिक एल्गोरिदम को लागू करके और नेचुरल डिडक्शन डेरिवेशंस को बनाने, जांचने और विज़ुअलाइज़ करने के लिए इंटरैक्टिव सहायता प्रदान करके कंप्यूटर विज्ञान में तर्क (लॉजिक), एल्गोरिदम और प्रमाण सिखाने के लिए डिज़ाइन किया गया है।
यह शोध पत्र सिमपलीशियल होमोटॉपी टाइप थ्योरी के भीतर लॉजिकल रिलेशंस के लिए एक निर्देशित, प्रूफ-रेलेवेंट फ्रेमवर्क विकसित करता है, जो रिडक्शन को इनइक्वैलिटी टाइप्स के रूप में आंतरिक बनाने और डिपेंडेंट टाइप्स के लिए निर्देशित बूलियन कैनोनिसिटी और रिप्रेजेंटेशन इंडिपेंडेंस को सिद्ध करने वाले मॉडल्स का निर्माण करने के लिए कॉन्ट्रावेरिएंट फैमिलियों का उपयोग करता है।
यह शोधपत्र यह स्थापित करता है कि लगभग-आवर्ती (almost-periodic) शब्द सटीक रूप से वे अनंत शब्द हैं जिन पर मोडल म्यू-कैलकुलस (modal mu-calculus) परिमित अभिसरण (finite convergence) का आनंद लेता है, जिससे इस गुण का एक पूर्ण लक्षण वर्णन प्राप्त होता है और सेमेनोव के 1984 के निर्णायकता परिणाम का एक नया प्रमाण मिलता है।
यह शोध पत्र लैम्ब्डा कैलकुलस की व्याख्या करने के लिए डोमेन-मान वाले रैंडम वेरिएबल्स का उपयोग करते हुए बुलियन-मानित डोमेन थ्योरी (Boolean-valued domain theory) विकसित करता है, जो रिफ्लेक्सिव डोमेन निर्माण पर केंद्रित है जहाँ समीकरण की वैधता को अंतर्निहित बुलियन बीजगणित के शीर्ष तत्व (top element) तक पहुँचने द्वारा परिभाषित किया जाता है।
यह शोध पत्र निष्पक्ष व्यापार को लागू करने के लिए डिक्लेरेटिव पॉलिसी लैंग्वेज MuAC और नॉन-स्टैंडर्ड लॉजिक MuACL को परिभाषित करके, सिस्टम की डैसिडेबिलिटी (decidability) को सिद्ध करके, और ब्लॉकचेन-आधारित नॉन-फंजिबल टोकन लेनदेन में इसके व्यावहारिक अनुप्रयोग को प्रदर्शित करके सुरक्षित डिजिटल संसाधन आदान-प्रदान के लिए एक औपचारिक ढांचे (formal framework) को प्रस्तुत करता है।
यह शोध पत्र एक नवीन रूपरेखा प्रस्तुत करता है जो P4 कंट्रोल ब्लॉक्स से परे औपचारिक सत्यापन (formal verification) का विस्तार करती है ताकि पार्सर (parsers), डीपार्सर (deparsers) और गैर-P4 घटकों सहित संपूर्ण पैकेट प्रोसेसिंग पाइपलाइनों की कार्यात्मक शुद्धता को व्यापक रूप से सिद्ध किया जा सके, और यह प्रदर्शित किया जा सके कि स्विच के समग्र व्यवहार को मान्य करने के लिए इन विविध तत्वों के प्रमाणों को कैसे संयोजित किया जाता है।
यह अनुभव रिपोर्ट विवरण देती है कि कैसे AI-सहायता प्राप्त उपकरणों (Codex) का उपयोग परिवर्तनीय अपडेट को संभालने के लिए एक नए रिकॉर्डेड-बैकवर्ड-एज इनवेरिएंट (recorded-backward-edge invariant) के इर्द-गिर्द सत्यापन को पुनर्गठित करके Rocq में CertiGC सत्यापित जनरेशनल गारबेज कलेक्टर प्रमाण को स्थिर करने और पूर्ण करने के लिए किया गया था, जबकि मानव विशेषज्ञों ने शुद्धता सुनिश्चित करने के लिए इनवेरिएंट्स के अधिनिर्णय और प्रमाण पथ के ऑडिट पर ध्यान केंद्रित किया।
यह शोध पत्र LLVM IR स्तर पर एक स्थानिक सत्यापन ढांचे (spatial verification framework) को प्रस्तुत करता है जो गैर-एफ़ाइन सरणी एक्सेस (non-affine array accesses) को बहुरूपी स्थानिक विधेयकों (polymorphic spatial predicates) के रूप में मॉडल करके हाई-लेवल सिंथेसिस में मेमोरी संघर्षों का पता लगाने और उन्हें रोकने के लिए सेपरेशन लॉजिक (Separation Logic) और SMT सॉल्वर का उपयोग करता है, जिससे पारंपरिक पॉलीहेड्रल विधियों के प्रदर्शन को कम करने वाले अति-अनुमानों (over-approximations) के बिना सुरक्षित समानांतरकरण सक्षम होता है।