Tag: Formal Methods Seminar
-
11-07-2018 | Jean-Baptiste Jeannin: Formal Verification of ACAS X, an Industrial Airborne Collision Avoidance System
Title: Formal Methods Seminar: Formal Verification of ACAS X, an Industrial Airborne Collision Avoidance System Speaker: Jean-Baptiste Jeannin, Assistant Professor, University of Michigan – Ann Arbor Date: Wednesday, November 7, 2018 Time: 1:00PM Location: B1230, R264A Abstract: Software plays an ever-increasing role in the design and operation of all aircraft, from UAVs to airliners. On-board software is rigorously developed following…
-
11-02-2018 | Laura Titolo: PRECiSA A Static Analysis Tool for Floating-Point Programs
Formal Methods Seminar Title: PRECiSA: A Static Analysis Tool for Floating-Point Programs Speaker: Laura Titolo, Staff Scientist, NIA Date: Friday, November 2, 2018 Time: 10:30am Location: B1230, R264A Abstract: Floating-point numbers are the most common finite representation of real numbers in computer programs and they offer a good trade-off between efficiency and precision. However, in safety-critical systems, round-off errors due…
-
10-19-2018 | Marco Feliu: Eliminating Unstable Tests in Floating-Point Programs
Title: Formal Methods Seminar: Eliminating Unstable Tests in Floating-Point Programs Speaker: Marco Feliu, Staff Scientist, NIA Date: Friday, October 19, 2018 Time: 10:30am Location: B1230, R264A Abstract: 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 from the ideal flow of the real-number computation. This problem,…
-
01-20-2017 | Laura Titolo and Mariano Moscato: A Static Analysis Framework for the Estimation of Verified Floating-Point Round-Off Errors
Title: FM Seminar: A Static Analysis Framework for the Estimation of Verified Floating-Point Round-Off Errors Date: Friday, January 20, 2017 Speakers: Laura Titolo, NIA and Mariano Moscato, NIA Location: NASA B1220-R110 Time: 10:30AM-11:30AM Host: Cesar Munzo, NASA/LaRC Abstract: Round-off errors in floating-point computations can lead to catastrophic consequences when occurring in safety-critical systems. In this talk,…
-
09-09-2016 | Ariane Alves Almeida: Automating Termination Proofs in PVS
Title: Formal Methods Seminar: “Automating Termination Proofs in PVS” Speaker: Ariane Alves Almeida, NIA visitor and PhD Candidate, University of Brasilia, Brazil Date: Friday, September 9, 2016 Time: 11:00am Location: NASA/LaRC, B1220, R110 Host: Cesar Munoz, NASA/LaRC Abstract: Each time a recursive function is specified in PVS, a decreasing measure over its arguments must be provided…
-
09-26-2014 | Mariano Moscato: Dynamite: A Tool for the Verification of Alloy Models Based on PVS
Formal Methods Seminar: DYNAMITE: A TOOL FOR THE VERIFICATION OF ALLOY MODELS BASED ON PVS Mariano Moscato, Postdoctoral Research Scholar, NIA September 26, 2014, 11:00 am, NASA Langley, Bldg 1220, Rm 110 Host: Cesar Munoz (NASA Langley) Abstract: Formal analysis of software models can be undertaken following two approaches: the lightweight and the heavyweight. The…