1086 पेपर
यह शोध पत्र कुछ अनबाउंडेड (unbounded) पेड़ों को बाउंडेड (bounded) पेड़ों में एलीमेंटरी रूप से एम्बेड करने के लिए एक पर्याप्त स्थिति स्थापित करता है, और साथ ही ट्री ऑपरेशन्स (tree operations) पेश करते हुए उनके फेफ़रमैन-वॉघ (Feferman-Vaught) शैली के संरक्षण गुणों को सिद्ध करता है।
यह शोध पत्र हायर-ऑर्डर मोडल फिक्स्ड-पॉइंट लॉजिक (HFL) के एक को-एल्जेब्रिक विस्तार को प्रस्तुत करता है जो HFL और इसके संभाव्य (प्रोबेबिलिस्टिक) संस्करण को एकीकृत करता है, यह प्रदर्शित करते हुए कि नॉन-डिटरमिनिस्टिक और प्रोबेबिलिस्टिक ऑटोमेटा के लिए प्रमुख निर्णय समस्याओं को इस नए ढांचे के भीतर मॉडल-चेकिंग में घटाया जा सकता है।
यह शोध पत्र टेलर एक्सपेंशन के माध्यम से -कैलकुलस के रैखिक सन्निकटन (linear approximation) की रूढ़िवादिता (conservativity) की जांच करता है, यह प्रदर्शित करते हुए कि जबकि यह गुण परिमित पदों (finite terms) के लिए मान्य है, यह "एकॉर्डियन" (Accordion) नामक एक प्रति-उदाहरण के कारण अनंत रिडक्शन (infinitary reductions) के लिए विफल हो जाता है, जिसे एक एकरूपता प्रतिबंध (uniformity constraint) लागू करके हल किया जाता है जो एक रूढ़िवादी विस्तार (conservative extension) प्रदान करता है जो -रिडक्शन पर भी लागू होता है।
यह शोधपत्र Btor2MLIR प्रस्तुत करता है, जो MLIR फ्रेमवर्क पर निर्मित एक नया हार्डवेयर सत्यापन प्रारूप और टूलचेन है जो सत्यापन उपकरणों के तीव्र प्रोटोटाइपिंग को सक्षम करने के लिए परिपक्व कंपाइलर इंफ्रास्ट्रक्चर का लाभ उठाता है और प्रमुख Btor2 प्रारूप के एक सशक्त विकल्प के रूप में कार्य करता है।
यह शोध पत्र निश्चित क्रम के रैखिक पुनरावृत्ति अनुक्रमों (linear recurrence sequences) पर बाउंडेड स्कोलेम समस्या (bounded Skolem Problem) के लिए एक रैंडमाइज्ड पॉलिनॉमियल-टाइम एल्गोरिदम प्रस्तुत करता है, जो -adic विश्लेषण का उपयोग करके संभावित शून्य (candidate zeros) को अलग करने और सत्यापन के लिए अरिथमेटिक-सर्किट आइडेंटिटी टेस्टिंग का लाभ उठाकर, क्रम 4 तक की अनरिस्ट्रिक्टेड स्कोलेम समस्या के लिए जटिलता ऊपरी सीमा को से में सुधारता है।
यह शोधपत्र एक नवीन लूप-ऑटोमेटा मॉडल पेश करके यह स्थापित करता है कि ग्राफ लूप ऑपरेटर (और आगे टॉप, टेस्ट, कन्वर्स और नोमिनेल्स के साथ) के साथ विस्तारित रिलेशनल क्लीने अलजेब्रा का इक्वेशनल थ्योरी PSPACE-कंप्लीट है, जिससे इन सिद्धांतों को 2-वे अल्टरनेटिंग ऑटोमेटा की भाषा समावेशन समस्या में कम किया जा सके, और इस प्रकार डोमेन के साथ रिलेशनल KAT की जटिलता के संबंध में एक खुले प्रश्न को हल किया जा सके।
यह शोध पत्र बाउंडेड मोडल लॉजिक (BML) को प्रस्तुत करता है, जो एक कंस्ट्रक्टिव मोडल लॉजिक है जिसमें स्पष्ट स्कोप डिपेंडेंसी और स्कोप नामों पर फर्स्ट-ऑर्डर क्वांटिफिकेशन शामिल है, ताकि मल्टी-स्टेज प्रोग्रामिंग के लिए एक साउंड और कंप्लीट टाइप-थ्योरेटिक फाउंडेशन प्रदान किया जा सके जो क्रॉस-स्टेज पर्सिस्टेंस जैसी जटिल स्कोपिंग संरचनाओं को कठोरता से संभाल सके।
यह शोध पत्र सोडा (Soda) में कार्यान्वित एक मॉड्यूलर, फंक्शनल प्रोग्रामिंग फ्रेमवर्क प्रस्तुत करता है जो मल्टी-एजेंट सिस्टम के लिए कंपोजेबल वेरिफिकेशन पाइपलाइनों को सक्षम बनाता है, जिससे उपयोगकर्ताओं को गलत सूचना और भावनात्मक तर्क जैसे जटिल परिदृश्यों वाले गतिशील सिस्टम के लिए YAML में डोमेन विवरण परिभाषित करने और पारदर्शी, गारंटीकृत-समाप्ति वाले रीजनिंग वर्कफ़्लो निष्पादित करने की अनुमति मिलती है।
यह शोध पत्र संभाव्य प्रक्रियाओं (probabilistic processes) के लिए एक नवीन ब्रांचिंग बिसिम्यूलेशन (branching bisimulation) प्रस्तुत करता है जो अवलोकनीय न होने वाले कार्यों (unobservable actions) को एब्स्ट्रैक्ट करने के मौजूदा तरीकों की तुलना में अधिक परिष्कृत तुल्यता संबंध स्थापित करता है, जिसमें मानक स्थिर, गतिशील और पुनरावर्ती संरचनाओं के अनुकूल एक रूटेड कॉंग्रुएंस (rooted congruence) संस्करण शामिल है।
यह शोध पत्र PriorProof को प्रस्तुत करता है, जो एक स्वचालित, ऑन्टोलॉजी-मुक्त विधि है जो लीन (Lean) में औपचारिक प्रमाण तकनीकों की नवीनता को उनके डिपेंडेंसी फुटप्रिंट्स (dependency footprints) के सरप्राइज़ल (surprisal) को एक समय-बद्ध पूर्ववर्ती (time-anchored prior) के विरुद्ध मापकर मात्रात्मक रूप से निर्धारित करता है, जो मानव विशेषज्ञों के साथ मध्यम सहमति प्रदर्शित करता है और विशेषज्ञ निर्णय के विकल्प के बजाय एक विखंडनीय (decomposable), व्याख्या योग्य संकेत के रूप में कार्य करता है।