12 citations · 17 across the 7 of their papers we have counts for
7 papers
A Compositional Proof Framework for FRETish Requirements
Esther Conrad, Laura Titolo, Dimitra Giannakopoulou +2
Structured natural languages provide a trade space between ambiguous natural languages that make up most written requirements and mathematical formal specifications such as Linear…
From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project
Aaron Dutle, César Muñoz, Esther Conrad +7
The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous op…
Automatic generation and verification of test-stable floating-point code
Laura Titolo, Mariano Moscato, Cesar A. Muñoz
Test instability in a floating-point program occurs when the control flow of the program diverges from its ideal execution assuming real arithmetic. This phenomenon is caused by th…
Eliminating Unstable Tests in Floating-Point Programs
Laura Titolo, Cesar A. Muñoz, Marco A. Feliu +1
Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate…
Modeling Hybrid Systems in the Concurrent Constraint Paradigm
Damián Adalid, María del Mar Gallardo, Laura Titolo
Hybrid systems, which combine discrete and continuous dynamics, require quality modeling languages to be either described or analyzed. The Concurrent Constraint paradigm (ccp) is a…
Modeling Hybrid Systems in Hy-tccp
Damian Adalid, Maria del Mar Gallardo, Laura Titolo
Concurrent,reactive and hybrid systems require quality modeling languages to be described and analyzed. The Timed Concurrent Constraint Language (tccp) was introduced as a simple b…
Towards an Effective Decision Procedure for LTL formulas with Constraints
Marco Comini, Laura Titolo, Alicia Villanueva
This paper presents an ongoing work that is part of a more wide-ranging project whose final scope is to define a method to validate LTL formulas w.r.t. a program written in the tim…