 On local reasoning in verification
(with Carsten Ihlemann and Swen Jacobs)
 Proceedings of TACAS'08, LNCS 4963, pages 265281, Springer 2008.
 Abstract:
We present a general framework which allows to identify
complex theories important in verification for which efficient
(hierarchical and modular) reasoning methods exist.
The framework we present is based on a general notion of locality.
We show that locality considerations allow us to obtain parameterized
decidability and complexity results for many (combinations of)
theories important in verification in general and in the
verification of parametric systems in particular.
We give numerous examples of local theory extensions; in particular
we show that several theories of data structures studied in the
verification literature are local extensions of a base theory.
The general framework we use allows us to identify situations in
which some of the syntactical restrictions imposed in previous
papers can be relaxed.
Download PostScript,
PDF
Extends the following paper:
Viorica SofronieStokkermans, Carsten Ihlemann, and Swen Jacobs,
" Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
" In Deduction and Decision Procedures, Dagstuhl Seminar Proceedings,
F. Baader, B. Cook, J. Giesl, R. Nieuwenhuis (Eds.) IBFI, Schloss Dagstuhl, Germany, December 2007. Download
 Verifying CSPOZDC specifications with complex data types and timing parameters
(with Johannes Faber and Swen Jacobs)
 Proceedings of IFM 2007: Integrated Formal Methods, LNCS 4591, pages 233252, Springer, 2007.
 Abstract: We extend existing verification methods for CSPOZDC
to reason about realtime systems with complex data types and timing
parameters. We show that important properties of systems can be encoded in
wellbehaved logical theories in which hierarchical reasoning is possible.
Thus, testing invariants and bounded model checking can be reduced to
checking satisfiability of ground formulae over a simple base theory.
We illustrate the ideas by means of a simplified version of a case study
from the European Train Control System.
Download PostScript,
PDF
 Constraint Solving for Interpolation
(with Andrey Rybalchenko)
 VMCAI'2007: Verification, Model Checking,
and Abstract Interpretation, LNCS 4349, pages 346362. 2007.
 Abstract:
Interpolation is an important component of recent methods for
program verification. It provides a natural and effective means for
computing separation between the sets of `good' and `bad' states.
The existing algorithms for interpolant generation are proofbased:
They require explicit construction of proofs, from which
interpolants can be computed. Construction of such proofs is a
difficult task. We propose an algorithm for the generation of
interpolants for the combined theory of linear arithmetic and
uninterpreted function symbols that does not require a priori
constructed proofs to derive interpolants. It uses a reduction of
the problem to constraint solving in linear arithmetic, which allows
application of existing highly optimized Linear Programming solvers
in blackbox fashion. We provide experimental evidence of the
practical applicability of our algorithm.
Download
PDF
 Applications of hierarchical reasoning in the verification of complex systems
(with Swen Jacobs)

