Lógica de separación

En informática , la lógica de separación ^[1] es una extensión de la lógica de Hoare , una forma de razonar sobre los programas. Fue desarrollada por John C. Reynolds , Peter O'Hearn , Samin Ishtiaq y Hongseok Yang, ^{[1] [2] [3] [4]} basándose en los primeros trabajos de Rod Burstall . ^[5] El lenguaje de aserción de la lógica de separación es un caso especial de la lógica de implicaciones agrupadas (BI). ^[6] Un artículo de revisión de CACM de O'Hearn traza los desarrollos en el tema hasta principios de 2019. ^[7]

Descripción general

La lógica de separación facilita el razonamiento sobre:

• programas que manipulan estructuras de datos de punteros, incluida información oculta en presencia de punteros;
• "transferencia de propiedad" (evitación de axiomas del marco semántico ); y
• separación virtual (razonamiento modular) entre módulos concurrentes.

La lógica de separación respalda el campo de investigación en desarrollo descrito por Peter O'Hearn y otros como razonamiento local , según el cual las especificaciones y pruebas de un componente de programa mencionan solo la parte de memoria utilizada por el componente y no el estado global completo del sistema. Las aplicaciones incluyen la verificación automatizada de programas (donde un algoritmo verifica la validez de otro algoritmo) y la paralelización automatizada de software.

Afirmaciones: operadores y semántica

Las afirmaciones de lógica de separación describen "estados" que consisten en un almacén y un montón , que corresponden aproximadamente al estado de las variables locales (o asignadas por pila ) y los objetos asignados dinámicamente en lenguajes de programación comunes como C y Java . Un almacén es una función que asigna variables a valores. Un montón es una función parcial que asigna direcciones de memoria a valores. Dos montones y son disjuntos (denotados como ) si sus dominios no se superponen (es decir, para cada dirección de memoria , al menos uno de y no está definido). ${\displaystyle s}$ ${\displaystyle h}$ ${\displaystyle h}$ ${\displaystyle h'}$ ${\displaystyle h\,\bot \,h'}$ ${\displaystyle \ell }$ ${\displaystyle h(\ell )}$ ${\displaystyle h'(\ell )}$

La lógica permite probar juicios de la forma , donde es un almacén, es un montón y es una afirmación sobre el almacén y el montón dados. Las afirmaciones de lógica de separación (denotadas como , , ) contienen los conectores booleanos estándar y, además, , , , y , donde y son expresiones. ${\displaystyle s,h\models P}$ ${\displaystyle s}$ ${\displaystyle h}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle R}$ ${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$ ${\displaystyle e\mapsto e'}$ ${\displaystyle P\ast Q}$ ${\displaystyle P{-\!\!\ast }\,Q}$ ${\displaystyle e}$ ${\displaystyle e'}$

• La constante afirma que el montón está vacío , es decir, cuando no está definido para todas las direcciones. ${\displaystyle \mathbf {e} \mathbf {m} \mathbf {p} }$ ${\displaystyle s,h\models \mathbf {e} \mathbf {m} \mathbf {p} }$ ${\displaystyle h}$
• El operador binario toma una dirección y un valor y afirma que el montón está definido exactamente en una ubicación, asignando la dirección dada al valor dado. Es decir, cuando (donde denota el valor de la expresión evaluada en la tienda ) y de lo contrario no está definido. ${\displaystyle \mapsto }$ ${\displaystyle s,h\models e\mapsto e'}$ ${\displaystyle h([\![e]\!]_{s})=[\![e']\!]_{s}}$ ${\displaystyle [\![e]\!]_{s}}$ ${\displaystyle e}$ ${\displaystyle s}$ ${\displaystyle h}$
• El operador binario (pronunciado asterisco o conjunción separadora ) afirma que el montón se puede dividir en dos partes disjuntas donde sus dos argumentos se cumplen, respectivamente. Es decir, cuando existen tales que y y y . ${\displaystyle \ast }$ ${\displaystyle s,h\models P\ast Q}$ ${\displaystyle h_{1},h_{2}}$ ${\displaystyle h_{1}\,\bot \,h_{2}}$ ${\displaystyle h=h_{1}\cup h_{2}}$ ${\displaystyle s,h_{1}\models P}$ ${\displaystyle s,h_{2}\models Q}$
• El operador binario (pronunciado varita mágica o implicación separadora ) afirma que extender el montón con una parte disjunta que satisface su primer argumento da como resultado un montón que satisface su segundo argumento. Es decir, cuando para cada montón tal que , también se cumple. ${\displaystyle -\!\!\ast }$ ${\displaystyle s,h\models P-\!\!\ast \,Q}$ ${\displaystyle h'\,\bot \,h}$ ${\displaystyle s,h'\models P}$ ${\displaystyle s,h\cup h'\models Q}$

Los operadores y comparten algunas propiedades con los operadores de conjunción e implicación clásicos . Se pueden combinar utilizando una regla de inferencia similar al modus ponens ${\displaystyle \ast }$ ${\displaystyle -\!\!\ast }$

${\displaystyle {\frac {s,h\models P\ast (P-\!\!\ast \,Q)}{s,h\models Q}}}$

y forman una adjunción , es decir, si y sólo si para ; más precisamente, los operadores adjuntos son y . ${\displaystyle s,h\cup h'\models P\ast Q\Rightarrow R}$ ${\displaystyle s,h\models P\Rightarrow Q-\!\!\ast \,R}$ ${\displaystyle h\,\bot \,h'}$ ${\displaystyle \_\ast Q}$ ${\displaystyle Q-\!\!\ast \,\_}$

Razonamiento sobre programas: triples y reglas de demostración

En la lógica de separación, los triples de Hoare tienen un significado ligeramente diferente al de la lógica de Hoare . El triple afirma que si el programa se ejecuta desde un estado inicial que satisface la condición previa , entonces el programa no se equivocará (por ejemplo, no tendrá un comportamiento indefinido) y, si termina, entonces el estado final satisfará la condición posterior . En esencia, durante su ejecución, puede acceder solo a las ubicaciones de memoria cuya existencia se afirma en la condición previa o que han sido asignadas por él mismo. ${\displaystyle \{P\}\ C\ \{Q\}}$ ${\displaystyle C}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle C}$ ${\displaystyle C}$

