We are interested in automatically proving safety properties of infinite state systems, by combining the classical algebraic approach of (Abdulla,Cerans,Jonsson,Tsay, LICS'96) with deductive techniques exploiting, off-the-shelf, SMT solvers. After briefly recalling the main contributions in that paper leading to the use of backward reachability analysis to prove safety properties and overviewing the long line of works stemming from that seminal paper, we present the notion of array based systems. Such systems are declarative abstractions of several classes of parametrised systems and (sequential) programs manipulating arrays. In the framework of array based systems, key notions (such as configuration, configuration ordering, and monotonic transition) can be adapted and reused in a uniform and simple way. A by-product of this approach is to make readily available deductive techniques (like the synthesis and the use of invariants in the context of the algorithmic verification technique of backward reachability. This is so because the framework retains the modularity and the flexibility typical of logic-based approaches to model-checking (in the same spirit of, e.g.,~\cite{voronkov}). The key feature of array-based systems is that a suitable format for initial/unsafe states and transition formulae can be designed: this format is sufficiently expressive to cover interesting classes of infinite state systems and, at the same time, generates proof obligations (during backward analysis) that can be discharged by instantiation and SMT solving techniques for quantifier-free formulae. To make the theoretical framework useful in practice, powerful heuristics are required to obtain adequate performances: these heuristics concern optimization of the computation of the pre-image, (static and dynamic) filtration of the instantiations that current SMT solvers cannot yet handle efficiently, as well as forward/backward simplification routines. In the last part of the talk, we report our experimental experience with a prototype tool called MCMT, currently under development: we discuss its architecture (especially the interplay between the generation of proof obligations, the computation of pre-images, and the various heuristics) and its integration with the SMT solver Yices; finally we compare MCMT with some state-of-the-art model checkers based on dedicated techniques like PFS. This is joint work with Silvio Ranise.

Cadoli \emph{et al} [BCM04, MC05, CM04] noted the potential of first order automated reasoning for the purpose of analysing constraint models, and reported some encouraging initial experimental results. We are currently pursuing a very similar research program with a view to incorporating deductive technology in a state of the art constraint programming platform. Here we outline our own view of this application direction and discuss new empirical findings on a more extensive range of problems than those considered in the previous literature. While the opportunities presented by reasoning about constraint models are indeed exciting, we also find that there are formidable obstacles in the way of a practicaly useful implementation.

In this paper, we study an efficient equality computation in Connection Tableaux, and give a variant of Brand, Bachmair and Paskevich's modification method, where symmetry transformation rule is never applied. As is well known, effective equality computing is very difficult in a top-down theorem proving framework such as Connection Tableaux, due to a strict restriction to re-writable terms. Brand/Bachmair's modification method with ordering constraints is a well-known remedy for top-down equality computation, and Paskevich adopted the method to Connection Tableaux. However the improved modification method still causes essentially redundant computation which originates in symmetry transformation of equational clauses. The symmetry transformation may produce an exponential number of clauses from a given single clause, which inevitably causes a huge amount of redundant backtracking in Connection Tableaux. In this paper, we study a simple but effective remedy, that is, we abandon such a symmetry transformation of clauses and instead introduce new equality inference rules into Connection Tableaux. These new inference rules can achieve efficient equality computation, without losing the symmetry property of equality, which never cause redundant backtracking nor redundant contrapositive computation. We implemented the proposed method in a sophisticated prover SOLAR which is implemented in JAVA, and show tentative experimental results for TPTP benchmark problems.

The elimination of redundant clauses is an essential part of resolution-based theorem proving in order to reduce the size of the search space. In this paper we focus on ordered fine-grained resolution with selection, a sound and complete resolution-based calculus for monodic first-order temporal logic. The inference rules of the calculus are based on standard resolution between different types of temporal clauses on one hand and inference rules with semi-decidable applicability conditions that handle eventualities on the other hand. We define a subsumption relation on temporal clauses and show how the calculus can be extended with reduction rules that eliminate redundant clauses. We also illustrate how the subsumption relation can be used to simplify the loop search process for eventualities.

This paper studies minimal model generation for SAT instances. In this study, we minimize models with respect to an atom set, and not to the whole atom set. In order to enumerate minimal models, we use an arbitrary SAT solver as a subroutine which returns models of satisfiable SAT instances. In this way, we benefit from the year-by-year progress of efficient SAT solvers for generating minimal models. As an application, we try to solve job-shop scheduling problems by encoding them into SAT instances whose minimal models represent optimum solutions.

Automatic verification of imperative programs that destructively manipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, or trees inductively as solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications.

Today many companies use an ERP (Enterprise Resource Planning) system such as SAP R/3 to run their daily business ranging from financial issues down to the actual control of a production line. Already due to their sheer size, these systems are very complex. In particular, developing and maintaining the authorization setup is a challenge. The goal of our effort is to automatically analyze the authorization setup of an SAP R/3 system against business policies. To this end we formalize the processes, authorization setup as well as the business policies in first-order logic. Then, properties can be (dis)proven fully automatically with our theorem prover Spass. We exemplify our approach on the purchase process, a typical constituent of any SAP R/3 installation.

We study an extension of the relational transducers introduced by Abiteboul, Vianu, Fordham, and Yesha, which are capable of specifying transaction protocols and their interplay with security constraints. We investigate the decidability of relevant verification problems such as goal reachability and log validation.

We develop a formal framework intended as a preliminary step for a single knowledge representation system that provides different representation techniques in a unified way. In particular we consider first-order logic extended by techniques for second-order quantifier elimination and non-monotonic reasoning. Background of the work is literal projection, a generalization of second-order quantification which permits, so to speak, to quantify upon an arbitrary sets of ground literals, instead of just (all ground literals with) a given predicate symbol. In this report, an operator "raise" is introduced that is only slightly different from literal projection and can be used to define a generalization of circumscription in a straightforward and compact way. Some properties of this operator and of circumscription defined in terms of it, also in combination with literal projection, are then shown. A previously known characterization of consequences of circumscribed formulas in terms of literal projection is generalized from propositional to first-order logic and proven thoroughly. A characterization of answer sets according to the stable model semantics in terms of our generalized notion of circumscription is given. This characterization does not recur onto syntactic notions like "reduct" and fixed-point construction and essentially renders in a compact way a "circumscription-like" characterization that has been recently proposed.

This position paper is concerned with a formal representation of lazily evaluated object in contrast to eagerly evaluated and failure objects, where the object is an abstract reference to be made, or not to be linked to. The representation problem may be applied to analysis in Web accessibility. A fixed point theory is adopted for such an analysis.

Instance-based theorem proving techniques have been implemented in many theorem provers. Some of these provers have been shown to prove some problems much faster then resolution-based theorem provers. On the other hand, resolution-based theorem provers continue to lead on other problems. While instance-based theorem provers are believed to have their own advantages over resolution-based theorem provers, their run-time performance relies on the guidance from instance generation heuristics such as semantics, etc.. Static analysis techniques have been studied for many years in the programming language community, most prominently the use of decidable typing to eliminate run-time checks. In analogy, if we regard checking whether an instance is useful for a proof as run-time checks and we can find types that eliminate irrelevant instances, we may also be able to prevent proof searches from checking those irrelevant instances, thereby improving the performance. This paper introduces a method that employs types as heuristics in proof search. The type inference algorithm CFT described in this paper is implemented OSHL-S 0.5.0.

I will introduce the constraint satisfaction problem and show that it unifies a very wide variety of computational problems. I will then discuss the techniques that have been used to analyse the complexity of different forms of constraint satisfaction problem. I will focus on the algebraic approach, explaining the basic ideas and highlighting some of the recent results in this area.