อัลท์-เออร์โก
นักพัฒนา	โอแคมลโปร
เขียนเป็น	โอแคมล์
มีจำหน่ายใน	ภาษาอังกฤษ
พิมพ์	ตัวแก้ปัญหาทางคณิตศาสตร์, ตัวตรวจสอบโปรแกรม
เว็บไซต์	alt-ergo .ocamlpro .com
ที่เก็บข้อมูล	github.com/OCamlPro/alt-ergo​​​

Alt-Ergoซึ่งเป็นตัวแก้ปัญหาอัตโนมัติสำหรับสูตรทางคณิตศาสตร์ ส่วนใหญ่ใช้ในการตรวจสอบโปรแกรมอย่างเป็นทางการโดยทำงานบนหลักการของความสามารถในการทำให้เป็นจริงโมดูลทฤษฎี (SMT) การพัฒนาดำเนินการโดยนักวิจัยจากมหาวิทยาลัยปารีส-ซูด , Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France และCNRSตั้งแต่ปี 2013 บริษัท OCamlPro ได้ดำเนินการจัดการและกำกับดูแลโครงการ^{[ 1 ]}เผยแพร่ภายใต้ใบ อนุญาต ซอฟต์แวร์โอเพนซอร์สและฟรี CeCILL-C

Alt-Ergo ใช้ภาษาป้อนข้อมูลเฉพาะที่มีโพลีมอร์ฟิซึมแบบพรีเน็กซ์ซึ่งออกแบบมาเพื่อลดจำนวนสัจพจน์ที่ต้องมีการระบุปริมาณ และเพื่อลดความซับซ้อนของปัญหา แม้ว่า Alt-Ergo จะรองรับ ภาษา SMT-LIB 2 ได้บางส่วน แต่ประสิทธิภาพในการทำงานกับไฟล์ SMT นั้นค่อนข้างจำกัด

โครงสร้างหลักของ Alt-Ergo ประกอบด้วยองค์ประกอบหลักสามส่วน ได้แก่ตัวแก้ปัญหา SAT ที่ใช้ การค้นหาเชิงลึก (DFS) กลไกการสร้างอินสแตนซ์ของตัวบ่งปริมาณที่ใช้การจับคู่แบบ eและชุดของขั้นตอนการตัดสินใจสำหรับทฤษฎีต่างๆ ที่มีอยู่ภายใน องค์ประกอบเหล่านี้ร่วมกันทำให้ Alt-Ergo มีความสามารถในการแก้สูตรโดยอัตโนมัติ

Alt-Ergo นำเสนอขั้นตอนการตัดสินใจ (แบบกึ่งๆ) สำหรับทฤษฎีต่อไปนี้:

• ทฤษฎีที่ว่างเปล่า
• เลขคณิตจำนวนเต็มเชิงเส้น
• เลขคณิตเชิงตรรกะเชิงเส้น
• เลขคณิตไม่เชิงเส้น
• การคำนวณเลขทศนิยม
• อาร์เรย์ โพลีมอร์ฟิก
• ประเภทข้อมูลแบบแจงนับ
• สัญลักษณ์ AC
• ประเภทข้อมูลบันทึก

มีการสร้างแพลตฟอร์มการตรวจสอบหลายแพลตฟอร์มบน Alt-Ergo:

• Why3ซึ่งเป็นแพลตฟอร์มสำหรับการตรวจสอบโปรแกรมแบบนิรนัย ใช้ Alt-Ergo เป็นตัวพิสูจน์หลัก^{[ 2 ]}
• CAVEAT ซึ่งเป็นตัวตรวจสอบ C ที่พัฒนาโดย CEA และใช้งานโดย Airbus; Alt-Ergo ถูกรวมอยู่ในมาตรฐานการรับรอง DO-178C ของเครื่องบินลำหนึ่งของบริษัท
• Frama-Cซึ่งเป็นเฟรมเวิร์กสำหรับวิเคราะห์โค้ดภาษาซี ใช้ Alt-Ergo ในปลั๊กอิน Jessie และ WP (ซึ่งออกแบบมาเพื่อการตรวจสอบความถูกต้องของโปรแกรมแบบนิรนัย )
• SPARKใช้ Alt-Ergo (ซึ่งอยู่เบื้องหลัง GNATprove) เพื่อตรวจสอบความถูกต้องของข้อความยืนยันบางส่วนโดยอัตโนมัติใน Spark 2014
• Atelier-Bสามารถใช้ Alt-Ergo แทนโปรแกรมพิสูจน์หลัก (ซึ่งช่วยเพิ่มอัตราความสำเร็จจาก 84% เป็น 98% ในเกณฑ์มาตรฐานของโครงการ ANR Bware )
• Rodinซึ่งเป็นเฟรมเวิร์ก B-method ที่พัฒนาโดย Systerel สามารถใช้ Alt-Ergo เป็นแบ็กเอนด์ได้
• Cubicleคือโปรแกรมตรวจสอบแบบจำลองโอเพนซอร์สสำหรับตรวจสอบคุณสมบัติความปลอดภัยของระบบการเปลี่ยนสถานะแบบอาร์เรย์
• EasyCryptคือชุดเครื่องมือสำหรับใช้ในการให้เหตุผลเกี่ยวกับคุณสมบัติเชิงสัมพันธ์ของการคำนวณเชิงความน่าจะเป็นด้วยโค้ดที่เป็นอันตราย
• บแวร์^{[ 3 ]}
• คาเฟอีน^{[ 3 ]}
• FUI Hi-Lite ^{[ 3 ]}
• รับรอง^{[ 3 ]}
• ADT Alt-Ergo ^{[ 3 ]}
• A3PAT ^{[ 3 ]}

• การตรวจสอบอย่างเป็นทางการ
• เครื่องพิสูจน์ทฤษฎีบท Z3

• เว็บไซต์อย่างเป็นทางการ OcamlPro
• Alt-Ergo ที่ LRI

บทความซอฟต์แวร์ทางวิทยาศาสตร์นี้ ยัง ไม่สมบูรณ์คุณสามารถช่วยวิกิพีเดียได้โดยการเพิ่มข้อมูลที่ขาดหายไป

• วี
• ที
• อี

บทความเกี่ยวกับซอฟต์แวร์โอเพนซอร์สและใช้งานได้ฟรีนี้ ยังเป็น เพียงบทความย่อคุณสามารถช่วยวิกิพีเดียได้โดยการเพิ่มข้อมูลที่ขาดหายไป

• วี
• ที
• อี