Además de las reglas estándar de la lógica de Hoare , la lógica de separación admite la siguiente regla muy importante:

${\displaystyle {\frac {\{P\}\ C\ \{Q\}}{\{P\ast R\}\ C\ \{Q\ast R\}}}~{\mathsf {mod}}(C)\cap {\mathsf {fv}}(R)=\emptyset }$

Esto se conoce como la regla del marco (nombrada así por el problema del marco ) y permite el razonamiento local. Dice que un programa que se ejecuta de forma segura en un estado pequeño (satisfaciendo ) , también puede ejecutarse en cualquier estado más grande (satisfaciendo ) y que su ejecución no afectará la parte adicional del estado (y por lo tanto seguirá siendo verdadera en la poscondición). La condición secundaria refuerza esto al especificar que ninguna de las variables modificadas por ocurre libre en , es decir, ninguna de ellas está en el conjunto de 'variables libres' de . ${\displaystyle P}$ ${\displaystyle P\ast R}$ ${\displaystyle R}$ ${\displaystyle C}$ ${\displaystyle R}$ ${\displaystyle {\mathsf {fv}}}$ ${\displaystyle R}$

Intercambio

La lógica de separación permite realizar demostraciones sencillas de manipulación de punteros para estructuras de datos que presentan patrones de compartición regulares que pueden describirse simplemente mediante conjunciones separadoras; por ejemplo, listas enlazadas simple y doblemente y variedades de árboles. Los gráficos, los DAG y otras estructuras de datos con una compartición más general son más difíciles de demostrar, tanto formal como informalmente. No obstante, la lógica de separación se ha aplicado con éxito al razonamiento sobre programas con una compartición general.