Electronic Notes in Theoretical Computer Sciences 174/8
(Special issue dedicated to PDPAR'06), pages 3954, 2007.
 Abstract: In this paper we show how hierarchical reasoning can be used
to verify properties of complex systems. Chains of local theory
extensions are used to model a case study taken from the
European Train Control System (ETCS) standard, but considerably
simplified. We show how testing invariants and bounded model
checking can automatically be reduced to checking satisfiability
of ground formulae over a base theory.
Download
PDF
This paper extends:
 Applications of hierarchical reasoning in the verification of complex systems
 Proceedings of the Fourth International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'06), pages 1526, 2006.
Download PDF
 Local reasoning in verification
 Proceedings of the Verification Workshop VERIFY'06, pages 128145, 2006.
 Abstract: he goal of this paper is to show, concretely,
the wide applicability of results on hierarchical reasoning in local
theory extensions in verification. We start with an uptodate survey
of our results on reasoning in local theory extensions, ranging from
characterizations of locality to interpolation. We then provide several
examples, emphasizing theories occurring in a natural way in verification.
Finally, we present several applications  some already existing in the
literature, others obtained during the work in the AVACS project  where
such theories occur in a natural way.
Download PostScript,
PDF
 Automated reasoning in some local extensions of ordered structures
 with Carsten Ihlemann, Journal of MultipleValued Logics and Soft Computing, To appear.
 Abstract
We give a uniform method for automated reasoning in
several types of extensions of ordered algebraic structures
(definitional extensions, extensions with boundedness
axioms or with monotonicity axioms). We show that such
extensions are local and, hence, efficient methods for
hierarchical reasoning exist in all these cases.
Download: preliminary version
PDF.
 Automated reasoning in some local extensions of ordered structures
 with Carsten Ihlemann, Proceedings of ISMVL'07, IEEE Press, paper 1, 2007.
 Abstract
We give a uniform method for automated reasoning in
several types of extensions of ordered algebraic structures
(definitional extensions, extensions with boundedness
axioms or with monotonicity axioms). We show that such
extensions are local and, hence, efficient methods for
hierarchical reasoning exist in all these cases.
Download: preliminary version
PDF.

On unification in certain finitely generated varieties of algebras
 Proceedings of UNIF 2007,extended abstract.

On unification for Bounded Distributive Lattices
 ACM TOCL 8(2), 2007.
 Abstract:
We give a method for deciding unifiability in the variety
of bounded distributive lattices.
For this, we reduce the problem of deciding whether a
unification problem ${\cal S}$ has a solution to the
problem of checking the satisfiability of a set
$\Phi_{\cal S}$ of ground clauses.
This is achieved by using a structurepreserving
translation to clause form.
The satisfiability check can then be performed
either by a resolutionbased theorem prover or
by a SAT checker. We apply the method to
unification with free constants and to unification
with linear constant restrictions, and show that,
in fact, it yields a decision procedure for the positive
theory of the variety of bounded distributive lattices.
We also consider the problem of unification over
(i.e.\ in an algebraic extension of) the free lattice.
Complexity issues are also addressed.
Download PostScript (ACM TOCL website)
PostScript (own version)
BibTexEntry.

Resolutionbased decision procedures for the positive theory of some finitely generated varieties of algebras
 Proceedings of the 34th International Symposium on MultipleValued Logic (ISMVL2004), Toronto, Canada, May 1922, 2004, IEEE Computer Society, Los Alamitos, 2004, to appear.
 Abstract
In this paper we give resolutionbased decision procedures for the positive theory of certain finitelygenerated varieties of algebras. The method is based on the existence of representation theorems for such classes of algebras..
Download: gzipped PostScript,
BibTexEntry

Resolutionbased decision procedures for the universal theory of some classes of distributive lattices with operators
 Journal of Symbolic Computation 36, 6, 891924, 2003.
 Abstract:
We establish a link between the satisfiability of universal sentences with
respect to classes of distributive lattices with operators and their
satisfiability with respect to certain classes of relational structures.
This justifies a method for structurepreserving translation to clause form
of universal sentences in such classes of algebras. We show that refinements
of resolution yield decision procedures for the universal theory of some such
classes. In particular, we obtain exponential space and time decision
procedures for the universal clause theory of (i) the class of all bounded
distributive lattices with operators satisfying a set of (generalized)
residuation conditions, (ii) the class of all bounded distributive lattices
with operators, and a doublyexponential time decision procedure for the
universal clause theory of the class of all Heyting algebras.
Download: gzipped .ps file,
BibTexEntry.

On uniform word problems involving bridging operators on distributive lattices
 Proceedings
of TABLEAUX 2002, July 2002, Copenhagen, LNCS 2381, 235250. Springer, 2002.
 Abstract:
In this paper we analyze some fragments of the universal theory
of distributive lattices with many sorted bridging operators.
Our interest in such algebras
is motivated by the fact that, in description logics,
numerical features are often expressed by using maps that
associate numerical values to sets (more generally,
to lattice elements).
We first establish a link between satisfiability
of universal sentences
with respect to algebraic models and satisfiability with respect to
certain classes of relational structures.
We use these results for giving a method for
translation to clause form of universal sentences,
and provide some decidability results based on the use of
resolution or hyperresolution.
Links between hyperresolution and tableau methods are also
discussed, and a tableau procedure for checking satisfiability
of formulae of type $t_1 \leq t_2$ is obtained by using a
hyperresolution calculus.
Download: Pdf file,
BibTexEntry.

On unification for Bounded Distributive Lattices
 Proceedings of CADE17, LNAI 1831, pages 465481, 2000, Springer Verlag.
 Abstract:
We give a resolutionbased procedure for deciding unifiability in the
variety of bounded distributive lattices. The algorithm consists of
the following steps:
(i) Structurepreserving translation to clause form.
Testing the satisfiability of a unification problem $S$ is reduced to
the problem of checking the satisfiability of a set $\Phi_S$ of clauses.
Expressing $\Phi_S$ as a set of constrained clauses further simplifies
the representation of the problem.
(ii) Ordered resolution with selection for (constrained) clauses is used for
testing the satisfiability of $\Phi_S$.
Step 1 uses the description of the free bounded distributive lattice over
$C$ as the lattice of all upwardssets of (P(C), \subseteq), which is a
consequence of the Priestley representation theorem.
We also show that similar ideas can be used for unification with linear
constant restrictions.
The main advantage of our approach is that it makes it much easier to
treat the unification problem for bounded distributive lattices, by using
results in resolution theory. Using results of Baader and Schulz, our results
also show that resolution can be used for deciding the positive theory of
${\sf D}_{01}$.
Download: PostScript,
BibTexEntry

On the Universal Theory of Varieties of Distributive Lattices
with Operators: Some Decidability and Complexity Results
 Proceedings of CADE16, LNAI 1632, pages 157171, Springer Verlag, 1999.
 Abstract:
In this paper we give a method for automated theorem proving in the
universal theory of certain varieties of distributive lattices
with wellbehaved operators. For this purpose, we use extensions of
Priestley's representation theorem for distributive lattices.
We first establish a link between satisfiability of universal sentences
with respect to varieties of distributive lattices with operators and
satisfiability with respect to certain classes of relational structures.
We then use these results for giving a method for translation to clause
form of universal sentences in such varieties, and obtain decidability
and complexity results for the universal theory of some such varieties.
The advantage is that we avoid the explicit use of the full algebraic
structure of such lattices, instead using sets endowed with a reflexive
and transitive relation and with additional functions and relations.
We first studied this type of relationships in the context of finitelyvalued
logics and then extended the ideas to more general nonclassical logics.
This paper shows that the idea is much more general. In particular, the method
presented here subsumes both existing methods for translating modal logics to
classical logic and methods for automated theorem proving in finitelyvalued
logics based on distributive lattices with operators.
Download:
PostScript,
BibTexEntry
 The results are extended in:

Resolutionbased decision procedures for the universal theory of some classes of distributive lattices with operators
 Research Report
MPII20012005
MaxPlanckInstitut füormatik, September 2001, ISSN 0946011X,

On unification in certain finitely generated varieties of algebras
 Proceedings of
UNIF 2007,extended abstract.
 Abstract: We present resolutionbased decision procedures for the positive theory of certain finitelygenerated varieties of algebras. The method is based on the existence of natural dualities for such classes of algebras.
Download: PDF Proceedings of
UNIF 2007.

On unification for Bounded Distributive Lattices
 ACM TOCL 8(2), 2007.
 Abstract:
We give a method for deciding unifiability in the variety
of bounded distributive lattices.
For this, we reduce the problem of deciding whether a
unification problem ${\cal S}$ has a solution to the
problem of checking the satisfiability of a set
$\Phi_{\cal S}$ of ground clauses.
This is achieved by using a structurepreserving
translation to clause form.
The satisfiability check can then be performed
either by a resolutionbased theorem prover or
by a SAT checker. We apply the method to
unification with free constants and to unification
with linear constant restrictions, and show that,
in fact, it yields a decision procedure for the positive
theory of the variety of bounded distributive lattices.
We also consider the problem of unification over
(i.e.\ in an algebraic extension of) the free lattice.
Complexity issues are also addressed.
Download PostScript (ACM TOCL website)
PostScript (own version)
BibTexEntry.

Resolutionbased decision procedures for the positive theory of some finitely generated varieties of algebras
 Proceedings of the 34th International Symposium on MultipleValued Logic (ISMVL2004), Toronto, Canada, May 1922, 2004, IEEE Computer Society, Los Alamitos, 2004.
 Abstract
In this paper we give resolutionbased decision procedures for the positive theory of certain finitelygenerated varieties of algebras. The method is based on the existence of representation theorems for such classes of algebras..
Download: gzipped PostScript,
BibTexEntry

On unification for Bounded Distributive Lattices
 Proceedings of CADE17, LNAI 1831, pages 465481, 2000, Springer Verlag.
 Abstract:
We give a resolutionbased procedure for deciding unifiability in the
variety of bounded distributive lattices. The algorithm consists of
the following steps:
(i) Structurepreserving translation to clause form.
Testing the satisfiability of a unification problem $S$ is reduced to
the problem of checking the satisfiability of a set $\Phi_S$ of clauses.
Expressing $\Phi_S$ as a set of constrained clauses further simplifies
the representation of the problem.
(ii) Ordered resolution with selection for (constrained) clauses is used for
testing the satisfiability of $\Phi_S$.
Step 1 uses the description of the free bounded distributive lattice over
$C$ as the lattice of all upwardssets of (P(C), \subseteq), which is a
consequence of the Priestley representation theorem.
We also show that similar ideas can be used for unification with linear
constant restrictions.
The main advantage of our approach is that it makes it much easier to
treat the unification problem for bounded distributive lattices, by using
results in resolution theory. Using results of Baader and Schulz, our results
also show that resolution can be used for deciding the positive theory of
${\sf D}_{01}$.
Download: PostScript,
BibTexEntry