Libdmc ^{[ 1 ] [ 2 ]}เป็นไลบรารีที่ออกแบบในห้องปฏิบัติการ LIP6 ^{[ 3 ]}โดยมีเป้าหมายเพื่ออำนวยความสะดวกในการแจกจ่ายตัวตรวจสอบแบบจำลอง ที่มีอยู่ นอกจากนี้ยังได้รับการออกแบบให้มีอินเทอร์เฟซทั่วไปมากที่สุดโดยไม่ลดทอนประสิทธิภาพด้วยภาษา C++

การตรวจสอบแบบจำลอง (Model checking)เป็นวิธีการอัตโนมัติในการพิสูจน์ว่าพฤติกรรมของระบบที่จำลองขึ้นนั้นถูกต้อง โดยการตรวจสอบคุณสมบัติ อย่างไรก็ตาม วิธีนี้ประสบปัญหาที่เรียกว่า ปัญหาการระเบิดของปริภูมิสถานะ ( state space explosion problem) ซึ่งเกิดจากการใช้หน่วยความจำอย่างมาก มีการเสนอแนวทางแก้ไขมากมายเพื่อเอาชนะปัญหานี้ (เช่น การแสดงผลเชิงสัญลักษณ์ด้วยแผนภาพการตัดสินใจ - เช่นBDD ) แต่แนวทางเหล่านี้อาจนำไปสู่การใช้เวลามากเกินไปอย่างรวดเร็ว

การตรวจสอบแบบจำลองแบบกระจาย (Distributed model checking) เป็นวิธีหนึ่งในการเอาชนะปัญหาการใช้หน่วยความจำและเวลามากเกินไป โดยใช้ทรัพยากรที่รวมกันของคลัสเตอร์เฉพาะ อย่างไรก็ตาม การเขียนโปรแกรมตรวจสอบแบบจำลองใหม่ทั้งหมดเป็นงานที่ยาก ดังนั้นแนวทางของ libdmc คือการจัดเตรียมกรอบการทำงานเพื่อใช้ในการสร้างโปรแกรมตรวจสอบแบบจำลอง