Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1301.0037

Formal Verification, Engineering and Business Value

Ralf Huuck
View original source ↗Read source document ↗Export metadata ↓

Abstract

How to apply automated verification technology such as model checking and static program analysis to millions of lines of embedded C/C++ code? How to package this technology in a way that it can be used by software developers and engineers, who might have no background in formal verification? And how to convince business managers to actually pay for such a software? This work addresses a number of those questions. Based on our own experience on developing and distributing the Goanna source code analyzer for detecting software bugs and security vulnerabilities in C/C++ code, we explain the underlying technology of model checking, static analysis and SMT solving, steps involved in creating industrial-proof tools.

Explore related subjects

cs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Ralf Huuck. 2013-01-01. Formal Verification, Engineering and Business Value. https://doi.org/10.4204/eptcs.105.1

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Estimating the Energy Footprint of Software Systems: a Primer

In Green Software Development, quantifying the energy footprint of a software system is one of the most basic activities. This documents provides a high-level overview of how the energy footprint of a software system can be estimated to support Green Software Development. We introduce basic concepts in the area, highlight methodological issues that must be accounted for when conducting experiments, discuss trade-offs associated with different estimation approaches, and make some practical considerations. This document aims to be a starting point for researchers who want to begin conducting work in this area.

cs.SE↗
arXiv2026

ECO: An LLM-Driven Efficient Code Optimizer for Warehouse Scale Computers

This paper introduces ECO, a system that automatically modifies source code to improve performance at scale. ECO overcomes the localization problem by combining fleet-wide continuous profiling to identify performance-critical code with an embedding-based search to pinpoint specific optimization candidates, guided by a mined dictionary of performance anti-patterns. It overcomes the reliability problem through a multi-stage verification approach that uses automated testing, LLM-based self-review, and post-deployment monitoring to ensure changes are both correct and effective. Fully productionized and deployed within Google's hyperscale production fleet, ECO has successfully landed over 6,400 commits, changing more than 25,000 lines of production code. Incorrect changes are caught before they are submitted to production, and 99.5% of the submitted commits did not cause any rollbacks. These optimizations have resulted in savings equivalent to several hundred thousand normalized CPU cores, showing that ECO makes LLM-based optimization both practical at scale and highly impactful in real-world settings.

cs.SE↗
arXiv2026

From Procedural Skills to Strategy Genes: Towards Experience-Driven Test-Time Evolution

This beta technical report asks how reusable experience should be represented so that it can function as effective test-time control and as a substrate for iterative evolution. We study this question in 4.590 controlled trials across 45 scientific code-solving scenarios. We find that documentation-oriented Skill packages provide unstable control: their useful signal is sparse, and expanding a compact experience object into a fuller documentation package often fails to help and can degrade the overall average. We further show that representation itself is a first-order factor. A compact Gene representation yields the strongest overall average, remains competitive under substantial structural perturbations, and outperforms matched-budget Skill fragments, while reattaching documentation-oriented material usually weakens rather than improves it. Beyond one-shot control, we show that Gene is also a better carrier for iterative experience accumulation: attached failure history is more effective in Gene than in Skill or freeform text, editable structure matters beyond content alone, and failure information is most useful when distilled into compact warnings rather than naively appended. On CritPt, gene-evolved systems improve over their paired base models from 9.1% to 18.57% and from 17.7% to 27.14%. These results suggest that the core problem in experience reuse is not how to supply more experience, but how to encode experience as a compact, control-oriented, evolution-ready object.

cs.SE↗