相关论文: Inferring Loop Invariants by Mutation, Dynamic Ana…

We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The type system supports abstract and recursive objects, and is…

We present a technique for automatically weaving structural invariant checks into an existing collection of classes. Using variations on existing design patterns, we use a concise specification to generate from this collection a new set of…

The termination problem of a logic program can be addressed in either a static or a dynamic way. A static approach performs termination analysis at compile time, while a dynamic approach characterizes and tests termination of a logic…

Relational properties describe relationships that hold over multiple executions of one or more programs, such as functional equivalence. Conventional approaches for automatically verifying such properties typically rely on syntax-based,…

Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable gains. To address this gap, we propose WybeCoder, an agentic…

The Move language provides abstractions for programming with digital assets via a mix of value semantics and reference semantics. Ensuring memory safety in programs with references that access a shared, mutable global ledger is difficult,…

Hoare-style verification provides a principled foundation for reasoning about the correctness of quantum programs, but existing approaches do not allow fully automatic verification. While automata-based verification scales well when…

We present in this paper a new technique for generating polynomial invariants, divided in two independent parts : a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a…

Software verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances,…

In recent years, numerous techniques were developed to automatically prove termination of different kinds of probabilistic programs. However, there are only few automated methods to disprove their termination. In this paper, we present the…

The problem of checking whether two programs are semantically equivalent or not has a diverse range of applications, and is consequently of substantial importance. There are several techniques that address this problem, chiefly by…

This dissertation discusses several problems loosely related, because they all involve a verification condition generator. The Boogie language is introduced; the architecture of a verification-generator is described. Then come more…

We introduce a new technique for inferring program invariants that uses symbolic states generated by symbolic execution. Symbolic states, which consist of path conditions and constraints on local variables, are a compact description of sets…

Automatically generating formal specifications including loop invariants, preconditions, and postconditions for legacy code is critical for program understanding, reuse and verification. However, the inherent complexity of control and data…

Modern Java projects increasingly adopt static analysis tools that prevent null-pointer exceptions by treating nullness as a type property. However, integrating such tools into large, existing codebases remains a significant challenge.…

We present a tool for verification of deterministic programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write effects. We implement our tool by encoding programs with…

The correctness of a compiler affects the correctness of every program written in the language, and thus must be thoroughly evaluated. Existing automatic compiler testing methods however either rely on weak oracles (e.g., a program behaves…

We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general loops, (ii) continuous distributions, and (iii) conditioning. To handle…

Synthetic verification techniques such as generating test cases and reward modelling are common ways to enhance the coding capabilities of large language models (LLM) beyond predefined tests. Additionally, code verification has recently…

One of the most attractive features of untyped languages is the flexibility in term creation and manipulation. However, with such power comes the responsibility of ensuring the correctness of these operations. A solution is adding run-time…