Published January 1, 2023 | Version v1
Publication Open

Incremental Rewriting Modulo SMT

Creators

  • 1. Philadelphia University
  • 2. Universidade Federal da Paraíba
  • 3. SRI International
  • 4. Menlo School

Description

Abstract Rewriting Modulo SMT combines two powerful automated deduction techniques (1) rewriting and (2) SMT-solving. Rewriting enables the specification of behavior of systems using rewriting rules, while SMT theories specify system properties. Rewriting Modulo SMT is enabled by combining existing tools, such as Maude and SMT solvers. Search algorithms used for carrying out Rewriting Modulo SMT, however, cannot exploit the incremental solving features available in SMT solvers as they are based on breadth-first search. This paper addresses this limitation by proposing Incremental Rewriting Modulo SMT Theories, which is a syntactical restriction to rewriting rules. This restriction turns out to naturally be used in several applications of Rewriting Modulo SMT, including the verification of algorithms, cyber-physical systems, and security protocols. Moreover, we propose a Hybrid-Search algorithm for Incremental Rewriting Modulo SMT Theories that combines breadth-first search and depth-first search, thus enabling incremental SMT-solving. We demonstrate through a collection of existing benchmarks that the Hybrid-Search algorithm can achieve a 10 times performance improvement in verification times.

⚠️ This is an automatic machine translation with an accuracy of 90-95%

Translated Description (Arabic)

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

Translated Description (French)

Abstract Rewriting Modulo SMT combine deux puissantes techniques de déduction automatisée (1) réécriture et (2) résolution SMT. La réécriture permet de spécifier le comportement des systèmes à l'aide de règles de réécriture, tandis que les théories SMT spécifient les propriétés du système. La réécriture de Modulo SMT est activée en combinant des outils existants, tels que les solveurs Maude et SMT. Les algorithmes de recherche utilisés pour effectuer la réécriture Modulo SMT, cependant, ne peuvent pas exploiter les fonctionnalités de résolution incrémentielle disponibles dans les solveurs SMT car ils sont basés sur la recherche de largeur en premier. Cet article aborde cette limitation en proposant des théories SMT du module de réécriture incrémentielle, qui est une restriction syntaxique aux règles de réécriture. Cette restriction s'avère être naturellement utilisée dans plusieurs applications de Rewriting Modulo SMT, y compris la vérification des algorithmes, des systèmes cyber-physiques et des protocoles de sécurité. De plus, nous proposons un algorithme de recherche hybride pour les théories SMT du module de réécriture incrémentielle qui combine la recherche en largeur et la recherche en profondeur, permettant ainsi une résolution SMT incrémentielle. Nous démontrons à travers une collection de benchmarks existants que l'algorithme Hybrid-Search peut atteindre une amélioration de performance 10 fois supérieure dans les temps de vérification.

Translated Description (Spanish)

El módulo SMT de reescritura de resúmenes combina dos potentes técnicas de deducción automatizada (1) reescritura y (2) resolución de SMT. La reescritura permite la especificación del comportamiento de los sistemas utilizando reglas de reescritura, mientras que las teorías SMT especifican las propiedades del sistema. La reescritura del módulo SMT se habilita combinando las herramientas existentes, como Maude y los solucionadores SMT. Sin embargo, los algoritmos de búsqueda utilizados para llevar a cabo la Reescritura del Módulo SMT no pueden explotar las funciones de resolución incremental disponibles en los solucionadores SMT, ya que se basan en la búsqueda por amplitud. Este artículo aborda esta limitación proponiendo Teorías SMT del Módulo de Reescritura Incremental, que es una restricción sintáctica a las reglas de reescritura. Esta restricción resulta ser utilizada naturalmente en varias aplicaciones de Rewriting Modulo SMT, incluida la verificación de algoritmos, sistemas ciberfísicos y protocolos de seguridad. Además, proponemos un algoritmo de búsqueda híbrida para las teorías SMT del módulo de reescritura incremental que combina la búsqueda de amplitud primero y la búsqueda de profundidad primero, lo que permite la resolución SMT incremental. Demostramos a través de una colección de puntos de referencia existentes que el algoritmo de búsqueda híbrida puede lograr una mejora de rendimiento de 10 veces en los tiempos de verificación.

Files

978-3-031-38499-8_32.pdf.pdf

Files (931.4 kB)

⚠️ Please wait a few minutes before your translated files are ready ⚠️ Note: Some files might be protected thus translations might not work.
Name Size Download all
md5:f6ac3c20fad5e4ef6184550566e36826
931.4 kB
Preview Download

Additional details

Additional titles

Translated title (Arabic)
إعادة الكتابة التدريجية لوحدة SMT
Translated title (French)
Module de réécriture incrémentielle SMT
Translated title (Spanish)
Reescritura incremental Módulo SMT

Identifiers

Other
https://openalex.org/W4386363566
DOI
10.1007/978-3-031-38499-8_32

Is supplement to
https://openalex.org/W4312716460 (Other)
https://openalex.org/W4206221271 (Other)
https://openalex.org/W3172487478 (Other)
https://openalex.org/W2504157767 (Other)
https://openalex.org/W2491573813 (Other)
https://openalex.org/W2475418661 (Other)
https://openalex.org/W2463026518 (Other)
https://openalex.org/W1761458962 (Other)
https://openalex.org/W1515515243 (Other)
https://openalex.org/W1504820687 (Other)

GreSIS Basics Section

Is Global South Knowledge
Yes
Country
Brazil

References

  • https://openalex.org/W1480909796
  • https://openalex.org/W1483514239
  • https://openalex.org/W1976195354
  • https://openalex.org/W2052524124
  • https://openalex.org/W2150470619
  • https://openalex.org/W2531460317
  • https://openalex.org/W2927889296
  • https://openalex.org/W3128588605
  • https://openalex.org/W338608548
  • https://openalex.org/W4234315090
  • https://openalex.org/W4288768859
  • https://openalex.org/W4288768903
  • https://openalex.org/W4386363566