Imagen de Portada

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Wang, Shuling, Ji, Zekun, Zhan, Bohua, Xu, Xiong, Gao, Qiang, Zhan, Naijun
Formato:	Preprint
Publicado:	2024
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

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

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

A Generalized Hybrid Hoare Logic
por: Zhan, Naijun, et al.
Publicado: (2023)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Verified Code Transpilation with LLMs
por: Bhatia, Sahil, et al.
Publicado: (2024)

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

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

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

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

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

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

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

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

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

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

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

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

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
por: Baumann, Jonathan, et al.
Publicado: (2026)

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

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

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

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

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

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

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

Compression of enumerations and gain
por: Barmpalias, George, et al.
Publicado: (2023)