Nous présentons Meta-F $$^{\star }$$ , un cadre de tactique et de métaprogrammation pour le vérificateur de programme F $ $ ^\star $ $. La principale nouveauté de Meta-F $ $^\star $$ est de permettre l'utilisation de tactiques et de métaprogrammation pour décharger des assertions non résolubles par SMT, ou simplement pour les simplifier en fragments SMT bien comportés. De plus, Meta-F $$^\star $$ peut être utilisé pour générer automatiquement du code vérifié. Meta-F $$^\star $$ est implémenté comme un effet F $$^\star $$, qui, compte tenu du système d'effet puissant de F $$^{\star }$$ , augmente fortement la réutilisation du code et permet même la vérification légère des métaprogrammes. Les métaprogrammes peuvent être interprétés ou compilés en un code natif efficace qui peut être chargé dynamiquement dans le vérificateur de type F $$^\star $$ et peut interagir avec le code interprété. L'évaluation d'études de cas réalistes montre que Meta-F $$^\star $$ offre des gains substantiels en développement de preuves, en efficacité et en robustesse.

Presentamos Meta-F $ $^{\star }$$ , un marco de tácticas y metaprogramación para el verificador del programa F $ $ ^\star $ $. La principal novedad de Meta-F $$^\Star $$ es permitir el uso de tácticas y metaprogramación para descargar afirmaciones no solucionables por SMT, o simplemente simplificarlas en fragmentos SMT de buen comportamiento. Además, Meta-F $$^\Star $$ se puede utilizar para generar código verificado automáticamente. Meta-F $$^\star $$ se implementa como un efecto F $$^\star $$, que, dado el potente sistema de efectos de F $$^{\star }$$ , aumenta en gran medida la reutilización de código e incluso permite la verificación ligera de metaprogramas. Los metaprogramas se pueden interpretar o compilar en código nativo eficiente que se puede cargar dinámicamente en el verificador de tipos F $$^\Star $$ y puede interoperar con el código interpretado. La evaluación de estudios de casos realistas muestra que Meta-F $$^\Star $$ proporciona ganancias sustanciales en el desarrollo, la eficiencia y la solidez de la prueba.

We introduce Meta-F $$^{\star }$$ , a tactics and metaprogramming framework for the F $$^\star $$ program verifier. The main novelty of Meta-F $$^\star $$ is allowing the use of tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F $$^\star $$ can be used to generate verified code automatically. Meta-F $$^\star $$ is implemented as an F $$^\star $$ effect, which, given the powerful effect system of F $$^{\star }$$ , heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F $$^\star $$ type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F $$^\star $$ provides substantial gains in proof development, efficiency, and robustness.

نقدم Meta -F $$^{\star }$$ ، وهو إطار تكتيكات وبرمجة metaprogramming لمحقق برنامج F $$^\ star $$. تتمثل الحداثة الرئيسية لـ Meta - F $$^\star $$ في السماح باستخدام التكتيكات والبرمجة الوصفية لتفريغ التأكيدات التي لا يمكن حلها بواسطة SMT، أو لتبسيطها فقط إلى أجزاء SMT حسنة السلوك. بالإضافة إلى ذلك، يمكن استخدام Meta - F $^\ star $$ لإنشاء رمز تم التحقق منه تلقائيًا. يتم تنفيذ Meta - F $$^\ star $$ كتأثير F $^\ star $$، والذي، بالنظر إلى نظام التأثير القوي لـ F $^{\ star }$$ ، يزيد بشكل كبير من إعادة استخدام الكود وحتى يمكّن من التحقق الخفيف من برامج metaprograms. يمكن تفسير البرامج الوصفية، أو تجميعها إلى رمز أصلي فعال يمكن تحميله ديناميكيًا في مدقق نوع F $^\star $$ ويمكن أن يعمل مع الرمز المفسر. يُظهر تقييم دراسات الحالة الواقعية أن Meta - F$$^\ star $$ يوفر مكاسب كبيرة في تطوير الدليل والكفاءة والمتانة.