Cover Image

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Dane, Serra Z., Chen, Jiawei, Pouzet, Marc, Jeannin, Jean-Baptiste
Format:	Preprint
Published:	2026
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Synchronous Programming with Refinement Types
by: Chen, Jiawei, et al.
Published: (2024)

PSM: Policy Synchronised Deterministic Memory
by: Mendler, Michael, et al.
Published: (2025)

Formally verified asymptotic consensus in robust networks
by: Tekriwal, Mohit, et al.
Published: (2022)

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
by: Tao, Yichen, et al.
Published: (2026)

Practical Formal Verification for MLIR Programs
by: Tucker, Emily, et al.
Published: (2026)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
by: Parthasarathy, Gaurav, et al.
Published: (2024)

Efficient Formal Verification of Quantum Error Correcting Programs
by: Huang, Qifan, et al.
Published: (2025)

Formal Simulation and Visualisation of Hybrid Programs
by: Mendes, Pedro, et al.
Published: (2024)

Towards Automated Verification of LLM-Synthesized C Programs
by: Mukherjee, Prasita, et al.
Published: (2024)

Minuska: Towards a Formally Verified Programming Language Framework
by: Tušil, Jan, et al.
Published: (2024)

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
by: Councilman, Aaron, et al.
Published: (2025)

Relating Answer Set Programming and Many-sorted Logics for Formal Verification
by: Hansen, Zachary
Published: (2025)

First-Class Refinement Types for Scala
by: Bovel, Matt, et al.
Published: (2026)

VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
by: Xin, Yutong, et al.
Published: (2026)

Refinement-Types Driven Development: A study
by: Domínguez, Facundo, et al.
Published: (2025)

Formal Verification of Variational Quantum Circuits
by: Assolini, Nicola, et al.
Published: (2025)

FLAT: Formal Languages as Types
by: Zhu, Fengmin, et al.
Published: (2025)

Solvable Tuple Patterns and Their Applications to Program Verification
by: Kobayashi, Naoki, et al.
Published: (2025)

Compositional Program Verification with Polynomial Functors in Dependent Type Theory
by: Aberlé, C. B.
Published: (2026)

SynQ: An Embedded DSL for Synchronous System Design with Quantitative Types
by: Chen, Rui, et al.
Published: (2025)

VyZX: Formal Verification of a Graphical Quantum Language
by: Lehmann, Adrian, et al.
Published: (2023)

Automated Formal Verification of a Software Fault Isolation System
by: Sotoudeh, Matthew, et al.
Published: (2025)

From Algebraic Word Problem to Program: A Formalized Approach
by: Wiemerslage, Adam, et al.
Published: (2020)

Enabling the Verification and Formalization of Hybrid Quantum-Classical Computing with OpenQASM 3.0 compatible QASM-TS 2.0
by: Kim, Sean, et al.
Published: (2024)

Practical Refinement Session Type Inference (Extended Version)
by: Ueno, Toby, et al.
Published: (2026)

Ownership Refinement Types for Pointer Arithmetic and Nested Arrays
by: Fujiwara, Yusuke, et al.
Published: (2026)

C*: Unifying Programming and Verification in C
by: Cao, Yiyuan, et al.
Published: (2025)

Towards Repository-Level Program Verification with Large Language Models
by: Zhong, Si Cheng, et al.
Published: (2025)

A Hybrid Approach to Semi-automated Rust Verification
by: Ayoun, Sacha-Élie, et al.
Published: (2024)

Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
by: Udomsrirungruang, Thien, et al.
Published: (2024)

Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
by: Barrière, Aurèle, et al.
Published: (2025)

Dependent Type Refinements for Futures
by: Somayyajula, Siva, et al.
Published: (2023)

Hybrid Path-Sums for Hybrid Quantum Programs
by: Chareton, Christophe, et al.
Published: (2026)

Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings
by: Bagrel, Thomas
Published: (2026)

SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop
by: Chang, Fu-Chieh, et al.
Published: (2026)

Towards LLM-Powered Verilog RTL Assistant: Self-Verification and Self-Correction
by: Huang, Hanxian, et al.
Published: (2024)

Weighted NetKAT: A Programming Language For Quantitative Network Verification
by: Acevedo, Emmanuel Suárez, et al.
Published: (2026)

KestRel: Relational Verification Using E-Graphs for Program Alignment
by: Dickerson, Robert, et al.
Published: (2024)

Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
by: Ciccalè, Marco, et al.
Published: (2025)

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
by: Faella, Marco, et al.
Published: (2024)