1115 पेपर
यह शोध पत्र हाई-लेवल पेट्री नेट्स के सिम्बोलिक अनफोल्डिंग्स के लिए पूर्ण परिमित प्रीफिक्स (complete finite prefixes) को परिभाषित और निर्मित करने के लिए अनफोल्डिंग्स और पूर्ण परिमित प्रीफिक्स की अवधारणाओं को एकीकृत करता है, जो सेफ नेट्स के मौजूदा एल्गोरिदम का सामान्यीकरण करता है और एक अनुकूलित कट-ऑफ मानदंड के माध्यम से अनंत तक पहुँचने योग्य मार्किंग्स वाले नेट्स को संभालने के लिए कार्यप्रणाली का विस्तार करता है।
यह शोध पत्र एक रीराइटिंग लॉजिक सेमेंटिक्स को परिभाषित करके इनहिबिटर आर्च (inhibitor arcs) वाले पैरामीट्रिक टाइम पेट्री नेट्स के लिए एक सुदृढ़ और पूर्ण औपचारिक विश्लेषण और पैरामीटर संश्लेषण ढांचा प्रस्तुत करता है जो Maude और SMT सॉल्विंग के साथ संगत है, जो उन्नत सत्यापन क्षमताओं को सक्षम बनाता है और अक्सर Romeo जैसे मौजूदा उपकरणों से बेहतर प्रदर्शन करता है।
कॉबलस्टोन (Cobblestone) एक लागत प्रभावी, विभाजित-और-जीतें (divide-and-conquer) ढांचा है जो कोक (Coq) में औपचारिक प्रमाणों को पुनरावृत्ति से विघटित और सत्यापित करने के लिए लार्ज लैंग्वेज मॉडल्स का लाभ उठाता है, जो संभावित रूप से दोषपूर्ण एआई घटकों पर निर्भर रहने के बावजूद जटिल प्रमेयों के सत्यापन को सफलतापूर्वक स्वचालित करते हुए भी शुद्धता की गारंटी देता है।
यह शोध पत्र एक नए वितरण-आधारित अर्थविज्ञान (distribution-based semantics) और एक प्रेडिकेट-आधारित परीक्षण दृष्टिकोण को पेश करके समवर्ती प्रणालियों (concurrent systems) में संभाव्य परीक्षण तुल्यता (probabilistic testing equivalences) के लिए एक एकीकृत रूपरेखा प्रस्तावित करता है, जो आंतरिक और बाहरी लक्षण वर्णन प्रदान करता है जो शास्त्रीय तुलमताओं का सामान्यीकरण करते हैं, जिन्हें कॉंग्रुएंस (congruences) सिद्ध किया गया है, और जिनकी संभाव्य बिज़िमिलरिटी (probabilistic bisimilarities) के साथ व्यापक रूप से तुलना की गई है।
यह शोध पत्र माल्सेव ब्लॉक्स के सेमीलैटिस (SMB बीजगणित) प्रस्तुत करता है, जो यह प्रदर्शित करने वाले नए प्रमाण प्रदान करता है कि सभी ऐसे बीजगणित सुलभ कंस्ट्रेंट सैटिस्फैक्शन प्रॉब्लम (CSP) टेम्प्लेट प्रेरित करते हैं, और इस वर्ग पर लागू होने पर CSP डाइकोटॉमी प्रमेय के दो प्रमुख प्रमाणों के बीच संरचनात्मक समानताओं का विश्लेषण करता है।
यह शोध पत्र लीन 4 (Lean 4) में नागाटा के फैक्टोरियलिटी प्रमेय (Nagata's factoriality theorem) के पहले ज्ञात औपचारिकीकरण को प्रस्तुत करता है, जो यह स्थापित करता है कि एक नोएदरियन डोमेन (Noetherian domain) एक यूएफडी (UFD) होता है यदि एक प्राइम-जनरेटेड सबमोनॉइड (prime-generated submonoid) पर इसका लोकलाइजेशन (localization) एक यूएफडी है, और इस परिणाम को यह सिद्ध करने के लिए लागू करता है कि नोएदरियन यूएफडी के ऊपर बहुपद रिंग (polynomial rings) भी यूएफडी होते हैं।
यह शोध पत्र PROMISE को प्रस्तुत करता है, जो एक संरचना-जागरूक (structure-aware) ढांचा है जो कार्य को प्रूफ़-स्टेट संक्रमणों (proof-state transitions) पर एक स्टेटफुल सर्च के रूप में पुनर्गठित करके और पुनरावृत्ति अनुकूलन के लिए संरचनात्मक पैटर्न की माइनिंग करके औपचारिक सत्यापन (formal verification) के लिए स्वचालित प्रूफ़ जनरेशन में सुधार करता है, जिससे seL4 बेंचमार्क पर मौजूदा विधियों की तुलना में महत्वपूर्ण प्रदर्शन लाभ प्राप्त होता है।
यह शोध पत्र UCPDL+ प्रस्तुत करता है, जो लॉजिकों का एक नया परिवार है जो प्रपोजिशनल डायनेमिक लॉजिक (Propositional Dynamic Logic), कंजंक्टिव क्वेरीज (Conjunctive Queries) और यूनरी नेगेशन फर्स्ट-ऑर्डर लॉजिक (Unary Negation First-order logic) के एक विस्तार को एकीकृत करता है, और उनकी तुल्यता, 2ExpTime-पूर्ण संतुष्टि (2ExpTime-complete satisfiability), और निश्चित ट्री-विड्थ उपवर्गों (fixed tree-width subclasses) के लिए PTime मॉडल चेकिंग को स्थापित करता है।
यह शोध पत्र यह सिद्ध करके कि कोई भी बीजगणितीय लंबाई 1 वाला बिना स्यूडो-लूप (pseudo-loop) का स्मूथ डाइग्राफ प्रत्येक परिमित संरचना का निर्माण कर सकता है, अनंत निर्देशित ग्राफ-रंगण (directed graph-colouring) समस्याओं के लिए प्रथम NP-कठिनता मानदंड स्थापित करता है, जिससे -कैटेगोरिकल सेटिंग में प्रमुख परिमित-डोमेन जटिलता परिणामों को सफलतापूर्वक उन्नत किया जा सका है।
यह शोध पत्र परिमित रूप से बंधित समांग मॉडल-पूर्ण कोर (finitely bounded homogeneous model-complete cores) के प्रथम-क्रम विस्तारों पर बाधा संतुष्टि समस्याओं (Constraint Satisfaction Problems) के लिए एक जटिलता द्विशाखन (complexity dichotomy) स्थापित करता है, यह सिद्ध करते हुए कि वे या तो प्रथम-क्रम परिभाषित हैं या प्रथम-क्रम न्यूनीकरणों (first-order reductions) के तहत L-कठिन हैं, जिससे बोडिर्स्की-पिंस्कर अनुमान (Bodirsky-Pinsker conjecture) की दिशा में अब तक का सबसे सामान्य परिणाम प्राप्त होता है।