En su artículo POPL'01, ^[3] O'Hearn e Ishtiaq explicaron cómo el conector de la varita mágica podría usarse para razonar en presencia de compartir, al menos en principio. Por ejemplo, en el triple ${\displaystyle {-\!\!*}}$

${\displaystyle \{(x\mapsto -)\ast ((x\mapsto 42){-\!\!*}P)\}\ [x]=42\ \{P\}}$

obtenemos la precondición más débil para una declaración que muta el montón en la ubicación , y esto funciona para cualquier postcondición, no solo una que se presenta ordenadamente usando la conjunción separadora. Esta idea fue llevada mucho más allá por Yang, quien solía proporcionar razonamiento localizado sobre mutaciones en el algoritmo clásico de marcado de grafos de Schorr-Waite. ^[8] Finalmente, uno de los trabajos más recientes en esta dirección es el de Hobor y Villard, ^[9] quienes emplean no solo sino también un conectivo que ha sido llamado de diversas maneras conjunción superpuesta o sepish, ^[10] y que puede usarse para describir estructuras de datos superpuestas: se cumple de un montón cuando y se cumple para submontones y cuya unión es , pero que posiblemente tienen una porción no vacía en común. De manera abstracta, puede verse como una versión del conectivo de fusión de la lógica de relevancia . ${\displaystyle x}$ ${\displaystyle {-\!\!*}}$ ${\displaystyle {-\!\!*}}$ ${\displaystyle \cup \,\!\!\!\!\!*}$ ${\displaystyle P\cup \!\!\!\!\!*Q}$ ${\displaystyle h}$ ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle h_{P}}$ ${\displaystyle h_{Q}}$ ${\displaystyle h}$ ${\displaystyle h_{P}\cap h_{Q}}$ ${\displaystyle P\cup \!\!\!\!\!*Q}$

Lógica de separación concurrente

Una lógica de separación concurrente (CSL), una versión de la lógica de separación para programas concurrentes, fue propuesta originalmente por Peter O'Hearn ^[11] , utilizando una regla de prueba

${\displaystyle {\frac {\{P_{1}\}C_{1}\{Q_{1}\}\quad \{P_{2}\}C_{2}\{Q_{2}\}}{\{P_{1}*P_{2}\}C_{1}\parallel C_{2}\{Q_{1}*Q_{2}\}}}}$

que permite el razonamiento independiente sobre subprocesos que acceden a almacenamiento separado. Las reglas de prueba de O'Hearn adaptaron un enfoque temprano de Tony Hoare para razonar sobre concurrencia, ^[12] reemplazando el uso de restricciones de alcance para asegurar la separación mediante el razonamiento en lógica de separación. Además de extender el enfoque de Hoare para aplicarlo en presencia de punteros asignados al montón, O'Hearn mostró cómo el razonamiento en lógica de separación concurrente podría rastrear la transferencia de propiedad dinámica de porciones del montón entre procesos; los ejemplos en el artículo incluyen un búfer de transferencia de punteros y un administrador de memoria .

Al comentar el trabajo clásico temprano sobre la libertad de interferencia de Susan Owicki y David Gries , O'Hearn dice que la verificación explícita de la no interferencia no es necesaria porque su sistema descarta la interferencia de manera implícita, por la naturaleza de la forma en que se construyen las pruebas.

Stephen Brookes fue el primero en proporcionar un modelo para la lógica de separación concurrente en un artículo complementario al de O'Hearn. ^[13] La solidez de la lógica había sido un problema difícil y, de hecho, un contraejemplo de John Reynolds había demostrado la falta de solidez de una versión anterior, no publicada, de la lógica; la cuestión planteada por el ejemplo de Reynolds se describe brevemente en el artículo de O'Hearn y más detalladamente en el de Brookes.

