12 noticias
El artículo técnico analiza la capacidad del lenguaje de especificación TLA+ para expresar propiedades de alcanzabilidad y posibilidad, un tema que suele generar confusión debido a la naturaleza lineal de su lógica frente a la lógica de tiempo ramificado. El texto explica que, aunque TLA+ no permite
En ingeniería de software se utiliza la palabra "abstracción" para designar dos prácticas muy distintas que suelen confundirse. Un análisis publicado por el blog técnico Muratbuffalo distingue entre la abstracción de modularidad, herencia de la carrera de ciencias de la computación, y la abstracción
El model checking de estados finitos —la verificación de sistemas mediante la exploración exhaustiva de todos sus estados posibles— ha sido técnicamente superado desde mediados de los años noventa por el model checking simbólico, capaz de manejar tamaños de modelo muy superiores. Sin embargo, sigue
La liquidación financiera transfronteriza sigue siendo lenta y costosa, con costes medios de remesa en torno al 6% del importe enviado y solo un tercio de los pagos minoristas internacionales liquidándose en menos de una hora. Keeta es una red blockchain de reciente lanzamiento, diseñada para pagos
Depot ha utilizado el lenguaje de especificación formal TLA+ y su model checker TLC para verificar el recolector de basura de Depot Registry v2. El equipo sostiene que los errores más difíciles en sistemas distribuidos no aparecen en una sola operación, sino en intercalados concretos: dos procesos h
La plataforma de pruebas Antithesis ha identificado errores en todas las implementaciones del protocolo de consenso Raft que ha analizado, entre ellas HashiCorp Raft, Aeron Cluster, OpenRaft y MicroRaft. Los fallos detectados violan la principal invariante del algoritmo, conocida como seguridad de l
El equipo de dqlite en Canonical, formado por Marco Manino y Alberto Carretero, ha analizado un error de larga duración presente en el motor de base de datos SQLite desde 2010, cuya corrección se publicó en la versión 3.51.3. El fallo reside en la fase de checkpoint del modo Write Ahead Log (WAL) y,
La regla de Stroustrup, formulada por el creador de C++, sostiene que los principiantes necesitan sintaxis explícita y detallada, mientras que los expertos prefieren notación breve y tersa. El principio aparece en una retrospectiva sobre C++ del propio Bjarne Stroustrup: las características nuevas p
La verificación formal permite demostrar matemáticamente que un programa cumple ciertas propiedades en todos los estados alcanzables, a diferencia del testing, que solo descarta un conjunto finito de casos. Para ello se usan lenguajes como Dafny, Lean, Rocq, Isabelle, F* o TLA+, en los que las espec
Los modelos de lenguaje grande (LLMs) están facilitando el uso de TLA+ (Temporal Logic of Actions), un lenguaje de verificación formal inventedo por Leslie Lamport en la década de 1990. Según el ingeniero Jesse Jiryu Davis en un artículo publicado en emptysqua.re, los LLMs Frontier pueden generar có
Un equipo de investigadores desarrolló SysMoBench, un benchmark automatizado para evaluar si los modelos de lenguaje de gran escala (LLMs) pueden modelar sistemas informáticos reales o simplemente recitan especificaciones de protocolos de manuales académicos. El sistema evalúa once sistemas distribu
Este artículo del blog de vertexclique.com introduce Kovan, una nueva biblioteca de Rust diseñada para abordar un problema crítico en sistemas concurrentes de alto rendimiento: la recolección de memoria wait-free. El problema surge al usar estructuras de datos lock-free, como las proporcionadas por
