1117 पेपर
यह शोध पत्र एक फाइन-ट्यून्ड लार्ज लैंग्वेज मॉडल फ्रेमवर्क प्रस्तुत करता है जो पारंपरिक इंजीनियरिंग तकनीकों, पुनरावृत्ति त्रुटि विश्लेषण और विशेषज्ञ फीडबैक को एकीकृत करके Oracle PL/SQL से PostgreSQL में SQL-आधारित सिस्टम के माइग्रेशन को प्रभावी ढंग से स्वचालित करता है, जिससे सिंटैक्स त्रुटियों को काफी कम किया जा सके और डेटाबेस लॉजिक को अनुकूलित किया जा सके।
यह शोध पत्र ग्रामर व्युत्पत्ति वृक्षों (grammar derivation trees) के लिए VASS अपघटन तकनीकों का सामान्यीकरण करके, एक-आयामी पतले ग्रामर वेक्टर एडिशन सिस्टम्स (thin 1-GVAS) के लिए एक प्रभावी पूर्णांक प्रोग्रामिंग प्रणाली स्थापित करता है, जिससे इंडेक्स माप (index measure) के आधार पर उनकी पहुँच योग्यता समस्या (reachability problem) की जटिलता पर एक अधिक सटीक ऊपरी सीमा प्राप्त होती है।
यह शोध पत्र रिलेशनल कलर रिफाइनमेंट (RCR) को प्रस्तुत करता है, जो मनमाने रिलेशनल स्ट्रक्चर्स के लिए शास्त्रीय कलर रिफाइनमेंट एल्गोरिदम का एक सामान्यीकरण है, और यह स्थापित करता है कि इसे समय में कार्यान्वित किया जा सकता है जबकि अचक्रीय (acyclic) रिलेशनल स्ट्रक्चर्स से होमोमोर्फिज्म और काउंटिंग क्वांटिफायर के साथ गार्डेड फ्रैगमेंट ऑफ फर्स्ट-ऑर्डर लॉजिक के वाक्यों के माध्यम से इसकी विभेदक शक्ति (distinguishing power) को सटीक रूप से वर्णित किया गया है।
यह शोध पत्र बेयसियन नेटवर्क को लीनियर लॉजिक प्रूफ-नेट्स में मैप करके बेयसियन इन्फरेंस के लिए एक प्रूफ़-थ्योरेटिकल ढांचा स्थापित करता है, जिसका लक्ष्य संरचनात्मक लचीलेपन और कम्प्यूटेशनल दक्षता के बीच संतुलन बनाने वाली कंपोजिशनल ग्राफिकल विधियाँ प्रदान करना है।
यह शोध पत्र CSLib को प्रस्तुत करता है, जो एक ओपन-सोर्स फ्रेमवर्क है जिसे लीन (Lean) प्रूफ असिस्टेंट के भीतर कंप्यूटर विज्ञान के लिए एक व्यापक, मैथलिब (Mathlib) जैसा ज्ञान आधार स्थापित करने के लिए डिज़ाइन किया गया है, जिससे व्यापक शैक्षिक अंगीकरण को सक्षम बनाया जा सके और बड़े पैमाने पर औपचारिक रूप से सत्यापित प्रणालियों के विकास को सुगम बनाया जा सके।
यह शोध पत्र Cargo Sherlock को प्रस्तुत करता है, जो एक SMT-आधारित फ्रेमवर्क है जो Rust डिपेंडेंसीज़ में सप्लाई चेन हमलों का पता लगाने के लिए मेटाडेटा-संचालित मानव कारकों (human factors) और कोड विश्लेषण को औपचारिक रूप से संयोजित करके सॉफ्टवेयर ट्रस्ट (software trust) को मापता है।
यह शोध पत्र प्रस्तुत करता है, जो प्रतिपक्ष (contraposition) और एक अद्वितीय "प्रति-प्रतिस्थापन" (contra-substitution) तंत्र पर आधारित एक नवीन शास्त्रीय रैखिक -कैलकुलस है, जिसे क्लासिकल मल्टीप्लिकेटिव एक्सपोनेंशियल लीनियर लॉजिक (MELL) के लिए सुसंगत (sound), पूर्ण (complete) और सुदृढ़ रूप से सामान्यीकृत (strongly normalizing) सिद्ध किया गया है।
यह शोध पत्र परिभाषाओं के तर्क (logic of definitions) के लिए टियू (Tiu) की कमजोर स्तरीकरण स्थिति (weakened stratification condition) का विस्तार जेनेरिक (नाब्ला) क्वांटिफिकेशन और सामान्य इंडक्शन को शामिल करने के लिए करता है, जिससे एबेला (Abella) प्रूफ़ असिस्टेंट को नकारात्मक उद्गामनों (negative occurrences) वाले परिभाषाओं को समर्थन देने में सक्षम बनाया जा सके, जैसे कि तार्किक संबंधों (logical relations) के लिए आवश्यक होते हैं।
यह शोध पत्र पेट्री नेट्स के लिए एक नवीन प्रतीकात्मक मॉडल चेकिंग विधि प्रस्तुत करता है जो स्टेट स्पेस एक्सप्लोजन (state space explosion) से निपटने के लिए वेक्टर्स पर सामान्यीकृत अंतरालों (generalised intervals) का उपयोग करता है, जो कुशल सैचुरेशन और क्लस्टरिंग तकनीकों के माध्यम से ग्लोबल सीटीएल (global CTL) सत्यापन कार्यों पर आशाजनक प्रदर्शन प्रदर्शित करता है।
यह शोध पत्र न्यूनतम-लागत प्रवाह (minimum-cost flows) के लिए ऑरलिन के कैपेसिटी स्केलिंग एल्गोरिदम की शुद्धता और वर्स्ट-केस रनिंग टाइम का इज़ाबेले/एचओएल (Isabelle/HOL) में पहला औपचारिक निरूपण प्रस्तुत करता है, जिसमें स्टेपवाइज रिफाइनमेंट के माध्यम से व्युत्पन्न एक पूर्ण रूप से निष्पादन योग्य कार्यान्वयन और सामान्य समस्या से एक सत्यापित न्यूनीकरण (verified reduction) शामिल है।