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 programas. Fue desarrollado 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 del MCCA realizado por O'Hearn muestra los avances 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 , mediante el cual las especificaciones y pruebas de un componente de programa mencionan solo la porción de memoria utilizada por el componente, y no todo el estado global 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 aserciones 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 . Una tienda 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 están separados (denotados ) 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 aserciones de lógica de separación (indicadas como , , ) contienen los conectivos 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, cuándo (dónde denota el valor de la expresión evaluada en la tienda ) y, por lo demás, 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 estrella o conjunción de separación ) afirma que el montón se puede dividir en dos partes separadas donde se cumplen sus dos argumentos, 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 de separación ) 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 clásicos de conjunción e implicación . Se pueden combinar usando 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 prueba.

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 precondición, entonces el programa no saldrá mal (por ejemplo, tendrá un comportamiento indefinido), y si termina, entonces el estado final satisfará la poscondición . En esencia, durante su ejecución, sólo podrá acceder a 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 regla marco (llamada 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 (satisfactorio ), también puede ejecutarse en cualquier estado más grande (satisfactorio ) 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 impone esto especificando 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 conduce a pruebas simples de manipulación de punteros para estructuras de datos que exhiben patrones de intercambio regulares que pueden describirse simplemente usando conjunciones de separación; los ejemplos incluyen listas simple y doblemente enlazadas y variedades de árboles. Los gráficos, DAG y otras estructuras de datos con un intercambio más general son más difíciles para la prueba tanto formal como informal. No obstante, la lógica de separación se ha aplicado con éxito al razonamiento sobre programas con compartición general.

En su artículo POPL'01, ^[3] O'Hearn e Ishtiaq explicaron cómo el conectivo 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 poscondición, no solo una que se presenta claramente usando la conjunción de separación. Esta idea fue llevada mucho más allá por Yang, quien solía proporcionar razonamientos localizados sobre mutaciones en el clásico algoritmo de marcado de gráficos 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 sólo 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: retenciones de un montón cuando y retenciones para submontones y cuya unión es , pero que posiblemente tengan una porción no vacía en común. De manera abstracta, puede verse como una versión de la lógica de fusión conectiva 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

Peter O'Hearn propuso originalmente una lógica de separación concurrente (CSL), una versión de la lógica de separación para programas concurrentes, [ ^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}\}}}}$

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

Al comentar sobre los primeros trabajos clásicos 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 realizan las pruebas. construido.

Stephen Brookes proporcionó por primera vez 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 e inédita 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.

Al principio parecía que CSL se adaptaba bien a lo que Dijkstra había llamado procesos poco conectados, ^[14] pero tal vez no a algoritmos concurrentes detallados con interferencia significativa. Sin embargo, gradualmente se fue dando cuenta de que el enfoque básico de CSL era considerablemente más poderoso 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 los triples de Hoare donde las condiciones previas y posteriores 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 podrían usarse para razonar sobre la interferencia de procesos concurrentes, por ejemplo codificando la técnica de garantía de confianza que se había utilizado originalmente. propuso 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 condiciones previas y posteriores. 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 el razonamiento sobre algoritmos concurrentes detallados. ^[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 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 reciben conjuntamente el 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 se encuentran en un espectro que va 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 herramientas de este tipo; la siguiente lista incluye algunos representantes en cada categoría.

• Análisis automáticos de programas. Estas herramientas normalmente buscan clases restringidas de errores (por ejemplo, errores de seguridad de la memoria) o intentan demostrar su ausencia, pero no logran 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] A partir de 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 varios concursos de verificación), MemCAD (que mezcla propiedades numéricas y de forma) y SLAyer (de Microsoft Research, centrado en estructuras de datos encontradas en controladores de dispositivos).
• Prueba interactiva. Las pruebas se han realizado utilizando incorporaciones 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 demuestran 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 fallas así como el funcionamiento normal. 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 prueba The 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 kernel de sistema operativo comercial, el kernel μC/OS-II, el primer kernel preventivo comercial que se ha verificado. ^[24]
  • Otros ejemplos incluyen la biblioteca Ynot ^[25] para el asistente de prueba Coq ; la incorporación de Holfoot de Smallfoot en HOL; Lógica de separación concurrente detallada y Bedrock (una biblioteca Coq para programación de bajo nivel).
• Entre. Muchas herramientas requieren más intervención del usuario que los análisis de programas, ya que esperan que el usuario ingrese afirmaciones como especificaciones previas y posteriores para funciones o invariantes de bucle, pero después de que se proporciona esta entrada, intentan ser total o casi completamente automáticos; 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 de Stanford Pascal. Este estilo de verificador se ha denominado recientemente verificación autoactiva, término que pretende evocar la forma de interactuar con un verificador a través de un bucle de verificación de afirmación, análogo a la interacción entre un programador y un verificador de tipos.
  • El primer verificador de Separation Logic, Smallfoot, estaba en esta categoría intermedia. Requería que el usuario ingresara especificaciones previas y posteriores, invariantes de bucle e invariantes de recursos para bloqueos. Introdujo un método de ejecución simbólica, así como una forma automática de inferir axiomas de marcos. Smallfoot incluyó lógica de separación concurrente.
  • SmallfootRG es un verificador de una combinación de 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 actual avanzada en la categoría intermedia. Ha demostrado pruebas que van 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. Consta principalmente de 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] Sobre la base de la infraestructura de Viper, han surgido varias interfaces para varios lenguajes de programación: Gobra para Go, Nagini para Python, Prusti para Rust y VerCors para C, Java, OpenCL y OpenMP. Estas interfaces traducen el lenguaje de programación frontend a Viper para luego usar un backend de verificación de Viper para demostrar la corrección del programa de entrada.
  • El lenguaje de programación Mezzo y los tipos de separación de líquidos asíncronos incluyen ideas relacionadas con CSL en el sistema de tipos de un lenguaje de programación. La idea de incluir separación en un sistema de tipos tiene ejemplos anteriores en Tipos de alias y Control sintáctico de interferencia.

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

