ใน สาขา วิทยาการคอมพิวเตอร์ ความถูกต้องของคอมไพเลอร์เป็นสาขาหนึ่งของวิทยาการคอมพิวเตอร์ที่เกี่ยวข้องกับการพยายามแสดงให้เห็นว่าคอมไพเลอร์ทำงานตามข้อกำหนดของภาษาเทคนิคต่างๆ ได้แก่ การพัฒนาคอมไพเลอร์โดยใช้วิธีการเชิงรูปธรรมและการใช้การทดสอบอย่างเข้มงวด (มักเรียกว่าการตรวจสอบความถูกต้องของคอมไพเลอร์) กับคอมไพเลอร์ที่มีอยู่แล้ว

แนวทาง การตรวจสอบความถูกต้องอย่างเป็นทางการหลักสองประการสำหรับการพิสูจน์ความถูกต้องของการคอมไพล์ ได้แก่ การพิสูจน์ความถูกต้องของคอมไพเลอร์สำหรับอินพุตทั้งหมด และการพิสูจน์ความถูกต้องของการคอมไพล์โปรแกรมเฉพาะ (การตรวจสอบความถูกต้องของการแปล)

การตรวจสอบความถูกต้องของคอมไพเลอร์ด้วยวิธีการเชิงรูปธรรมเกี่ยวข้องกับห่วงโซ่ตรรกะเชิงรูปธรรมแบบ นิรนัยที่ยาวนาน ^{[ 1 ]} อย่างไรก็ตาม เนื่องจากเครื่องมือในการค้นหาหลักฐาน ( ตัวพิสูจน์ทฤษฎีบท ) ถูกนำไปใช้ในซอฟต์แวร์และมีความซับซ้อน จึงมีความเป็นไปได้สูงที่จะมีข้อผิดพลาด แนวทางหนึ่งคือการใช้เครื่องมือที่ตรวจสอบหลักฐาน ( ตัวตรวจสอบหลักฐาน ) ซึ่งเนื่องจากมีความเรียบง่ายกว่าตัวค้นหาหลักฐานมาก จึงมีโอกาสน้อยที่จะมีข้อผิดพลาด

ตัวอย่างที่โดดเด่นของแนวทางนี้คือCompCertซึ่งเป็นคอมไพเลอร์ที่ตรวจสอบอย่างเป็นทางการซึ่งเพิ่มประสิทธิภาพของชุดย่อยขนาดใหญ่ของC99 ^{[ 2 ] [ 3 ] [ 4 ]}

คอมไพเลอร์ที่ได้รับการตรวจสอบอีกตัวหนึ่งได้รับการพัฒนาในโครงการ CakeML ^{[ 5 ]}ซึ่งสร้างความถูกต้องของชุดย่อยที่สำคัญของภาษาการเขียนโปรแกรมML มาตรฐาน โดยใช้ ตัวช่วยพิสูจน์ HOL

แนวทางอื่นในการสร้างคอมไพเลอร์ที่ถูกต้องอย่างเป็นทางการคือการใช้การสร้างคอมไพเลอร์ที่กำกับโดยความหมาย^{[ 6 ]}

