In this work, we explore uncertainty estimation as a proxy for correctness in LLM-generated code. To end, adapt two state-of-the-art techniques from natural language generation -- one based on entropy and another mutual information to the domain of code generation. Given distinct semantic properties code, introduce modifications, including equivalence check symbolic execution. Our findings indicate correlation between computed through these correctness, highlighting potential quality...

Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the overridden methods superclasses, leading imprecision during program reasoning. To address this, we advocate a fresh approach OO verification that focuses on distinction relation between cater calls with static dispatching from those dynamic dispatching. We formulate novel specification...

Proving program termination is key to guaranteeing absence of undesirable behaviour, such as hanging programs and even security vulnerabilities denial-of-service attacks. To make checks scale large systems, interprocedural analysis seems essential, which a largely unexplored area research in analysis, where most effort has focussed on difficult single-procedure problems. We present modular for C using template-based summarisation. Our combines context-sensitive, over-approximating forward...

Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present new algorithm based on counter-example guided inductive synthesis automates the design of controllers are correct by construction. The result sound respect to complete range approximations, including time discretization, quantization effects, and finite-precision arithmetic its rounding errors. have our in tool called DSSynth, able automatically...

Non-termination is the root cause of a variety program bugs, such as hanging programs and denial-of-service vulnerabilities. This makes an automated analysis that can prove absence bugs highly desirable. To scale termination checks to large systems, interprocedural seems essential. largely unexplored area research in analysis, where most effort has focussed on small but difficult single-procedure problems. We present modular for C using template-based summarisation. Our combines...

In recent years, separation logic has emerged as a contender for formal reasoning of heap-manipulating imperative programs. Recent works have focused on specialised provers that are mostly based fixed sets predicates. To improve expressivity, we proposed prover can automatically handle user-defined These shape predicates allow programmers to describe wide range data structures with their associated size properties. the current work, shall enhance this by providing support new type...

The HIP and SLEEK systems are aimed at automatic verification of functional correctness heap manipulating programs. is a separation logic based automated system for simple imperative language, able to modularly verify the specifications heap-manipulating specification language allows user defined inductive predicates used model complex data structures. Specifications can contain both constraints various pure like arithmetic constraints, bag constraints. Based on given annotations each...

Automated verification plays an important role for high assurance software. This typically uses a pair of pre/post conditions as formal (but possibly partial) specification each method before it is systematically verified. In this paper, we advocate multiple pairs to be associated with which provides way such used in more scenarios. Multiple specifications are heap-manipulating programs where they can precisely expressed using separation logic. work highlights the importance specifications,...

Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the overridden methods superclasses, leading imprecision during program reasoning. To address this, we advocate a fresh approach OO verification that focuses on distinction relation between cater calls with static dispatching from those dynamic dispatching. We formulate novel specification...

In the current work, we investigate benefits of immutability guarantees for allowing more flexible handling aliasing, as well precise and concise specifications. Our approach supports finer levels control that can mark data structures being immutable through use annotations. By using such annotations to encode guarantees, expect obtain better specifications accurately describe intentions, prohibitions, method. Ultimately, our goal is improving precision verification process, making readable,...

We present a sound and automated approach to synthesizing safe, digital controllers for physical plants represented as time-invariant models. Models are linear differential equations with inputs, evolving over continuous state space. The synthesis precisely accounts the effects of finite-precision arithmetic introduced by controller. uses counterexample-guided inductive synthesis: an generalization phase produces controller that is known stabilize model but may not be safe all initial...

Termination analyses investigate the termination behavior of programs, intending to detect nontermination, which is known cause a variety program bugs (e.g. hanging denial-of-service vulnerabilities). Beyond formal approaches, various attempts have been made estimate programs using neural networks. However, majority these approaches continue rely on methods provide strong soundness guarantees and consequently suffer from similar limitations. In this paper, we move away embrace stochastic...

In this article, we propose a unified framework for designing static analysers based on program synthesis . For purpose, identify fragment of second-order logic with restricted quantification that is expressive enough to model numerous analysis problems (e.g., safety proving, bug finding, termination and non-termination refactoring). As our focus programs use bit-vectors, build decision procedure over finite domains in the form synthesiser. We provide instantiations solving diverse range...