אימות תוכנה – הבדלי גרסאות

ישנן שתי בעיות עיקריות באימות תוכנה. המעשית שבהן היא שאימות תוכנה דורש מיומנות רבה ורקע מתמטי ברמה גבוהה מהמקובל. הבעיה החמורה יותר היא שלא ניתן להוכיח קיום או שלילה של תכונה כלשהי על כל תוכנית שרירותית. דוגמה לכך היא ההוכחה כי אי אפשר לפתח [[תוכנית מחשב|תוכנית]] שיכולה לוודא האם תוכנית כלשהי תעצור כאשר תקבל קלט מסוים (בעיה זו ידועה כ[[בעיית העצירה]]). [[משפט רייס]] מוכיח כי לא ניתן לכתוב תוכנית שתוכל להכריע לגבי כל תוכנית שהיא האם היא מקיימת תכונה לא טריוויאלית (תוכנהתכונה שלא כל תוכנית בהכרח מקיימת) כלשהי.