En un principio, parecía que el CSL era adecuado para lo que Dijkstra había llamado procesos débilmente conectados ^[14] , pero tal vez no para algoritmos concurrentes de grano fino con interferencias significativas. Sin embargo, poco a poco se fue dando cuenta de que el enfoque básico del CSL era considerablemente más potente de lo que se había previsto inicialmente, si se empleaban modelos no estándar de los conectivos lógicos e incluso de las ternas de Hoare.

Se propuso una versión abstracta de la lógica de separación que funciona para triples de Hoare donde las precondiciones y las poscondiciones son fórmulas interpretadas sobre un monoide conmutativo parcial arbitrario en lugar de un modelo de montón particular. ^[15] Más tarde, mediante la elección adecuada del monoide conmutativo, se descubrió sorprendentemente que las reglas de prueba de las versiones abstractas de la lógica de separación concurrente se podían utilizar para razonar sobre procesos concurrentes que interfieren, por ejemplo, codificando la técnica de garantía de confianza que se había propuesto originalmente para razonar sobre la interferencia; ^[16] en este trabajo, los elementos del modelo no se consideraron recursos, sino más bien "vistas" del estado del programa, y ​​una interpretación no estándar de los triples de Hoare acompaña la lectura no estándar de las precondiciones y poscondiciones. Finalmente, se han utilizado principios de estilo CSL para componer razonamientos sobre historias de programas en lugar de estados de programas, con el fin de proporcionar técnicas modulares para razonar sobre algoritmos concurrentes de grano fino. ^[17]

Se han incluido versiones de CSL en muchas herramientas de verificación interactivas y semiautomáticas (o "intermedias"), como se describe en la siguiente sección. Un esfuerzo de verificación particularmente significativo es el del núcleo μC/OS-II mencionado allí. Pero, aunque se han dado pasos, ^[18] hasta el momento el razonamiento al estilo CSL se ha incluido en comparativamente pocas herramientas en la categoría de análisis automático de programas (y ninguna se menciona en la siguiente sección).

O'Hearn y Brookes son co-ganadores del Premio Gödel 2016 por su invención de la lógica de separación concurrente. ^[19]

Herramientas de verificación y análisis de programas

Las herramientas para razonar sobre programas abarcan desde herramientas de análisis de programas totalmente automáticas, que no requieren ninguna intervención del usuario, hasta herramientas interactivas en las que el ser humano participa íntimamente en el proceso de prueba. Se han desarrollado muchas de estas herramientas; la siguiente lista incluye algunos representantes de cada categoría.

• Análisis automático de programas. Estas herramientas suelen buscar clases restringidas de errores (por ejemplo, errores de seguridad de la memoria) o intentan demostrar su ausencia, pero no consiguen demostrar su total corrección.
  • Un ejemplo actual es Facebook Infer , una herramienta de análisis estático para Java, C y Objective-C basada en lógica de separación y bi-abducción. ^[20] En 2015, Infer encontraba cientos de errores por mes y los desarrolladores los solucionaban antes de enviarlos a las aplicaciones móviles de Facebook ^[21].
  • Otros ejemplos incluyen SpaceInvader (uno de los primeros analizadores SL), Predator (que ha ganado varias competiciones de verificación), MemCAD (que mezcla formas y propiedades numéricas) y SLAyer (de Microsoft Research, centrado en las estructuras de datos que se encuentran en los controladores de dispositivos).
