-
wave equation numerical resolution: a comprehensive mechanized proof of a c program
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 902
- تعداد پرسش و پاسخ ها: 0
- شماره تماس دبیرخانه رویداد: -
we formally prove correct a c program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. we annotate this c program to specify both method error and round-off error. we use frama-c to generate theorems that guarantee the soundness of the code. we discharge these theorems using smt solvers, gappa, and coq. this involves a large coq development to prove the adequacy of the c program to the numerical scheme and to bound errors. to our knowledge, this is the first time such a numerical analysis program is fully machine-checked.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
بررسی رابطه ی ویروس پاپیلوم انسانی با سرطان سلول سنگفرشی در نمونه ی بیوپسی مری بیماران مراجعه کننده به بیمارستان ولی عصر زنجان، سال 82-1381
-
بررسی دیرینه شناسی و چینه شناسی سازند کلات در برش دریاچه بزنگان (کل بی بی)
-
بهینه سازی ابعادی دیوار برشی بتنی بوسیله الگوریتم ژنتیک
-
تحلیل عوامل موثر در پیدایش تعارض قوانین و رابطه آن با تعارض دادگاه ها
-
global compactness results for quasilinear elliptic problems with combined critical sobolev–hardy terms
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
ارائه الگوریتم جدید برای سری متوالی به منظور فشرده سازی آنها در فرآیند اکتشاف داده ها
-
بررسی مدارس و کلاس های هوشمند
-
بررسی فقهی و حقوقی آثار واگذاری حق طلاق
-
تاثیر شبکه های مجازی در راستای انحرافات و آسیب های اجتماعی نوجوانان
-
اثربخشی تئوری انتخاب بر وسواس فکری - عملی و نشخوار ذهنی در دوره بیماری کرونا ویروس در زنان خانه دار شهر همدان
سوال خود را در مورد این مقاله مطرح نمایید :