Aug 2026· Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication· 0 citations· 46 references
Computer Science
TL;DR
This paper introduces the first verification-aware data-plane language: VeriLucid, which aims to unify programming and specification in one high-level language, with built-in proof automation.
Abstract
Correctness is important in data-plane programs, which run on critical infrastructure connecting millions of users. Verification helps programmers build correct software, but current data-plane tools can only check simple properties or require immense programmer effort. As a solution, this paper introduces the first verification-aware data-plane language: VeriLucid. The core idea is to unify programming and specification in one high-level language, with built-in proof automation. Integration makes it natural for programmers to use verification continuously throughout development, like unit testing but with strong guarantees. In evaluation, we show that VeriLucid requires 10X less programmer effort, in terms of lines of code, than other verification tools with comparable expressiveness.
Compilomorphic fuzzing is introduced, a new validation approach that turns a compiler into its own test oracle via structure-preserving transformations over programs and structured inputs, establishing a practical, model-free foundation for validating compilers in critical DSL domains.
Cloq is introduced, the first dependently typed, machine-checked framework for verifying timing properties of raw (stripped) machine code within the Rocq interactive theorem-proving environment, and provides high-assurance, high-precision timing guarantees that verify that real-time systems and cryptographic algorithms...
Experimental results show that Chameleon can augment P4 programs with small one-time preprocessing and compilation overheads, and supports millisecond-level runtime configuration operations for verification requirements.
Ying Yao, Le Tian, Yu-Xiang Hu· Conference on Applications,...· 0 citations
The Trusted LLM (T-LLM) Compiler is presented, which proposes an advancement in compiler technology through a collaborative effort involving high-level LLM code transformations, traditional compilers, and verification tools and facilitates iterative code optimization efforts with verification strategies that enable cor...
Zahra Fazel, Sunanda Gamage, Shayan Shirahmad Gale Bagi et al.· 0 citations
Pretty Verifier significantly improves the developer’s experience and facilitates the resolution of critical security issues by improving the readability of eBPF verifier messages and strengthening their connection to the original C source code.
Rosario Rizza, Riccardo Sisto, Fulvio Valenza· Information and Software Tec...· 0 citations
The recording and utilization of execution traces of assignments, operation calls, and return statements are proposed to make the internal behavior of operations persistent and analyzable as state-based models.
T. Oda, Han-Myung Chang· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
