Skip to main content

Main navigation

  • About ITEFI
  • Research
  • Formación y empleo
  • OpenLab
  • Servicios científico técnicos
  • Staff Directory

VeriFly: On-the-fly Assertion Checking with Ciao PP

Sánchez, M.A., García, I., Pérez, V., Morales, J.F., López, P., Hermenegildo, M.V.
6th Workshop on Formal Integrated Development Environment (F-IDE 2021), Electronic Proceedings in Theoretical Computer Science (EPTCS), pág. 1-5, Open Publishing Association (OPA), Mayo 2021. Co-located with ETAPS 2021
https://doi.org/10.4204/EPTCS.338

Fast response times are essential for the integration of global static analysis tools at early stages of the software development cycle. 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 the CiaoPP static analysis and verification framework this challenge is addressed through 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 integration 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). 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.

 

 

Partially funded by MICINN PID2019-108528RB-C21 ProCode and Madrid P2018/TCS-4339 BLOQUES-CM. We would like to thank the anonymous reviewers for their very useful comments.

 

https://arxiv.org/html/2108.02369 https://arxiv.org/html/2108.02369
GiCSI
Acoustics and Non Destructive Evaluation (DAEND)
  • Environmental Acoustics (GAA)
  • G Carma: Materials Characterization by Non Destructive Evaluation
  • ULAB, Ultrasounds for Liquid Analysis and Bioengineering
Information and Communication Technologies (TIC)
  • Cybersecurity and Privacy Protection Research Group (GiCP)
  • Research group on Cryptology and Information Security (GiCSI)
    • Quantum Communications Laboratory (LCQE)
  • Multichannel Ultrasonic Signal Processing Group (MUSP)
Sensors and Ultrasonic Systems (DSSU)
  • Ultrasonic Systems and Technologies (USTG)
  • Nanosensors and Smart Systems (NoySi)
  • Ultrasonic Resonators for cavitation and micromanipulation (RESULT)
  • Advanced Sensor Technology (SENSAVAN)
  • Quantum Electronics (QE)
Laboratorios
  • Laboratorio de Acústica
  • Laboratorio de Metrología Ultrasónica Médica (LMUM)
  • Laboratorio de Comunicaciones Cuánticas
  • Laboratory for International Collaboration in Advanced Biophotonics Imaging

Instituto de Tecnologías Físicas y de la Información Leonardo Torres Quevedo  - ITEFI
C/ Serrano, 144. 28006 - Madrid • Tel.: (+34) 91 561 88 06  Contacto  •  Intranet
EDIFICIO PARCIALMENTE ACCESIBLE POR PERSONAS CON MOVILIDAD REDUCIDA