Trace-Based Execution-Level Observability of VDM-SL Specifications

VeriLucid: A Verification-aware Data-plane Programming Language

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.

Engineering Verified Model Transformations through a Proof-Based Language Workbench

Model-driven transformations play a central role in MDE processes, yet their correctness is most often validated through testing or simulation. However, in contexts where critical scenarios may compromise system integrity or certification objectives, stronger guarantees are necessary. This paper investigates how the B method can support transformation engineering through verified formal specifications. To this end, we developed BCerT, an extension of the Meeduse language workbench, originally dedicated to the formal modeling of domain-specific languages. In our approach, transformations are defined as B operations or B events, allowing animation and model checking with ProB, as well as theorem proving with Atelier B. We discuss three complementary specification strategies: (i) a rule-oriented modeling approach optionally controlled with CSP||B; (ii) a property-driven operational B specification in which the transformation is expressed as a relation constrained by invariants; and (iii) an Event-B system capturing the transformation as atomic events focused on the end state. The approach is illustrated through two applications: the verification of a Truth Tables to Binary Decision Diagrams transformation presented at the Transformation Tool Contest, and the development of U2BCerT, a certified transpiler from UML state machines to Event-B.

Can Formal Specifications Be Synthesized from Tests Alone?

Formal specifications offer strong guarantees, but remain costly to write manually. Recent LLM-based approaches automate this by inferring specifications from source code, yet their reliance on white-box access poses barriers to industrial adoption due to intellectual property risks and deployment costs. Our approach uses LLMs to infer candidate specifications solely from test code and dynamic execution traces: the LLM observes only the program interface, selected inputs, and corresponding outputs or state changes, while the implementation internals remain hidden. Candidate specifications are validated locally using bounded model checking, with feedback guiding iterative refinement. Initial results on the SpecGenBench benchmark suggest that tests can guide LLMs towards meaningful Java Modeling Language specifications, while also highlighting checker compatibility and diagnostic feedback as key challenges for reliable refinement.

Towards Extensible, Auditable, and Modular Measurement Specification and Execution in Computer Networking

We present the Measurement Template Library (Mtl), a Go library and runtime for specifying and executing measurements. Mtl provides a framework for specifying and executing extensible, modular, and auditable measurements using generic programming techniques. By leveraging the notion of polymorphic measurement programs, we show how to lift measurement tools/probes into a typed computational context and model. This lifting supports the structured definition and refinement of common data structures, algorithms, and concurrency and interleaving semantics which appear in measurement work. In short, we show that measurement points (i.e., the Linux ping utility, scamper, or RIPE Atlas) are types, and measurements are type expressions.

Forbench: Symbolic Simulation Helps Make Your Testbench More Formal

Simulation remains the dominant approach in pre-silicon verification due to its ease of deployment and intuitive workflow. However, as simulation only explores a limited subset of possible execution traces within feasible time budgets, it often fails to explore rare corner cases, leaving latent bugs undetected. In contrast, formal verification offers mathematically rigorous guarantees of correctness. However, its practical adoption is constrained, not only by the scalability challenges over large-scale designs, but also by the change of mindset from stimulus-driven operations to the sequence-centric axiomatic view of design behaviors, introducing extra difficulty of writing precise properties to capture the exact verification intent. This paper aims to lower the barrier of applying formal methods in verification, by making simulation"more formal."It introduces Forbench, a word-level symbolic simulation framework that retains the familiar execution semantics of simulation but augments it with solver-backed symbolic signals and state transitions, enabling systematic exploration of RTL behaviors under symbolic inputs and conditions. It offers a Python interface, similar to the existing simulation-based frameworks, for defining constraints, coordinating symbolic (co-)simulations, and performing property checks. In additional to this more accessible interface, experiments also show that Forbench achieves notably speed-up over prior symbolic methods without the loss of coverage.

Remote Concolic Multiverse Debugging (Artifact)