1090 पेपर
यह शोधपत्र यह प्रदर्शित करके औपचारिक सत्यापन (formal verification) के लिए एक टोपोलॉजिकल ढांचा स्थापित करता है कि सीमित व्यवहार संबंधी अवलोकनों के माध्यम से सत्यापन योग्य गुण सटीक रूप से प्रेरित टोपोलॉजी में खुले सेटों (open sets) के अनुरूप होते हैं, जबकि ट्रेस (trace), सिमुलेशन (simulation) और बिसिम्यूलेशन (bisimulation) संबंधों द्वारा उत्पन्न विशिष्ट संरचनाओं को अभिलक्षणित करते हैं।
यह शोधपत्र DissProve प्रस्तुत करता है, जो एक स्वचालित सत्यापन उपकरण है जो सीमित संचार राउंड के भीतर असीमित निष्पादन इतिहासों को संभालने के लिए मटेरियलाइजेशन (materialization), कॉज़ैलिटी (causality) और समराइजेशन (summarization) जैसी लक्ष्य-निर्देशित तकनीकों का उपयोग करके एफाइन संचार वाले एसिंक्रोनस, पैरामीट्रिक वितरित प्रोटोकॉल के लिए सुरक्षा गुणों को सिद्ध करता है।
यह शोध पत्र क्लिक-गार्डेड फर्स्ट-ऑर्डर लॉजिक विद काउंटिंग (cgFOC) को प्रस्तुत करता है, जो इसके VC और ग्राफ आयामों पर गणनीय सीमाओं (computable bounds) को स्थापित करता है और स्थानीय रूप से सीमित विस्तार वर्गों (locally bounded expansion classes) पर क्वेरी उत्तर देने और सीखने के लिए एल्गोरिद्मिक मेटाथ्योरम्स को सिद्ध करता है, जबकि यह भी प्रदर्शित करता है कि इस तर्क के मामूली विस्तार भी पेड़ों (trees) पर भी अनियंत्रित (intractable) हो जाते हैं।
यह शोध पत्र मार्कोव जंप लीनियर सिस्टम के लिए एक मॉडल चेकिंग फ्रेमवर्क प्रस्तावित करता है जो विशिष्ट प्रारंभिक स्थितियों के सापेक्ष मोमेंट-आधारित स्थिरता गुणों को औपचारिक रूप से निर्दिष्ट और सत्यापित करने के लिए प्रोबेबिलिस्टिक कम्प्यूटेशन ट्री लॉजिक (PCTL) का उपयोग करता है, जो शास्त्रीय एसिम्प्टोटिक स्थिरता विश्लेषण के मुकाबले एक कम रूढ़िवादी विकल्प प्रदान करता है।
यह शोध पत्र रचनात्मक मोडल लॉजिक , , , और के लिए परिमित द्विरिश्तात्मक फ्रेम (finite birelational frame) गुण स्थापित करता है, जिससे उनकी निर्णयक्षमता (decidability) के संबंध में लंबे समय से खुले पड़े प्रश्नों को हल किया गया है और नए जटिलता सीमाएँ (complexity bounds) प्रदान की गई हैं।
यह शोध पत्र अनुकूलित FC-Datalog खंडों (fragments) का एक ढांचा प्रस्तावित करता है जो कोर स्पैनर्स (core spanners) के लिए कुशल, सुलभ स्ट्रिंग क्वेरीइंग को सक्षम करने हेतु अभिव्यंजक शक्ति और कम्प्यूटेशनल दक्षता के बीच संतुलन बनाता है, जिसे नियत रेगुलर एक्सप्रेशन (deterministic regex) के अनुकरण द्वारा प्रदर्शित किया गया है।
यह शोध पत्र यह प्रदर्शित करता है कि जबकि CUSUM जैसी टेम्पोरल एक्यूमुलेशन (temporal accumulation) तकनीकें उन 'स्लो-बर्न' हमलों का पता लगाने के लिए कमजोर, वितरित प्रॉम्प्ट-इंजेक्शन संकेतों को बढ़ा सकती हैं जो प्रति-घटना डिटेक्टरों से बच निकलते हैं, उनकी प्रभावशीलता सख्ती से उन परिदृश्यों तक सीमित है जहाँ व्यक्तिगत घटनाओं में पहले से ही एक पता लगाने योग्य सिग्नल मार्जिन मौजूद होता है, और वे वहां पहचान क्षमता उत्पन्न करने में विफल रहती हैं जहाँ कोई संकेत मौजूद ही नहीं है।
यह शोध पत्र TwoSafe को प्रस्तुत करता है, जो एक नवीन स्टैटिक एनालिसिस टूल है और डीप न्यूरल नेटवर्क की ग्लोबल रोबस्टनेस को कुशलतापूर्वक सत्यापित करने के लिए डिफरेंशियल हेलो ज़ोनोटोप्स (differential halo zonotopes) का उपयोग करता है, जो सटीकता और स्केलेबिलिटी दोनों में मौजूदा अत्याधुनिक तकनीकों से काफी बेहतर प्रदर्शन करता है।
यह शोध पत्र मॉडल दरों में अनिश्चितता को संभालने के लिए पैरामीट्रिक मार्कोव ऑटोमेटा का परिचय देता है और एक दो-चरणीय विविक्तीकरण (डिस्क्रीटाइजेशन) दृष्टिकोण प्रस्तुत करता है, जिसे स्टॉर्म (Storm) मॉडल चेकर में कार्यान्वित किया गया है, ताकि पैरामीटर स्पेस को मनमाने परिशुद्धता के साथ संतुष्ट करने वाले और उल्लंघन करने वाले क्षेत्रों में विभाजित करके समय-बद्ध पहुँच संश्लेषण (reachability synthesis) समस्याओं को हल किया जा सके।
यह शोध पत्र muTGL तर्क को विस्तारित करने के लिए एक "स्पेस होराइजन" (space horizon) ऑपरेटर प्रस्तुत करता है, जो मल्टी-एजेंट सिस्टम में दूरी-बद्ध पहुंच (distance-bounded reachability) और संचार श्रृंखला लागतों के सत्यापन को सक्षम बनाता है, और एक केंद्रीकृत ऑफलाइन मॉनिटरिंग एल्गोरिदम प्रदान करता है जिसे सर्वसम्मति-आधारित कार्य आवंटन प्रोटोकॉल पर सत्यापित किया गया है।