相关论文: Automating Unrealizability Logic: Hoare-Style Proo…

Formal verification provides strong guarantees of correctness of software, which are especially important in safety or security critical systems. Hoare logic is a widely used formalism for rigorous verification of software against…

In systems verification we are often concerned with multiple, inter-dependent properties that a program must satisfy. To prove that a program satisfies a given property, the correctness of intermediate states of the program must be…

The unification algorithm has long been a target for program synthesis research, but a fully automatic derivation remains a research goal. In deductive program synthesis, computer programming is phrased as a task in theorem proving; a…

Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory…

Verifying a real-world program's functional correctness can be decomposed into (1) a refinement proof showing that the program implements a more abstract high-level program and (2) an algorithm correctness proof at the high level.…

Fundamentally, every static program analyser searches for a proof through a combination of heuristics providing candidate solutions and a candidate validation technique. Essentially, the heuristic reduces a second-order problem to a…

Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a novel property-driven verification method that first infers…

Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model checking, abstract interpretation, etc. The underlying synthesis problem, however, is challenging and…

Probabilistic Hoare logic (PHL) is an extension of Hoare logic and is specifically useful in verifying randomized programs. It allows researchers to formally reason about the behavior of programs with stochastic elements, ensuring the…

An uninterpreted program (UP) is a program whose semantics is defined over the theory of uninterpreted functions. This is a common abstraction used in equivalence checking, compiler optimization, and program verification. While simple, the…

Many natural program correctness properties can be stated in terms of symmetries, but existing formal methods have little support for reasoning about such properties. We consider how to formally verify a broad class of symmetry properties…

Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in…

Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct…

We introduce APPL (Abstract Program Property Logic), a unifying Hoare-style logic that subsumes standard Hoare logic, incorrectness logic, and several variants of Hyper Hoare logic. APPL provides a principled foundation for abstract program…

We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted functions and relations, and abide by a…

While there is a long tradition of reasoning about (non)termination in program analysis, specialized logics are typically needed to give different termination criteria. This includes partial correctness, where termination is not guaranteed,…

In previous work, we have introduced a contract-based real- izability checking algorithm for assume-guarantee contracts involving infinite theories, such as linear integer/real arith- metic and uninterpreted functions over infinite domains.…

O'Hearn's Incorrectness Logic (IL) has sparked renewed interest in static analyses that aim to detect program errors rather than prove their absence, thereby avoiding false alarms -- a critical factor for practical adoption in industrial…

Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables the automated construction of proven-to-be-correct programs,…

Rust is a modern programming language that guarantees memory safety and the absence of data races with a strong type system. We present RustyDL, a program logic for Rust, as a foundation for an auto-interactive, deductive verification tool…