{rfName}
Ve

Indexado en

Licencia y uso

Icono OpenAccess

Citaciones

17

Altmetrics

Investigadores/as Institucionales

Morales, JfAutor o CoautorHermenegildo, MvAutor o Coautor

Compartir

26 de septiembre de 2022
Publicaciones
>
Artículo
Sí

VeriFly: On-the-fly Assertion Checking via Incrementality

Publicado en: THEORY AND PRACTICE OF LOGIC PROGRAMMING. 21 (6): 768-784 - 2021-11-01 21(6), DOI: 10.1017/s1471068421000430

Autores:

Sanchez-Ordaz, MA; Garcia-Contreras, I; Perez, V; Morales, JF; Lopez-Garcia, P; Hermenegildo, MV
[+]

Afiliaciones

IMDEA Software Inst, Madrid, Spain - Autor o Coautor
Spanish Council Sci Res CSIC, Madrid, Spain - Autor o Coautor
UPM, Madrid, Spain - Autor o Coautor
Ver más

Resumen

Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers, this means being able to have relevant properties, such as modes, types, determinacy, nonfailure, sharing, constraints, and cost, checked and errors flagged without having to actually run the program. Such global static analysis tools are arguably most useful the earlier they are used in the software development cycle, and fast response times are essential for interactive use. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. This is specially the case when complex properties need to be inferred for large, realistic code bases. In our static analysis and verification framework, this challenge is addressed through a combination of modular and incremental (context- and path-sensitive) analysis that is responsive to program edits, at different levels of granularity. In this tool paper, we present how the combination of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text - the tool's VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the- shelf "on-the-fly" syntax checking facilities (flycheck). We believe that similar extensions are also reproducible with low effort in other mature development environments. Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process. The tool supports Prolog natively, as well as other languages by semantic transformation into Horn clauses.
[+]

Palabras clave

Abstract interpretationAbstract interpretationsAbstractingAnalysis and verificationsAssertion-checkingCiaoConstraint programmingConstraint theoryDevelopment environmentHorn clausesIncremental analysisLogic and constraint programmingLogic-programmingOn-the-fly assertion checkingProgram developmentProgram development environmentProgram development environmentsProlog (programming language)SemanticsSoftware designStatic analysisSystemVerification

Indicios de calidad

Impacto bibliométrico. Análisis de la aportación y canal de difusión

El trabajo ha sido publicado en la revista THEORY AND PRACTICE OF LOGIC PROGRAMMING debido a la progresión y el buen impacto que ha alcanzado en los últimos años, según la agencia WoS (JCR), se ha convertido en una referencia en su campo. En el año de publicación del trabajo, 2021, se encontraba en la posición 5/21, consiguiendo con ello situarse como revista Q1 (Primer Cuartil), en la categoría Logic.

Independientemente del impacto esperado determinado por el canal de difusión, es importante destacar el impacto real observado de la propia aportación.

Según las diferentes agencias de indexación, el número de citas acumuladas por esta publicación hasta la fecha 2026-04-20:

  • Google Scholar: 8
  • WoS: 3
  • Scopus: 5
[+]

Impacto y visibilidad social

Desde la dimensión de Influencia o adopción social, y tomando como base las métricas asociadas a las menciones e interacciones proporcionadas por agencias especializadas en el cálculo de las denominadas “Métricas Alternativas o Sociales”, podemos destacar a fecha 2026-04-20:

  • La utilización de esta aportación en marcadores, bifurcaciones de código, añadidos a listas de favoritos para una lectura recurrente, así como visualizaciones generales, indica que alguien está usando la publicación como base de su trabajo actual. Esto puede ser un indicador destacado de futuras citas más formales y académicas. Tal afirmación es avalada por el resultado del indicador “Capture” que arroja un total de: 2 (PlumX).

Es fundamental presentar evidencias que respalden la plena alineación con los principios y directrices institucionales en torno a la Ciencia Abierta y la Conservación y Difusión del Patrimonio Intelectual. Un claro ejemplo de ello es:

  • El trabajo se ha enviado a una revista cuya política editorial permite la publicación en abierto Open Access.
  • Asignación de un Handle/URN como identificador dentro del Depósito en el Repositorio Institucional: https://oa.upm.es/70095/

Como resultado de la publicación del trabajo en el repositorio institucional, se han obtenido datos estadísticos de uso que reflejan su impacto. En términos de difusión, podemos afirmar que, hasta la fecha

  • Visualizaciones: 304
  • Descargas: 297
[+]

Análisis de liderazgo de los autores institucionales

Existe un liderazgo significativo ya que algunos de los autores pertenecientes a la institución aparecen como primer o último firmante, se puede apreciar en el detalle: Primer Autor (Sanchez-Ordaz, MA) y Último Autor (HERMENEGILDO SALINAS, MANUEL DE).

el autor responsable de establecer las labores de correspondencia ha sido Sanchez-Ordaz, MA.

[+]

Reconocimientos ligados al ítem

Research partially funded by MINECO MICINN PID2019-108528RB-C21 ProCode project, FPU grant 16/04811, the Madrid M141047003 N-GREENS and P2018/TCS-4339 BLOQUES-CM programs, and the Tezos foundation. We are also grateful to the anonymous reviewers for their comments.
[+]