במערכות רבות קיימים קטעי קוד קצרים שתפקודם הנכון קריטי לפעולת המערכת. במידה ואין זה מעשי לשכתב קטעים אלו בשיטות פורמליות ניתן להשתמש בטכניקות של הוכחה פורמלית כדי לודא שהקוד מתנהג כמצופה. בחברת פרואקטיב מודלינג אנחנו משתמשים בכלי ההוכחה הפורמלית ACL2 כדי להוכיח טענות על קוד קיים בסביבה מצומצמת של ה-JVM. כלי זה נמצא בשימוש בין היתר בחברת AMD להוכחה פורמלית של האלגוריתמים הנומריים של מעבדי החברה. |
|
|
Verifying Critical Code |