Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types

Reference. Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types

Cite

Cite as @dane-2026-towards (helia, typst) · \cite{dane-2026-towards} (LaTeX)

BibTeX

bibtex · 1 line

@inbook{dane-2026-towards, title={Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types}, ISBN={9783032280794}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-032-28079-4_21}, DOI={10.1007/978-3-032-28079-4_21}, booktitle={NASA Formal Methods}, publisher={Springer Nature Switzerland}, author={Dane, Serra Z. and Chen, Jiawei and Pouzet, Marc and Jeannin, Jean-Baptiste}, year={2026}, pages={456–476} }

hayagriva YAML (typst)

yaml · 19 lines

dane-2026-towards:
  type: chapter
  title: Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
  author:
  - Dane, Serra Z.
  - Chen, Jiawei
  - Pouzet, Marc
  - Jeannin, Jean-Baptiste
  date: 2026
  page-range: 456-476
  url: http://dx.doi.org/10.1007/978-3-032-28079-4_21
  serial-number:
    doi: 10.1007/978-3-032-28079-4_21
    isbn: '9783032280794'
    issn: 1611-3349
  parent:
    type: book
    title: NASA Formal Methods
    publisher: Springer Nature Switzerland

Download: dane-2026-towards.bib · dane-2026-towards.yml

Cites 30 works (0 here)

External (30)

Semantics and Formal Analysis of Lingua Franca CPS Specifications in Rewriting Logic (2025)
Synchronous Programming with Refinement Types (2024)
A Temporal Differential Dynamic Logic Formal Embedding (2024)
Towards Building Verifiable CPS using Lingua Franca (2023)
A hybrid programming language for formal modeling and verification of hybrid systems (2022)
Refinement Types: A Tutorial (2021)
Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications (2018)
Logical Foundations of Cyber-Physical Systems (2018)
SCADE 6: A formal language for embedded critical software development (invited paper) (2017)
Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point (2016)
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (2015)
LiquidHaskell: experience with refinement types in the real world (2014)
Zélus: a synchronous language with ODEs (2013)
Non-standard semantics of hybrid systems modelers (2012)
A hybrid synchronous language with hierarchical automata (2011)
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified (2011)
Hoare type theory, polymorphism and separation (2008)
Differential Dynamic Logic for Hybrid Systems (2008)
Liquid types (2008)
Operational Semantics of Hybrid Systems (2005)
Safety Verification of Hybrid Systems Using Barrier Certificates (2004)
The synchronous languages 12 years later (2003)
The theory of hybrid automata (2002)
A Syntactic Approach to Type Soundness (1994)
Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems (1993)
The Esterel synchronous programming language: design, semantics, implementation (1992)
Continuous System Modeling (1991)
Programming real-time applications with SIGNAL (1991)
Real time programming: special purpose or general purpose languages (1989)
LUSTRE: a declarative language for real-time programming (1987)