• Prueba interactiva. Se han realizado pruebas utilizando incrustaciones de lógica de separación en demostradores de teoremas interactivos, como el asistente de prueba Coq y HOL (asistente de prueba) . En comparación con el trabajo de análisis de programas, estas herramientas requieren más esfuerzo humano, pero prueban propiedades más profundas, hasta la corrección funcional.
  • Una prueba del sistema de archivos FSCQ ^[22] donde la especificación incluye el comportamiento en caso de fallos y en condiciones normales de funcionamiento. Este trabajo ganó el premio al mejor artículo en el Simposio sobre Principios de Sistemas Operativos de 2015.
  • Verificación de un gran fragmento del sistema de tipos Rust y algunas de sus bibliotecas estándar en el proyecto RustBelt utilizando el marco Iris para la lógica de separación en el asistente de pruebas Coq .
  • Verificación de una implementación OpenSSL de un algoritmo de autenticación criptográfica, ^[23] utilizando C verificable
  • Verificación de módulos clave de un núcleo de sistema operativo comercial, el núcleo μC/OS-II, el primer núcleo preventivo comercial que se ha verificado. ^[24]
  • Otros ejemplos incluyen la biblioteca Ynot ^{[25] para el} asistente de prueba Coq ; la incrustación Holfoot de Smallfoot en HOL; lógica de separación concurrente de grano fino y Bedrock (una biblioteca Coq para programación de bajo nivel).
• Entremedio. Muchas herramientas requieren más intervención del usuario que los análisis de programas, ya que esperan que el usuario ingrese aserciones como especificaciones pre/post para funciones o invariantes de bucle, pero después de que se proporciona esta entrada intentan ser completamente o casi completamente automáticas; este modo de verificación se remonta a trabajos clásicos de la década de 1970, como el verificador de J. King y el verificador Pascal de Stanford. Este estilo de verificador se ha denominado recientemente verificación activa automática, un término que pretende evocar la forma de interactuar con un verificador a través de un bucle de verificación de aserciones, análogo a la interacción entre un programador y un verificador de tipos.
  • El primer verificador de lógica de separación, Smallfoot, se encontraba en esta categoría intermedia. Requería que el usuario ingresara especificaciones previas y posteriores, invariantes de bucle e invariantes de recursos para los bloqueos. Introdujo un método de ejecución simbólica, así como una forma automática de inferir axiomas de marco. Smallfoot incluía lógica de separación concurrente.
  • SmallfootRG es un verificador para la unión de la lógica de separación y el método clásico de confianza/garantía para programas concurrentes.
  • Heap Hop implementa una lógica de separación para el paso de mensajes, siguiendo las ideas de Singularity (sistema operativo) .
  • VeriFast es una herramienta avanzada de última generación que se encuentra en la categoría intermedia. Ha demostrado pruebas que abarcan desde patrones orientados a objetos hasta algoritmos altamente concurrentes y programas de sistemas.
  • Viper es una infraestructura de verificación automatizada de última generación para razonamiento basado en permisos. Consiste principalmente en un lenguaje de programación y dos backends de verificación, uno basado en ejecución simbólica y otro en generación de condiciones de verificación (VCG). ^[26] Basados ​​en la infraestructura Viper, han surgido varios frontends para varios lenguajes de programación: Gobra para Go, Nagini para Python, Prusti para Rust y VerCors para C, Java, OpenCL y OpenMP. Estos frontends traducen el lenguaje de programación frontend a Viper para luego usar un backend de verificación Viper para probar la corrección del programa de entrada.
  • El lenguaje de programación Mezzo y los tipos de separación líquida asincrónica incluyen ideas relacionadas con CSL en el sistema de tipos de un lenguaje de programación. La idea de incluir la separación en un sistema de tipos tiene ejemplos anteriores en Tipos de alias y Control sintáctico de interferencias.

La distinción entre verificadores interactivos y verificadores intermedios no es tan clara. Por ejemplo, Bedrock busca un alto grado de automatización, en lo que denomina verificación mayoritariamente automática, mientras que Verifast a veces requiere anotaciones que se asemejan a las tácticas (pequeños programas) que se utilizan en los verificadores interactivos.

Decidibilidad y complejidad

