Mechanically proving determinacy of hierarchical block diagram translations

DOI10.1007/978-3-030-11245-5_27OpenAlexW2797117664MaRDI QIDQ2287118

Stavros Tripakis, Iulia Dragomir, Viorel Preoteasa

Publication date: 23 January 2020

Full work available at URL: https://arxiv.org/abs/1611.01337

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (3)

The refinement calculus of reactive systems ⋮ A denotational semantics of simulink with higher-order UTP ⋮ Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP

Uses Software

• Coq
• Isabelle/HOL
• Simulink
• CompCert
• Locales
• SL2SX

This page was built for publication: Mechanically proving determinacy of hierarchical block diagram translations