Cover Image

KBX: Verified Model Synchronization via Formal Bidirectional Transformation

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Zhao, Jianhong, Zhao, Yongwang, Yao, Peisen, Zeng, Fanlang, Zhan, Bohua, Ren, Kui
Format:	Preprint
Published:	2024
Subjects:	Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs
by: Zhao, Jianhong, et al.
Published: (2024)

HintPilot: LLM-based Compiler Hint Synthesis for Code Optimization
by: Jiang, Hanyun, et al.
Published: (2026)

FormalRTL: Verified RTL Synthesis at Scale
by: Li, Kezhi, et al.
Published: (2026)

Formally Verified Binary-level Pointer Analysis
by: Verbeek, Freek, et al.
Published: (2025)

Verify Implementation Equivalence of Large Models
by: Zhan, Qi, et al.
Published: (2026)

VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models
by: Sevenhuijsen, Merlijn, et al.
Published: (2024)

Whose fault is it anyway? SILC: Safe Integration of LLM-Generated Code
by: Lin, Peisen, et al.
Published: (2024)

Unsafe by Flow: Uncovering Bidirectional Data-Flow Risks in MCP Ecosystem
by: Hou, Xinyi, et al.
Published: (2026)

Formally and Empirically Verified Methodologies for Scalable Hierarchical Full-Stack Systems
by: Liu, Dong
Published: (2025)

Supporting Software Formal Verification with Large Language Models: An Experimental Study
by: Wang, Weiqi, et al.
Published: (2025)

Bidirectional Empowerment of Metamorphic Testing and Large Language Models: A Systematic Survey
by: Zheng, Zheng, et al.
Published: (2026)

ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks
by: Wei, Tianhao, et al.
Published: (2024)

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
by: Hu, Jilin, et al.
Published: (2025)

ExecVerify: White-Box RL with Verifiable Stepwise Rewards for Code Execution Reasoning
by: Tang, Lingxiao, et al.
Published: (2026)

VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications
by: Misu, Md Rakib Hossain, et al.
Published: (2026)

UICopilot: Automating UI Synthesis via Hierarchical Code Generation from Webpage Designs
by: Gui, Yi, et al.
Published: (2025)

Code Clone Detection via an AlphaFold-Inspired Framework
by: Jia, Changguo, et al.
Published: (2025)

Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis
by: Huang, Zhechong, et al.
Published: (2026)

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

SIEVE: Towards Verifiable Certification for Code-datasets
by: Mbodji, Fatou Ndiaye, et al.
Published: (2025)

Debugging Performance Issues in WebAssembly Runtimes via Mutation-based Inference
by: Zeng, Ruiying, et al.
Published: (2026)

SpecGen: Automated Generation of Formal Program Specifications via Large Language Models
by: Ma, Lezhi, et al.
Published: (2024)

Can Large Language Models Model Programs Formally?
by: Chen, Zhiyong, et al.
Published: (2026)

FINER: Enhancing State-of-the-art Classifiers with Feature Attribution to Facilitate Security Analysis
by: He, Yiling, et al.
Published: (2023)

Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement
by: Kobayashi, Tsutomu, et al.
Published: (2024)

SeRe: A Security-Related Code Review Dataset Aligned with Real-World Review Activities
by: Zhao, Zixiao, et al.
Published: (2026)

Bounded Synthesis of Synchronized Distributed Models from Lightweight Specifications
by: Castro, Pablo F., et al.
Published: (2025)

Crash-free Deductive Verifiers
by: Nauta, Wander, et al.
Published: (2026)

Verify Linearizability of Concurrent Stacks
by: Wen, Tangliu
Published: (2021)

Does SWE-Bench-Verified Test Agent Ability or Model Memory?
by: Prathifkumar, Thanosan, et al.
Published: (2025)

Assessing Large Language Models in Comprehending and Verifying Concurrent Programs across Memory Models
by: Jain, Ridhi, et al.
Published: (2025)

CODESYNC: Synchronizing Large Language Models with Dynamic Code Evolution at Scale
by: Wang, Chenlong, et al.
Published: (2025)

CodeDPO: Aligning Code Models with Self Generated and Verified Source Code
by: Zhang, Kechi, et al.
Published: (2024)

A Benchmark for Evaluating Repository-Level Code Agents with Intermediate Reasoning on Feature Addition Task
by: Liu, Shuhan, et al.
Published: (2026)

From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification
by: Erfan, Md, et al.
Published: (2026)

ProfInfer: An eBPF-based Fine-Grained LLM Inference Profiler
by: Zou, Bohua, et al.
Published: (2026)

Formalizing and validating properties in Asmeta with Large Language Models (Extended Abstract)
by: Bombarda, Andrea, et al.
Published: (2026)

Formally Verifying Noir Zero Knowledge Programs with NAVe
by: Antonino, Pedro, et al.
Published: (2026)

Verifier Warnings Do Not Improve Comprehensibility Prediction
by: De Silva, Nadeeshan, et al.
Published: (2026)

OpenComputer: Verifiable Software Worlds for Computer-Use Agents
by: Wei, Jinbiao, et al.
Published: (2026)