Mon 17 Jan 2022 13:30 - 13:55 at Salon III - Semantics and Program Verification Chair(s): Benjamin Delaware

Structured natural languages provide a trade space between ambiguous natural languages that make up most written requirements and mathematical formal specifications such as Linear Temporal Logic. Fretish is a structured natural language for the elicitation of system requirements developed at NASA. The related open-source tool Fret provides support for translating Fretish requirements into temporal logic formulas that can be input to several verification and analysis tools. In the context of safety-critical systems, it is crucial to ensure that a generated formula captures the semantics of the corresponding Fretish requirement precisely. This paper presents a rigorous formalization of the Fretish language including a new denotational semantics and a proof of semantic equivalence between Fretish specifications and their temporal logic counterparts computed by Fret. The complete formalization and the proof have been developed in the Prototype Verification System (PVS) theorem prover.

Mon 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 15:10
Semantics and Program VerificationCPP at Salon III
Chair(s): Benjamin Delaware Purdue University
13:30
25m
Talk
A Compositional Proof Framework for FRETish RequirementsRemote
CPP
Esther Conrad NASA LaRC, Laura Titolo NIA/NASA LaRC, Dimitra Giannakopoulou NASA Ames Research Center, Thomas Pressburger NASA ARC, Aaron Dutle NASA Langley Research Center
Pre-print Media Attached
13:55
25m
Talk
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with DerivativesRemote
CPP
Derek Egolf Northeastern University, Sam Lasser Tufts University, Kathleen Fisher Tufts University
Link to publication Media Attached
14:20
25m
Talk
Formally Verified Superblock SchedulingInPerson
CPP
Cyril Six Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Léo Gourdin Université Grenoble-Alpes, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Justus Fasse Université Grenoble-Alpes; KU Leuven, Nicolas Nardino École normale supérieure de Lyon
DOI Pre-print
14:45
25m
Talk
Overcoming Restraint: Composing Verification of Foreign Functions with CogentRemote
CPP
Louis Cheung University of Melbourne, Liam O'Connor University of Edinburgh, Christine Rizkallah University of Melbourne
DOI Pre-print Media Attached