相关论文: Detecting Unsolvable Queries for Definite Logic Pr…
This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic,…
Program semantics can often be expressed as a (many-sorted) first-order theory S, and program properties as sentences $\varphi$ which are intended to hold in the canonical model of such a theory, which is often incomputable. Recently, we…
Disjunctive finitary programs are a class of logic programs admitting function symbols and hence infinite domains. They have very good computational properties, for example ground queries are decidable while in the general case the stable…
The saturation-based reasoning methods are among the most theoretically developed ones and are used by most of the state-of-the-art first-order logic reasoners. In the last decade there was a sharp increase in performance of such systems,…
This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the…
When solving combinatorial problems, pruning symmetric solution candidates from the search space is essential. Most of the existing approaches are instance-specific and focus on the automatic computation of Symmetry Breaking Constraints…
First-order logic is a natural way of expressing the properties of computation, traditionally used in various program logics for expressing the correctness properties and certificates. Subsequently, modern methods in the automated inference…
Synthesizing a program that realizes a logical specification is a classical problem in computer science. We examine a particular type of program synthesis, where the objective is to synthesize a strategy that reacts to a potentially…
We present a novel and well automatable approach to formal verification of programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain evaluations. First, we reduce this problem to…
Recent years have seen tremendous growth in the amount of verified software. Proofs for complex properties can now be achieved using higher-order theories and calculi. Complex properties lead to an ever-growing number of definitions and…
The problem of determining whether a probabilistic program terminates almost surely (i.e.~with probability one) is undecidable, and actually $\Pi^0_2$-complete. For this reason, a growing literature has explored classes of programs for…
On one hand, termination analysis of logic programs is now a fairly established research topic within the logic programming community. On the other hand, non-termination analysis seems to remain a much less attractive subject. If we divide…
Satisfiability-based automated reasoning is an approach that is being successfully used in software engineering to validate complex software, including for safety-critical systems. Such reasoning underlies many validation activities, from…
A sufficient and necessary condition is given under which least Herbrand models exactly characterize the answers of definite clause programs. To appear in Theory and Practice of Logic Programming (TPLP).
The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that computes answers in logic programming, and the declarative…
In the logic programming paradigm, a program is defined by a set of methods, each of which can be executed when specific conditions are met during the current state of an execution. The semantics of these programs can be elegantly…
Efficient omission of symmetric solution candidates is essential for combinatorial problem-solving. Most of the existing approaches are instance-specific and focus on the automatic computation of Symmetry Breaking Constraints (SBCs) for…
Formalisms based on temporal logics interpreted over finite strict linear orders, known in the literature as finite traces, have been used for temporal specification in automated planning, process modelling, (runtime) verification and…
We report on work in progress on automatic procedures for proving properties of programs written in higher-order functional languages. Our approach encodes higher-order programs directly as first-order SMT problems over Horn clauses. It is…
SMT solvers have been used successfully as reasoning engines for automated verification and other applications based on automated reasoning. Current techniques for dealing with quantified formulas in SMT are generally incomplete, forcing…