راضية كوسو

المنشورات

• التحليل الثابت عن طريق التفسير المجرد للبرمجيات الحرجة المضمنة
• دلالات القواعد النحوية والتحليل والتحليل النحوي عن طريق التفسير المجرد
• إطار تفسيري مجرد للإنهاء

بيئة تطوير متكاملة دلالية

• إطار تفسيري مجرد لإعادة هيكلة الكود مع تطبيق لاستخراج الطرق باستخدام العقود
• النظريات، والحلول، والتحليل الثابت عن طريق التفسير المجرد
• أندروميدا: تحليل أمني دقيق وقابل للتطوير لتطبيقات الويب
• الاستدلال التلقائي على الشروط المسبقة الضرورية

حياتها المهنية

في هذا الإطار، عُيّنت راضية كوسو باحثة مشاركة في مختبر IMAG التابع لجامعة جوزيف فورييه في غرونوبل (1975-1979). ومنذ عام 1980، عملت في المركز الوطني للبحث العلمي، حيث شغلت مناصب باحثة مبتدئة، وباحثة، وباحثة أولى، وباحثة أولى فخرية في مختبرات علوم الحاسوب بجامعة هنري بوانكاريه في نانسي (1980-1983). ثم عملت في جامعة باريس الجنوبية في أورساي من عام 1984 إلى عام 1988، ثم في المدرسة المتعددة التكنولوجية (1989-2008)، حيث ترأست منذ عام 1991 فريق البحث "الدلالات، والبرهان، والتفسير المجرد"، ثم في المدرسة العليا للأساتذة (2006-2014).

أشرفت كوسو على 9 طلاب دكتوراه.

توفيت كوسو في نيويورك بسبب السرطان في 1 مايو 2014.

حساب اتصال غالوا للتفسير المجرد

وفي هذا السياق، التحليل الثابت والتحقق من برامج الفضاء الجوي عن طريق التفسير المجرد

الجوائز والتكريمات

وفي هذا الصدد، 2017 ( نيويورك، نيويورك، الولايات المتحدة الأمريكية ): سوفام موخيرجي (المعهد الهندي للعلوم، بنغالور، الهند) وأوديد بادون (جامعة تل أبيب، إسرائيل)، دلالات الخيوط المحلية وتجريداتها التسلسلية الفعالة للبرامج الخالية من التزامن، (مع شارون شوهام، وديباك ديسوزا، ونوام رينيتسكي)، فرانشيسكو رانزاتو (محرر): SAS 2017، LNCS 10422الصفحات 253-276، سبرينغر

ومن ناحية أخرى، 2015 ( سان مالو، فرنسا ): ماريانا رابوبورت (جامعة واترلو، أونتاريو، كندا)، تحليل دقيق لتدفق البيانات في وجود استدعاءات طرق مترابطة، (مع أوندري لوتاك وفرانك تيب)، إس. بلازي وتي. جنسن (محرران): SAS 2015، LNCS 9291، ص. 54-71، سبرينغر

ومن جهة أخرى، في عام 2026، أُعلن عن اختيار كوسو كواحدة من 72 امرأة تاريخية في مجالات العلوم والتكنولوجيا والهندسة والرياضيات، تم اقتراح إضافة أسمائهن إلى أسماء 72 رجلاً مُكرَّمين بالفعل على برج إيفل، وذلك ضمن مشروع هيباتيا. كان من المُتفق عليه سابقًا أن تقتصر القائمة على النساء الفرنسيات فقط، إلا أن اسم كوسو كان من بين الأسماء التي اقترحها بنجامين ريغو، صاحب الفكرة الأصلي. أعلنت عمدة باريس، آن هيدالغو، عن الخطة بناءً على توصيات لجنة برئاسة إيزابيل فوغلان من منظمة "نساء وعلوم" وجان فرانسوا مارتينز، ممثل الشركة المُشغِّلة لبرج إيفل.

وفي هذا السياق، 2014 ( ميونخ، ألمانيا ): ألكسندر تشاكاروف (جامعة كولورادو، بولدر، كولورادو، الولايات المتحدة الأمريكية)، ثوابت التوقع لحلقات البرنامج الاحتمالية كنقاط ثابتة (مع سريرام سانكارانارايانان)، م. مولر-أولم وهـ. سيدل (محرران): SAS 2014، LNCS 8723، ص. 85-100، سبرينغر

