ورود هندسه جبری به مهندسی کامپیوتر/ ابزاری برای درستی‌سنجی کدها

امیر کفشدار‌گوهرشادی رتبه اول پژوهش‌های بنیادی گروه علوم پایه در بیستمین جشنواره جوان خوارزمی برای طرح تحلیل استاتیک برنامه‌ها با استفاده از هندسه جبری و نظریه احتمال در گفتگو با خبرنگار حوزه‌ علم و فناوری گروه دانشگاه خبرگزاری آنا گفت: طرح من در زمینه درستی‌سنجی نرم‌افزارها در هندسه جبری است. این امر از این نظر مهم است که هر چه کدنویسی یک برنامه طولانی‌تر شود، امکان چک کردن آن برای برنامه‌نویس سخت‌تر می‌شود و درصد احتمال وقوع خطا بالاتر می‌رود. در کدنویسی ماهواره‌ها و خودروهای خودکار که چند هزار کد دارند، برنامه‌نویس نمی‌تواند تمام کدها را برای پیدا کردن خطا چک کند.

وی افزود: وجود کوچک‌ترین خطا در کدها  باعث می‌شود که کل سیستم از کار بیفتد. برای مثال در 96 موشک آرین 5 که قرار بود ماهواره اتحادیه اروپا را به فضا ببرد، 40 ثانیه پس از کار منفجر شد که علت آن خطای برنامه‌نویسی بود. در این پروژه الگوریتم‌های جدید و بهتری برای اثبات درستی برنامه‌ها از طریق سورس کد آنها ارائه دادیم. این الگوریتم‌ها با استفاده از هندسه جبری و نظریه احتمال ایجاد شده‌اند. در این پروژه اولین کاربرد هندسه جبری در مهندسی کامپیوتر را نیز به دست آوردیم که بسیار مهم است.

گوهرشادی که در حال حاضر دانشجوی دکتری علوم کامپیوتر در انستیتوی علم و فناوری اتریش است، گفت: این طرح جزئی از پروژه دکتری من است که توسعه آن حدود سه سال طول کشید. مؤسسات مختلفی در این طرح همکاری داشتند که شامل انستیتوی دانش و فناوری اتریش، مرکز مطالعات پیشرفته نرم‌افزار مادرید، بخش تحقیقات شرکت آی‌بی‌ام و آکادمی علوم اتریش می‌شود. این طرح همچنین چند گرنت برد از جمله بورسیه دکتری شرکت آی‌بی‌ام و گرنت علوم کامپیوتر انجمن ریاضی لندن و بورسیه دکتری آکادمی اتریش.

وی درباره تجاری‌‎سازی این طرح گفت: در حال حاضر از نتایج این طرح در نرم‌افزارهای آی‌بی‌ام و شرکت‌های دیگر استفاده می‌شود. به جرأت می‌توان گفت که این طرح همین حالا هم تجاری‌سازی شده است، زیرا برای اثبات درستی نرم‌افزارهای فعلی از نرم‌افزار من استفاده می‌کنند. در شاخه درستی‌سنجی نرم‌افزار به‌محض اثبات تئوری، به‌سرعت وارد کار می‌شود، چراکه ابزارها در این زمینه کم و نیاز بسیار زیاد است.

انتهای پیام/4021/