Systematic API Testing Through Model Checking and Executable Contracts
यह शोध पत्र IcePick प्रस्तुत करता है, जो एक नया निष्पादन योग्य अनुबंध भाषा (executable contract language) जिसे Glacier कहा जाता है, के साथ TLA+ मॉडल चेकिंग को जोड़ता है ताकि व्यवस्थित रूप से स्टेटफुल API टेस्ट सीक्वेंस उत्पन्न किए जा सकें जो प्रमाणित व्यवहारिक कवरेज (provable behavioral coverage) प्राप्त करते हैं और पारंपरिक ब्लैक-बॉक्स परीक्षण की सीमाओं को दूर करते हैं।