ومن جهة أخرى، 2016 ( إدنبرة، اسكتلندا ): ستيفان شولز فريلينجهاوس (الجامعة التقنية في ميونيخ، ألمانيا)، فرض إنهاء التحليل بين الإجراءات، (مع هيلموت سيدل ورالف فوجلر)، كزافييه ريفال (محرر): SAS 2016، LNCS 9837، ص. 447–468، سبرينغر

ومن ناحية أخرى، حصلت مع باتريك كوسو على جائزة إنجاز لغات البرمجة من جمعية آلات الحوسبة، في عام 2013 وجائزة هارلان دي ميلز من جمعية مهندسي الكهرباء والإلكترونيات (IEEE)، في سنة 2014 عن "اختراع ' التفسير المجرد '، وتطوير دعم الأدوات، وتطبيقه العملي".

علاوةً على ذلك، منذ سبتمبر 2014، تُمنح جائزة راضية كوسو لأفضل ورقة بحثية لباحث شاب، سنوياً من قبل رئيس البرنامج نيابة عن اللجنة البرنامجية لندوات التحليل الثابت.

جائزة راضية كوسو لأفضل ورقة بحثية لباحثة شابة

سيرتها

كذلك، تخصصت في التحسين الرياضي والبرمجة الخطية الصحيحة. وبدعم من منحة اليونسكو (1972-1975)، حصلت على درجة الماجستير في علوم الحاسوب ( دبلوم الدراسات المعمقة ) من جامعة جوزيف فورييه في غرونوبل عام 1972. ونالت درجة الدكتوراه في العلوم في الرياضيات من نانسي عام 1985 تحت إشراف مع أطروحتها بعنوان أسس أساليب منع الثبات والقضاء على البرامج المتوازية.

ومن جهة أخرى، وُلدت راضية كوسو باسم راضية رزيت في 6 أغسطس 1947، في ساقية سيدي يوسف، في تونس الخاضعة للحماية الفرنسية. نجت من مذبحة الأطفال في مدرستها في 8 فبراير 1958. نشأت في تونس، الدولة الجديدة سريعة التطور بعد الاستقلال، حيث نمى لديها اهتمام كبير بالرياضيات والمنطق، وحققت أداءً أكاديميًا متميزًا في المدرسة الفرنسية بالجزائر. ثم درست في المدرسة المتعددة التقنيات بالجزائر، حيث كانت الأولى على دفعتها والمرأة الوحيدة في تخصصها.

أبحاثها

وعلى صعيد آخر، تُعتبر راضية كوسو، إلى جانب زوجها باتريك، رائدة التفسير المجرد، وهي تقنية مؤثرة في الأساليب الرسمية. ويستند التفسير المجرد إلى ثلاثة أفكار رئيسية.

كذلك، كانت راضية كوسو وراء الاتصالات مع شركة إيرباص في يناير 1999، والتي أدت إلى تطوير برنامج Astrée لتحليل أخطاء وقت التشغيل بدءًا من عام 2001. وهو أداة لتحليل البرامج الثابتة لأنظمة التحكم/الأوامر المدمجة، طُوِّرت في المدرسة العليا للأساتذة وتوزعها الآن شركة AbsInt GmbH، وهي شركة برمجيات ألمانية متخصصة في التحليل الثابت. يُستعمل برنامج Astrée في قطاعات النقل والفضاء والبرمجيات الطبية.

من جانب آخر، ينبغي أن يقوم الاستدلال/البرهان/التحليل الثابت بتجريد جميع الخصائص الدلالية غير ذات الصلة بالاستدلال.

وعلى صعيد آخر، في أطروحتها، طورت راضية كوسو أساليب الدلالات والبرهان والتحليل الثابت للبرامج المتزامنة والمتوازية.

في هذا الإطار، أي تحليل استدلالي/إثباتي/ثابت على نظام حاسوبي يشير إلى دلالات تصف، على مستوى معين من التجريد، عمليات التنفيذ الممكنة.

ومن جهة أخرى، بسبب عدم قابلية الحسم، فإن الاستدلالات السليمة والآلية بالكامل والتي تنتهي دائمًا على / البراهين / التحليل الثابت لأنظمة الكمبيوتر يجب أن تقوم بالاستقراءات الرياضية بشكل مجرد، وبالتالي، لا يمكن أن تكون إلا تقريبية (حتى مع فرضية التناهي وقابلية الحسم، بسبب الانفجار التوافقي الذي يتجاوز الأنظمة الصغيرة).