چکيده
چكيده
نرم افزار در يك سيستم الكترونيكي اغلب بيشترين موضوع موردبحث باتوجه به كيفيت و جريان هاي طراحي است. ابزار تاييد رسمي
مي تواند تضمين نمايد كه طراحي بدون مشخصه هاي خاصي باشد. ما الگوريتم هايي را بررسي مي كنيم كه تحليل اتوماتيك،
استاتيك نرم افزار را براي تشخيص خطاهاي برنامه نويسي يا اثبات آن انجام مي دهند. سه تكنيكي كه ما درنظر گرفته ايم تحليل
استاتيك با دامنه هاي انتزاعي، بررسي مدل و بررسي مدل محدود است. ما آموزش كوتاهي در مورد اين تكنيك ها ارائه مي دهيم،
كه تفاوت هاي آنها را هنگام استفاده از مسائل عملي برجسته مي كند. ما همچنين ابزارهايي را مورد بررسي قرار داده ايم كه براي
اجراي اين تكنيك ها دردسترس هستند و نقاط قوت و ضعف آنها را توصيف مي كنيم.
