smack

SMACK एक मॉड्यूलर सॉफ्टवेयर सत्यापन टूलचेन और एक स्व-निहित सॉफ्टवेयर सत्यापक दोनों है। इसका उपयोग अपने इनपुट प्रोग्रामों में अभिकथनों को सत्यापित करने के लिए किया जा सकता है। अपने डिफ़ॉल्ट मोड में, लूप पुनरावृत्तियों और रिकर्सन गहराई पर दी गई सीमा तक अभिकथनों को सत्यापित किया जाता है; इसमें असीमित सत्यापन के लिए प्रायोगिक समर्थन भी है। SMACK C भाषा की जटिल विशेषताओं को संभालता है, जिसमें डायनामिक मेमोरी आवंटन, पॉइंटर अंकगणित, और बिटवाइज़ ऑपरेशन शामिल हैं।

हुड के नीचे, SMACK LLVM कंपाइलर के लोकप्रिय मध्यवर्ती प्रतिनिधित्व (IR) का Boogie मध्यवर्ती सत्यापन भाषा (IVL) में अनुवादक है। LLVM IR को स्रोत बनाने से कंपाइलर फ्रंट-एंड, अनुकूलन और विश्लेषणों की बढ़ती संख्या का लाभ उठाया जाता है। वर्तमान में SMACK केवल Clang कंपाइलर के माध्यम से C भाषा का समर्थन करता है, हालांकि हम अतिरिक्त भाषाओं के लिए समर्थन प्रदान करने पर काम कर रहे हैं। Boogie को लक्षित करने से एक विहित प्लेटफ़ॉर्म का लाभ उठाया जाता है जो सत्यापन, मॉडल जाँच और अमूर्त व्याख्या के लिए एल्गोरिदम के कार्यान्वयन को सरल बनाता है। वर्तमान में, SMACK Boogie और Corral सत्यापकों का लाभ उठाता है।

सिस्टम आवश्यकताओं, स्थापना, उपयोग और बाकी सब कुछ के लिए नीचे देखें।

हम SMACK का उपयोग करने के आपके अनुभव में बहुत रुचि रखते हैं। कृपया किसी भी संभावित प्रतिक्रिया के लिए Zvonimir, Michael, या Shaobo से संपर्क करें।

समर्थन

• सामान्य प्रश्नों के लिए, पहले FAQ देखें।

• यदि कुछ और टूटा हुआ या गायब है, तो एक मुद्दा खोलें।

• अंतिम उपाय के रूप में, Michael, Zvonimir, और Shaobo को मेल भेजें।

• अपडेट के बारे में सूचित रहने के लिए, आप SMACK के Github पृष्ठ को देख सकते हैं।

आभार

SMACK परियोजना को आंशिक रूप से राष्ट्रीय विज्ञान फाउंडेशन, VMware, Amazon, और Microsoft Research से वित्त पोषण द्वारा समर्थित किया गया है। हम SMACK के व्यापक बेंचमार्किंग के लिए यूनिवर्सिटी ऑफ यूटा के Emulab बुनियादी ढांचे पर भी निर्भर हैं।

विषयसूची

1. सिस्टम आवश्यकताएँ और स्थापना
2. SMACK चलाना
3. डेमो
4. सामान्य प्रश्न
5. इनलाइन बूगी कोड
6. योगदान दिशानिर्देश
7. परियोजनाएँ
8. प्रकाशन
9. लोग