1117 पेपर
यह शोध पत्र GKAT और CF-GKAT ट्रेस तुल्यता (trace equivalence) के लिए कुशल, SAT-आधारित प्रतीकात्मक निर्णय प्रक्रियाओं (symbolic decision procedures) को प्रस्तुत करता है, जिसे Rust में कार्यान्वित किया गया है, जो मौजूदा उपकरणों की तुलना में प्रदर्शन में क्रम-दर-क्रम (order-of-magnitude) सुधार प्रदर्शित करते हैं और उद्योग-मानक Ghidra डीकंपाइलर में एक बग को सफलतापूर्वक पहचाना है।
यह शोध पत्र विभिन्न ग्राफ निर्माणों के माध्यम से ट्री-ऑर्डर्ड वीकली स्पार्स संरचनाओं के मोनाडिकली डिपेंडेंट वर्गों के अभिलक्षण प्रदान करता है, यह स्थापित करते हुए कि ऐसे वर्ग मोनाडिकली डिपेंडेंट हैं यदि और केवल यदि उनका स्पारसीफिकेशन नाउहियर-डेंस है, जबकि स्वतंत्र हेरेडिटरी वर्गों पर फर्स्ट-ऑर्डर मॉडल चेकिंग की जटिलता को भी प्रदर्शित करता है और माइनर-एक्सक्लूडिंग ग्राफ वर्गों के लिए एक नवीन मॉडल-थ्योरेटिकल अभिलक्षण प्रस्तुत करता है।
यह शोध पत्र सफिशिएंट इनकरेक्टनेस लॉजिक (SIL) को प्रस्तुत करता है, जो एक नया अंडर-एप्रोक्सिमेटिंग प्रोग्राम लॉजिक है जिसे त्रुटियों की ओर ले जाने वाली प्रारंभिक अवस्थाओं के सेट की सटीक पहचान करने के लिए डिज़ाइन किया गया है, और यह पॉइंटर्स तथा डायनेमिक एलोकेशन को संभालने के लिए सेपरेशन लॉजिक के साथ इसका विस्तार करता है, जबकि मौजूदा दृष्टिकोणों की तुलना में अधिक मजबूत गारंटी और अधिक संक्षिप्त पोस्टकंडीशन्स (postconditions) प्रदान करता है।
यह शोधपत्र एक ऐसे ढांचे को प्रस्तुत करता है जो डेटा-संचालित प्रक्रियाओं, स्वचालित टेम्पलेट-आधारित मॉडलिंग और cATM तर्क का उपयोग करके MITRE हमले के अभियानों की संभावना को परिमाणित करता है ताकि साइबर सुरक्षा रक्षा प्राथमिकता निर्धारण के लिए पारदर्शी, जवाबदेह और कुशल मात्रात्मक तुलना सक्षम की जा सके।
यह शोधपत्र सार्वभौमिक गुणों और पुनरावृत्ति अनरैवलिंग (iterative unravellings) के माध्यम से वृक्षों (trees) को अभिलक्षणिक बनाने और उनके निर्माण हेतु 'रीचेबल को-अल्जेब्रा' (reachable coalgebra) के सिद्धांत का सामान्यीकरण करता है, जो यह प्रदर्शित करता है कि दोनों दृष्टिकोण एक एकीकृत 'रीचेबिलिटी' (reachability) की अवधारणा से उत्पन्न होते हैं जो सभी विश्लेषणात्मक सेट फंक्टर्स (analytic set functors) पर लागू होती है।
यह शोध पत्र REAL को प्रस्तुत करता है, जो पूर्णांकों (integers), वास्तविक संख्याओं (reals) और मिश्रित डोमेन पर रैखिक अंकगणित सिद्धांतों (linear arithmetic theories) में रामसे क्वांटिफायर (Ramsey quantifiers) को हटाने के लिए एक कुशल उपकरण है, जो FASTer रीचेबिलिटी एनालाइज़र की पहुंच को SMT-LIB-आधारित प्रारूप में एक स्वचालित अनुवाद के माध्यम से विस्तारित करके लाइवनेस सत्यापन (liveness verification) को महत्वपूर्ण रूप से त्वरित करता है।
यह शोध पत्र "सबफ्लिप" (subflip) ऑपरेशन को इन वर्गों को अभिलक्षित करने के लिए और यह प्रदर्शित करने के लिए कि इन्हें केवल अस्तित्वपरक धनात्मक प्रथम-क्रम सूत्रों (existential positive first-order formulas) का उपयोग करके 'नोवेयर डेंस' (nowhere dense) वर्गों से तार्किक रूप से एनकोड किया जा सकता है, को-मैचिंग-फ्री मोनाडिकली स्थिर ग्राफ वर्गों के लिए अस्तित्वपरक धनात्मक स्पार्सिफिकेशन अनुमान (existential positive sparsification conjecture) का प्रस्ताव और सत्यापन करता है।
यह शोध पत्र लेयर्ड ऑटोमेटा (layered automata) को अल्टरनेटिंग पैरिटी ऑटोमेटा (alternating parity automata) के एक कैनोनिकल, बहुपद-समय गणना योग्य उपवर्ग के रूप में प्रस्तुत करता है जो नियतात्मक मॉडलों का सामान्यीकरण करता है, ओमेगा-रेगुलर भाषाओं के लिए अद्वितीय न्यूनतम रूपों की पेशकश करता है और कुशल निरंतरता जाँच (consistency checking) तथा समावेशन परीक्षण (inclusion testing) को सक्षम बनाता है।
यह शोध पत्र लर्निंग रेट्स पर बाधाओं को शिथिल करके अनुमानित फलनों के फिक्स्पॉइंट्स की गणना करने के लिए डैम्प्ड मैन इटरेशन स्कीम का सामान्यीकरण करता है, जिससे उच्च-आयामी समस्याओं के लिए अराजक इटरेशन (chaotic iterations) सक्षम होते हैं और सिंपल स्टोकेस्टिक गेम्स जैसे संभाव्य मॉडलों के लिए प्रयोज्यता का विस्तार होता है।
यह शोध पत्र संक्रमण संभावनाओं (transition probabilities) में एपिस्टेमिक अनिश्चितता (epistemic uncertainty) को संभालने के लिए रोबस्ट कंकरेंट स्टोकेस्टिक गेम्स (विशेष रूप से इंटरवल सीएसजी) प्रस्तुत करता है, जो जीरो-सम और नॉन-जीरो-सम उद्देश्यों के वर्स्ट-केस रोबस्ट वेरिफिकेशन के लिए एक सैद्धांतिक ढांचा और कुशल एल्गोरिदम प्रदान करता है, जिन्हें PRISM-games मॉडल चेकर में कार्यान्वित किया गया है और बड़े बेंचमार्क पर सत्यापित किया गया है।