ตรงกันข้ามกับการพยายามพิสูจน์ว่าคอมไพเลอร์ถูกต้องสำหรับโปรแกรมอินพุตที่ถูกต้องทั้งหมด การตรวจสอบความถูกต้องของการแปล^{[ 7 ]}มีเป้าหมายเพื่อสร้างความแน่นอนโดยอัตโนมัติว่าโปรแกรมอินพุตที่กำหนดนั้นคอมไพล์ได้อย่างถูกต้อง การพิสูจน์การคอมไพล์ที่ถูกต้องของโปรแกรมที่กำหนดนั้นอาจง่ายกว่าการพิสูจน์ว่าคอมไพเลอร์ถูกต้องสำหรับทุกโปรแกรม แต่ยังคงต้องใช้การให้เหตุผลเชิงสัญลักษณ์ เนื่องจากโปรแกรมที่กำหนดไว้อาจยังคงทำงานได้กับอินพุตขนาดใหญ่ตามอำเภอใจและทำงานได้นานตามอำเภอใจ การตรวจสอบความถูกต้องของการแปลสามารถนำการใช้งานคอมไพเลอร์ที่มีอยู่มาใช้ซ้ำได้โดยการสร้างหลักฐานว่าการคอมไพล์นั้นถูกต้องสำหรับการคอมไพล์ที่กำหนด การตรวจสอบความถูกต้องของการแปลสามารถใช้ได้แม้กับคอมไพเลอร์ที่บางครั้งสร้างโค้ดที่ไม่ถูกต้อง ตราบใดที่ความไม่ถูกต้องนี้ไม่ปรากฏให้เห็นสำหรับโปรแกรมที่กำหนด ขึ้นอยู่กับโปรแกรมอินพุต การตรวจสอบความถูกต้องของการแปลอาจล้มเหลว (เนื่องจากโค้ดที่สร้างขึ้นนั้นผิดหรือเทคนิคการตรวจสอบความถูกต้องของการแปลอ่อนแอเกินไปที่จะแสดงความถูกต้อง) อย่างไรก็ตาม หากการตรวจสอบความถูกต้องของการแปลสำเร็จ โปรแกรมที่คอมไพล์แล้วจะรับประกันได้ว่าถูกต้องสำหรับอินพุตทั้งหมด

การทดสอบถือเป็นส่วนสำคัญของความพยายามในการจัดส่งคอมไพเลอร์ แต่ได้รับการกล่าวถึงค่อนข้างน้อยในเอกสารมาตรฐาน ฉบับปี 1986 ของ Aho, Sethi, & Ullman's Compilers: Principles, Techniques and Toolsมีส่วนเกี่ยวกับการทดสอบคอมไพเลอร์เพียงหน้าเดียว โดยไม่มีตัวอย่างที่ระบุชื่อ^{[ 8 ]} ฉบับปี 2006 ละเว้นส่วนเกี่ยวกับการทดสอบ แต่เน้นย้ำถึงความสำคัญของมันว่า “คอมไพเลอร์ที่ปรับแต่งประสิทธิภาพนั้นยากที่จะทำให้ถูกต้องมากจนเรากล้าพูดได้ว่าไม่มีคอมไพเลอร์ที่ปรับแต่งประสิทธิภาพใดที่ปราศจากข้อผิดพลาดโดยสิ้นเชิง! ดังนั้นวัตถุประสงค์ที่สำคัญที่สุดในการเขียนคอมไพเลอร์คือความถูกต้อง” ^{[ 9 ]} Fraser & Hanson 1995 มีส่วนสั้นๆ เกี่ยวกับการทดสอบการถดถอยมีซอร์สโค้ดให้ใช้งานได้^{[ 10 ]} Bailey & Davidson 2003 ครอบคลุมการทดสอบการเรียกใช้ขั้นตอน^{[ 11 ]} บทความจำนวนมากยืนยันว่าคอมไพเลอร์ที่เผยแพร่หลายตัวมีข้อบกพร่องด้านความถูกต้องของโค้ดที่สำคัญ^{[ 12 ]} Sheridan 2007 น่าจะเป็นบทความวารสารล่าสุดเกี่ยวกับการทดสอบคอมไพเลอร์ทั่วไป^{[ 13 ]}สำหรับวัตถุประสงค์ส่วนใหญ่ ข้อมูลส่วนใหญ่ที่มีอยู่เกี่ยวกับการทดสอบคอมไพเลอร์คือชุดการตรวจสอบ Fortran ^{[ 14 ]}และ Cobol ^{[ 15 ]}

เทคนิคทั่วไปเพิ่มเติมในการทดสอบคอมไพเลอร์ ได้แก่การฟัซซิ่ง^{[ 16 ]} (ซึ่งสร้างโปรแกรมแบบสุ่มเพื่อพยายามค้นหาข้อบกพร่องในคอมไพเลอร์) และการลดกรณีทดสอบ (ซึ่งพยายามลดกรณีทดสอบที่พบเพื่อให้เข้าใจได้ง่ายขึ้น) ^{[ 17 ]}

• การตรวจสอบและยืนยันความถูกต้อง (ซอฟต์แวร์)
• ข้อคิดเกี่ยวกับการไว้วางใจ