Se puede demostrar que el problema de satisfacibilidad para un fragmento multiclasificado y sin cuantificadores de lógica de separación parametrizado sobre los tipos de ubicaciones y datos es PSPACE-completo . ^[27] Se ha integrado un algoritmo para resolver este fragmento en solucionadores SMT basados ​​en DPLL(T) en cvc5 . ^[28] Extendiendo este resultado, también se puede demostrar que la satisfacibilidad para un análogo de la clase Bernays–Schönfinkel para lógica de separación con ubicaciones de memoria no interpretadas es PSPACE-completo, mientras que el problema es indecidible con ubicaciones de memoria interpretadas (por ejemplo, números enteros) o con otras alternancias de cuantificadores ^[29]

Referencias

1. Reynolds, John C. (2002). "Lógica de separación: una lógica para estructuras de datos mutables compartidas" (PDF) . LICS .
2. Reynolds, John C. (1999). "Razonamiento intuicionista sobre estructuras de datos mutables compartidas". En Davies, Jim ; Roscoe, Bill ; Woodcock, Jim (eds.). Perspectivas milenarias en informática, Actas del Simposio Oxford-Microsoft de 1999 en honor a Sir Tony Hoare . Palgrave .
3. Ishtiaq, Samin; O'Hearn, Peter (2001). "BI como lenguaje de aserción para estructuras de datos mutables". Actas del 28.º simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . ACM . págs. 14-26. doi :10.1145/360204.375719. ISBN . 1581133367. Número de identificación del sujeto  2652274. {{cite book}}: |journal=ignorado ( ayuda )
4. O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). "Razonamiento local sobre programas que alteran estructuras de datos". CSL . CiteSeerX 10.1.1.29.1331 . 
5. Burstall, RM (1972). "Algunas técnicas para probar programas que alteran las estructuras de datos". Inteligencia artificial . 7 .
6. O'Hearn, PW; Pym, DJ (junio de 1999). "La lógica de las implicaciones agrupadas". Boletín de lógica simbólica . 5 (2): 215–244. CiteSeerX 10.1.1.27.4742 . doi :10.2307/421090. JSTOR  421090. S2CID  2948552. 
7. O'Hearn, Peter (febrero de 2019). "Lógica de separación". Commun. ACM . 62 (2): 86–95. doi : 10.1145/3211968 . ISSN  0001-0782.
8. Yang, Hongseok (2001). "Un ejemplo de razonamiento local en la lógica de punteros de BI: el algoritmo de marcado de grafos de Schorr-Waite". Actas del 1.er taller sobre análisis de programas semánticos y entornos informáticos para la gestión de memoria .
9. Hobor, Aquinas; Villard, Jules (2013). "Las ramificaciones de la compartición en estructuras de datos" (PDF) . ACM SIGPLAN Notices . 48 : 523–536. doi :10.1145/2480359.2429131.
10. Gardner, Philippa; Maffeis, Sergio; Smith, Hareth (2012). "Hacia una lógica de programación para Java Script" (PDF) . Actas del 39.º simposio anual ACM SIGPLAN-SIGACT sobre Principios de lenguajes de programación - POPL '12 . págs. 31–44. doi :10.1145/2103656.2103663. hdl :10044/1/33265. ISBN. 9781450310833.S2CID 9571576  .
11. O'Hearn, Peter (2007). "Recursos, concurrencia y razonamiento local" (PDF) . Ciencias de la computación teórica . 375 (1–3): 271–307. doi : 10.1016/j.tcs.2006.12.035 .
12. Hoare, CAR (1972). "Hacia una teoría de la programación paralela". Técnicas de sistemas operativos. Academic Press .
13. Brookes, Stephen (2007). "Una semántica para la lógica de separación concurrente" (PDF) . Theoretical Computer Science . 375 (1–3): 227–270. doi :10.1016/j.tcs.2006.12.034.
14. Dijkstra, Edsger W. Procesos secuenciales cooperativos (EWD-123) (PDF) . Archivo EW Dijkstra. Centro de Historia Estadounidense, Universidad de Texas en Austin .(transcripción) (septiembre de 1965)
15. Calcagno, Cristiano; O'Hearn, Peter W.; Yang, Hongseok (2007). "Lógica de separación abstracta y acción local" (PDF) . 22.º Simposio anual IEEE sobre lógica en informática (LICS 2007) . pp. 366–378. CiteSeerX 10.1.1.66.6337 . doi :10.1109/LICS.2007.30. ISBN .  978-0-7695-2908-0.S2CID1044254  .​
16. Dinsdale-Young, Thomas; Birkedal, Lars; Gardner, Philippa; Parkinson, Matthew; Yang, Hongseok (2013). "Vistas" (PDF) . Avisos SIGPLAN de la ACM . 48 : 287–300. doi :10.1145/2480359.2429104.
17. Sergey, Ilya; Nanevski, Aleksandar; Banerjee, Anindya (2015). "Especificación y verificación de algoritmos concurrentes con historias y subjetividad" (PDF) . 24º Simposio Europeo de Programación . arXiv : 1410.0306 . Código Bibliográfico :2014arXiv1410.0306S.
18. Gotsman, Alexey; Berdine, Josh; Cook, Byron; Sagiv, Mooly (2007). "Análisis de forma modular de hilos". Verificación, comprobación de modelos e interpretación abstracta (PDF) . Apuntes de clase en informática. Vol. 5403. págs. 266–277. doi :10.1007/978-3-540-93900-9_3. ISBN 978-3-540-93899-6. {{cite book}}: |journal=ignorado ( ayuda )
19. "Premio Gödel 2016". Asociación Europea de Informática Teórica . Consultado el 29 de agosto de 2022 .
20. Lógica de separación y bi-abducción, página, sitio del proyecto Infer.
21. Código abierto de Facebook Infer: identifica errores antes de publicar. C Calcagno, D D'Stefano y P O'Hearn. 11 de junio de 2015
22. Uso de la lógica Crash Hoare para certificar el sistema de archivos FSCQ, H Chen et al, SOSP'15
23. Verificación de la exactitud y seguridad de OpenSSL HMAC. Lennart Beringer, Adam Petcher, Katherine Q. Ye y Andrew W. Appel. En el 24.º Simposio de seguridad de USENIX , agosto de 2015
24. Un marco de verificación práctico para kernels de SO preventivos. Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang y Zhaohui Li:. En CAV 2016: 59-79
25. Página de inicio del Proyecto Ynot, Universidad de Harvard , EE. UU.
26. Viper: una infraestructura de verificación para el razonamiento basado en permisos, P. Müller, M. Schwerhoff y AJ Summers, VMCAI'16
27. Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "Un procedimiento de decisión para la lógica de separación en SMT". En Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). Tecnología automatizada para verificación y análisis . Apuntes de clase en informática. Cham: Springer International Publishing. págs. 244–261. arXiv : 1603.06844 . doi :10.1007/978-3-319-46520-3_16. ISBN . 978-3-319-46520-3.
28. Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). "cvc5: Un solucionador SMT versátil y de potencia industrial". En Fisman, Dana; Rosu, Grigore (eds.). Herramientas y algoritmos para la construcción y análisis de sistemas . Apuntes de clase en informática. Cham: Springer International Publishing. págs. 415–442. doi : 10.1007/978-3-030-99524-9_24 . ISBN 978-3-030-99524-9.
29. Reynolds, Andrew; Iosif, Radu; Serban, Cristina (2017). "Razonamiento en el fragmento de Bernays-Schönfinkel-Ramsey de la lógica de separación". En Bouajjani, Ahmed; Monniaux, David (eds.). Verificación, comprobación de modelos e interpretación abstracta . Apuntes de clase en informática. Cham: Springer International Publishing. págs. 462–482. doi :10.1007/978-3-319-52234-0_25. ISBN . 978-3-319-52234-0.