Related papers: FO-Complete Program Verification for Heap Logics
Relational verification encompasses research directions such as reasoning about data abstraction, reasoning about security and privacy, secure compilation, and functional specificaton of tensor programs, among others. Several relational…
{log} (read 'setlog') was born as a Constraint Logic Programming (CLP) language where sets and binary relations are first-class citizens, thus fostering set programming. Internally, {log} is a constraint satisfiability solver implementing…
We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract…
Reasoning in language models is difficult to evaluate: natural-language traces are unverifiable, symbolic datasets are too small, and most benchmarks conflate heuristics with inference. We present FOL-Traces, the first large-scale dataset…
In prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their…
This work presents a formalized proof of modal completeness for G\"odel-L\"ob provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation, focusing on our choices…
We advocate a declarative approach to proving properties of logic programs. Total correctness can be separated into correctness, completeness and clean termination; the latter includes non-floundering. Only clean termination depends on the…
For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and permissions. Separation Logic is often extended to include…
We introduce a natural Turing-complete extension of first-order logic FO. The extension adds two novel features to FO. The first one of these is the capacity to add new points to models and new tuples to relations. The second one is the…
We prove completeness results for a wide variety of intuitionistic conditional logics. We do so by first using a canonical model construction obtain completeness with respect to descriptive conditional frames, and then introducing the…
We prove a topological completeness theorem for the modal logic GLP containing operators $\langle\lambda\rangle$ for $\lambda \in$ Ord intended to capture progressively stronger notions of consistency in mathematical theories. We show that,…
We introduce a method of verifying termination of logic programs with respect to concrete queries (instead of abstract query patterns). A necessary and sufficient condition is established and an algorithm for automatic verification is…
Logical formalisms such as first-order logic (FO) and fixpoint logic (FP) are well suited to express in a declarative manner fundamental graph functionalities required in distributed systems. We show that these logics constitute good…
We present verification methods for logic programs with delay declarations. The verified properties are termination and freedom from errors related to built-ins. Concerning termination, we present two approaches. The first approach tries to…
Most automated program verifiers for separation logic use either symbolic execution or verification condition generation to extract proof obligations, which are then handed over to an SMT solver. Existing verification algorithms are…
Incorrectness Separation Logic (ISL) is a proof system designed to automate verification and detect bugs in programs manipulating heap memories. In this study, we extend ISL to support variable-length array predicates and pointer…
This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic…
Theoretical foundations of compositional reasoning about heaps in imperative programming languages are investigated. We introduce a novel concept of compositional symbolic memory and its relevant properties. We utilize these formal…
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,…
The primary purpose of this article is to show that a certain natural set of axioms yields a completeness result for continuous first-order logic. In particular, we show that in continuous first-order logic a set of formulae is (completely)…