Laura Titolo
  • Bio
  • Publications
  • Projects
  • Experience
  • News
  • Recent & Upcoming Talks
    • Example Talk
  • Blog
    • LOPSTR 2025
    • New position at Code Metal
    • NFM 2025
    • CPP 2025
    • CPP 2025
    • FMICS 2023
    • NASA Group Achivement award for CPR
    • SOAP 2022
    • NFM 2021
  • Publications
    • Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0
    • A Temporal Differential Dynamic Logic Formal Embedding
    • A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts
    • A Compositional Proof Framework for FRETish Requirements
    • Formal analysis of the compact position reporting algorithm
    • From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project
    • Automatic Generation of Guard-Stable Floating-Point Code
    • Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm
    • A Mixed Real and Floating-Point Solver
    • Eliminating Unstable Tests in Floating-Point Programs
    • A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
    • An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
    • Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis
    • A Formal Analysis of the Compact Position Reporting Algorithm
    • A constraint-based language for modelling intelligent environments
    • A program analysis framework for tccp based on abstract interpretation
    • Abstract Analysis of Universal Properties for tccp
    • Modelling Hybrid Systems in Hy-tccp
    • Modeling Hybrid Systems in the Concurrent Constraint Paradigm
    • Abstract Diagnosis for tccp using a Linear Temporal Logic
    • Towards an Effective Decision Procedure for LTL formulas with Constraints
    • An Abstract Interpretation Framework for Verification of Timed Concurrent Constraint Languages
    • Abstract Diagnosis for Timed Concurrent Constraint programs
  • Projects
    • PRECiSA
    • ReFlow
    • VSCode-PRECiSA
    • FRET Proof Framework
    • FPRoCK
    • CPR*
  • Projects
  • Experience

A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts

Oct 24, 2023·
Nikson Bernardes Fernandes Ferreira
,
Mariano M. Moscato
,
Laura Titolo
,
Mauricio Ayala-Rincon
· 0 min read
PDF Cite DOI
Type
Preprint
Publication
23rd Conference in Formal Methods in Computer-Aided Design
Last updated on Oct 24, 2023
← A Temporal Differential Dynamic Logic Formal Embedding Jan 15, 2024
A Compositional Proof Framework for FRETish Requirements Jan 17, 2022 →

©2024 Laura Titolo.

Published with Hugo Blox Builder — the free, open source website builder that empowers creators.