Cover Image

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Wang, Shuling, Ji, Zekun, Zhan, Bohua, Xu, Xiong, Gao, Qiang, Zhan, Naijun
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Mars 2.0: A Toolchain for Modeling, Analysis, Verification and Code Generation of Cyber-Physical Systems
by: Zhan, Bohua, et al.
Published: (2024)

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
by: Jin, Xiangyu, et al.
Published: (2024)

HpC: A Calculus for Hybrid and Mobile Systems -- Full Version
by: Xu, Xiong, et al.
Published: (2025)

A Generalized Hybrid Hoare Logic
by: Zhan, Naijun, et al.
Published: (2023)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
by: Yang, Chengxi, et al.
Published: (2025)

Verifying Randomized Consensus Protocols with Common Coins
by: Gao, Song, et al.
Published: (2024)

VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
by: Zeng, Lingfei, et al.
Published: (2025)

Switching Controller Synthesis for Hybrid Systems Against STL Formulas
by: Su, Han, et al.
Published: (2024)

Verified Lifting of Deep learning Operators
by: Zhan, Qi, et al.
Published: (2024)

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

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
by: Wu, Jinhua, et al.
Published: (2026)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

CLEVER: A Curated Benchmark for Formally Verified Code Generation
by: Thakur, Amitayush, et al.
Published: (2025)

Verifying Sequential Consistency under Bounded Preemptions
by: Govind, R., et al.
Published: (2026)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation
by: Nezhad, Sina Bagheri, et al.
Published: (2025)

Formally Verified Linear-Time Invertible Lexing
by: Chassot, Samuel, et al.
Published: (2025)

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming
by: Wu, Hao, et al.
Published: (2023)

Verified Code Transpilation with LLMs
by: Bhatia, Sahil, et al.
Published: (2024)

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

Formal Foundations for Translational Separation Logic Verifiers (extended version)
by: Dardinier, Thibault, et al.
Published: (2024)

Piecewise Analysis of Probabilistic Programs via $k$-Induction
by: Yang, Tengshun, et al.
Published: (2024)

VeriAgent: A Tool-Integrated Multi-Agent System with Evolving Memory for PPA-Aware RTL Code Generation
by: Wang, Yaoxiang, et al.
Published: (2026)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
by: Bucev, Mario, et al.
Published: (2024)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
by: Ravi, Nikil, et al.
Published: (2026)

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
by: Huyghebaert, Sander, et al.
Published: (2023)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics
by: Chen, Haobin Hiroki, et al.
Published: (2025)

A Formally Verified Robustness Certifier for Neural Networks (Extended Version)
by: Tobler, James, et al.
Published: (2025)

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
by: Baumann, Jonathan, 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)

Verifying Fault-Tolerance of Quantum Error Correction Codes
by: Chen, Kean, et al.
Published: (2025)

QCP: A Practical Separation Logic-based C Program Verification Tool
by: Wu, Xiwei, et al.
Published: (2025)

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
by: Dane, Serra Z., et al.
Published: (2026)

Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
by: Rinard, Martin
Published: (2026)

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

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
by: Reitz, Antonin, et al.
Published: (2024)

Compression of enumerations and gain
by: Barmpalias, George, et al.
Published: (2023)