Decidibilidad y complejidad

Se puede demostrar que el problema de satisfacibilidad para un fragmento de lógica de separación multiclasificado y sin cuantificadores parametrizado sobre los tipos de ubicaciones y datos es PSPACE completo . ^[27] Se ha integrado en cvc5 un algoritmo para resolver este fragmento en solucionadores SMT basados ​​en DPLL(T) . ^[28] Ampliando este resultado, también se puede demostrar que la satisfacibilidad de un análogo de la clase de Bernays-Schönfinkel para la 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 más. 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) . LIC .
2. Reynolds, John C. (1999). "Razonamiento intuicionista sobre la estructura de datos mutables compartidos". En Davies, Jim ; Roscoe, Bill ; Woodcock, Jim (eds.). Millennial Perspectives in Computer Science, 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. S2CID  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 estructuras de datos". Inteligencia de las máquinas . 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". Comunitario. 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 puntero de BI: el algoritmo de marcado de gráficos de Schorr-Waite". Actas del primer taller sobre semántica, 'análisis de programas' y entornos informáticos para la gestión de la memoria .
9. Hobor, Tomás de Aquino; Villard, Jules (2013). "Las ramificaciones de compartir estructuras de datos" (PDF) . Avisos ACM SIGPLAN . 48 : 523–536. doi :10.1145/2480359.2429131.
10. Gardner, Philippa; Maffeis, Sergio; Smith, Hareth (2012). «Hacia una lógica de programa 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) . Informática Teórica . 375 (1–3): 271–307. doi : 10.1016/j.tcs.2006.12.035 .
12. Hoare, COCHE (1972). "Hacia una teoría de la programación paralela". Técnicas de sistemas operativos. Prensa académica .
13. Brookes, Stephen (2007). "Una semántica para la lógica de separación concurrente" (PDF) . Informática Teórica . 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). «Acción local y lógica de separación abstracta» (PDF) . 22º Simposio anual del IEEE sobre lógica en informática (LICS 2007) . págs. 366–378. CiteSeerX 10.1.1.66.6337 . doi :10.1109/LICS.2007.30. ISBN  978-0-7695-2908-0. S2CID  1044254.
16. Dinsdale-Young, Thomas; Birkedal, Lars; Gardner, Philippa; Parkinson, Mateo; Yang, Hongseok (2013). "Vistas" (PDF) . Avisos ACM SIGPLAN . 48 : 287–300. doi :10.1145/2480359.2429104.
17. Sergey, Ilya; Nanevski, Aleksandar; Banerjee, Anindya (2015). "Especificar y verificar algoritmos concurrentes con historias y subjetividad" (PDF) . 24º Simposio Europeo de Programación . arXiv : 1410.0306 . Código Bib : 2014arXiv1410.0306S.
18. Gotsman, Alexey; Berdine, Josh; Cocinero, Byron; Sagiv, Mooly (2007). "Análisis de forma modular de hilo". Verificación, verificación de modelos e interpretación de resúmenes (PDF) . Apuntes de conferencias sobre 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. Facebook Infer de código abierto: identifique errores antes de realizar el envío. C Calcagno, D DIstefano y P O'Hearn. 11 de junio de 2015
22. Uso de Crash Hoare Logic para certificar el sistema de archivos FSCQ, H Chen et al, SOSP'15
23. Corrección y seguridad verificadas 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, Andrés; José, Radu; Serban, Cristina; Rey, Tim (2016). Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). "Un procedimiento de decisión para la lógica de separación en SMT". Tecnología Automatizada para Verificación y Análisis . Apuntes de conferencias sobre informática. Cham: Springer International Publishing: 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; Cerebro, Martín; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andrés; Özdemir, Alex; Preiner, Mathías; Reynolds, Andrés; Sheng, Ying; Tinelli, César (2022). Fisman, Dana; Rosu, Grigore (eds.). "cvc5: un solucionador SMT versátil y de potencia industrial". Herramientas y Algoritmos para la Construcción y Análisis de Sistemas . Apuntes de conferencias sobre informática. Cham: Springer International Publishing: 415–442. doi : 10.1007/978-3-030-99524-9_24 . ISBN 978-3-030-99524-9.
29. Reynolds, Andrés; José, Radu; Serban, Cristina (2017). Bouajjani, Ahmed; Monniaux, David (eds.). "Razonamiento en el fragmento de lógica de separación de Bernays-Schönfinkel-Ramsey". Verificación, verificación de modelos e interpretación de resúmenes . Apuntes de conferencias sobre informática. Cham: Springer International Publishing: 462–482. doi :10.1007/978-3-319-52234-0_25. ISBN 978-3-319-52234-0.