Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 11:00 - 11:30 at Sala III - Software Verification and Synthesis Chair(s): Ori Lahav

Hierarchical block diagrams (HBDs) are at the heart of embedded system design tools, including Simulink. Numerous translations exist from HBDs into languages with formal semantics, amenable to formal verification. However, none of these translations has been proven correct, to our knowledge.

We present in this paper the first mechanically proven HBD translation algorithm. The algorithm translates HBDs into an algebra of terms with three basic composition operations (serial, parallel, and feedback). In order to capture various translation strategies resulting in different terms achieving different tradeoffs, the algorithm is nondeterministic. Despite this, we prove its {\em semantic determinacy}: for every input HBD, all possible terms that can be generated by the algorithm are semantically equivalent. We apply this result to show how three Simulink translation strategies introduced previously can be formalized as determinizations of the algorithm, and derive that these strategies yield semantically equivalent results (a question left open in previous work). All results are formalized and proved in the Isabelle theorem-prover and the code is publicly available.

Presentation (presentation.pdf)480KiB

Tue 15 Jan

Displayed time zone: Belfast change

11:00 - 12:30
Software Verification and SynthesisVMCAI at Sala III
Chair(s): Ori Lahav Tel Aviv University
Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
Viorel Preoteasa , Iulia Dragomir , Stavros Tripakis Aalto University and UC Berkeley
Link to publication DOI Pre-print File Attached
euforia: Complete Software Model Checking with Uninterpreted Functions
Program Synthesis with Equivalence Reduction
Calvin Smith University of Wisconsin - Madison, Aws Albarghouthi University of Wisconsin-Madison