Hélène Collavizza

Mike Gordon
email: mike.gordon@cl.cam.ac.uk

Integration of Theorem-proving and Constraint Programming for Software Verification

A novel approach to program verification combining constraint programming methods with theorem proving is proposed. Starting from an initial symbolic state and precondition, a program is symbolically executed along all feasible paths and then a post-condition is proved or refuted on the final states. Symbolic execution is by mechanised reduction of a formal semantics applied to the program. The constraint solver incrementally prunes execution paths by testing if conditions are feasible in the current state. At the end of each path, deductive theorem proving and constraint solving are tried in sequence. If the theorem prover fails, the constraint solver provides a decision procedure for a finite subset of integers. It can also efficiently compute counter-examples. There is a flexible trade-off between speed and assurance. Oracles may be employed as solvers to boost efficiency, but slower formal tools (automatic or interactive) can be used when higher assurance is needed, or the proof requires manual guidance. Theorems proved with oracles are tagged, so the weakest link in a verification is apparent. The approach has been successfully applied to textbook algorithms and first results show that it is quite efficient. On simple examples most of the proofs are done by the theorem prover, the constraint solver is mainly used to compute counter-examples and check non-linear expressions.

Introduction

Our aim is to link together two different and complementary approaches to program verification: (i) constraint solving applied to symbolic execution paths (bounded model checking) and (ii) theorem proving applied to formal semantic specifications (proof of functional correctness).

There is a spectrum of degrees of formality. At one end everything is coded without any mechanical link to formal specifications (e.g. in Java). The formal semantics is just documentation and the only link between it and the verifier code is in the mind of the programmer. At the other extreme everything is mechanically deduced from a formalisation of the programming language semantics. In the middle -this is the approach described in this paper -lies a mixture of trusted code and theorem proving. Our aim is to explore efficiency/assurance trade-offs obtained by using formal theorem proving tools within a larger verification framework.

The rest of the paper is structured as follows: first a simple example is used to illustrate key ideas. Next we explain our heuristics for combining constraint solving with theorem proving. We then discuss how theorems derived from a formal semantics are used to generate symbolic execution paths. Finally, experimental results are given (including comparisons with previous work).

Example: AbsMinus

Consider the Java class AbsMinus in Figure 1. This computes the absolute value of the subtraction of inputs i and j. Lines 2-4 give its specification in JML (Java Modelling Language [START_REF]JML[END_REF]), where ensures is the postcondition and \result represents the value returned by the program. The JML specification of AbsMinus is first parsed into a Hoare triple. The translation is not formal, so it is necessary to trust that it faithfully extracts the Java semantics.

The representation resulting from the initial parsing phase contains three parts: a precondition, a program and a postcondition, which are arguments to a predicate RSPEC that specifies the meaning of the Hoare triple (see Figure 2): ∀p c r. RSPEC p c r = ∀s 1 s 2 . p s 1 ∧ EVAL c s 1 s 2 ⇒ r s 1 s 2 EVAL c s 1 s 2 (see Section 4.1) is true if executing c in an initial state s 1 results in a final state s 2 . The JML precondition is parsed to a predicate on the initial state, represented by a λ-expression. Since there is no explicit precondition in AbsMinus, the parser returns the always-true predicate (λ. T). The program is represented using conventional abstract syntax constructors: Seq is the sequential execution of instructions, Cond is the conditional and Skip is the null instruction. The meaning of these constructors are specified in the definition of EVAL. The postcondition is a relation between the initial and final states, represented as "λs1 s2. • • • ". Such VDM-style relational postconditions reduce the need for ghost (auxiliary) variables and can neatly represent JML's \old construct. States are finite maps from strings to values. Values may be scalars (currently just integers) or arrays (finite maps from indexing numbers to values). Details concerning arrays are omitted from this paper. We will write finite maps in the form [x 1 → v 1 ; . . . ; x n → v n ] and the result of looking up a variable x in a map m as m^x (the actual notations used in the theorem prover are more cumbersome as they explicitly indicate whether values are scalars or arrays). The symbolic execution of AbsMinus proceeds as follows:

A. Compute an initial symbolic state: C. Start with an initial path that contains no condition and thus is equal to T.

["i" → i; "j" → j; "k" → k; "Result" → Result; "result" → result]
class AbsMinus { /*@ ensures ((i < j) ==> (\result == j-i)) && ((i >= j) ==> (\result == i-j)); @*/ int absMinus (int i, int j) { int result; int k = 0; if (i <= j) k = k+1; if (k == 1 && i != j) result = j-i; else result = i-j; // ERROR: result = j-i; return result;}} The new state is computed directly from a small-step semantics that has been formally verified (by interactive proof) to correspond to the big-step reference semantics (see part 4.1). The new state is:

["i" → i; "j" → j; "k" → k; "Result" → Result; "result" → 0] (b)
The next instruction (line 6) is executed in the same way to get state:

["i" → i; "j" → j; "k" → 0; "Result" → Result; "result" → 0] (c) The conditional instruction (line 8) is executed using a heuristic that combines the theorem prover (HOL4) and constraint solver to test if the path is feasible (see part 3.2). The condition is first evaluated on the current state, using the semantics of Boolean operations defined for the language (see part 4.1). The result is: i <= j. We then test if this condition is possible according to the precondition (which is T) and the current path (which is also T). First the constraint solver is called to solve the constraint system: i[-128..127] <= j[-128..127]. It trivially finds solution (i,-128) (j,-128) (note that the integer format has been fixed to 8 bits here using the heuristic described in 3.2). So condition i <= j is added into the current path and execution continues on the 'then' part of the conditional instruction (line 10). (d) (Assign "k" (Plus (Var "k") (Const 1))) (line 10) is executed to get:

["i" → i; "j" → j; "k" → 1; "Result" → Result; "result" → 0] (e) The next instruction (line 13) is a conditional branching on:

(And (Equal (Var "k") (Const 1)) (Not (Equal (Var "i") (Var "j")))).
This is is evaluated on the current state to ¬(i = j) using the semantics of Boolean expressions. The constraint solver is called to test if this condition is possible on the current path. The constraint system is: which has a trivial solution. So i=j is added into the current path and execution continues on the 'then' part (line 16). (f) The two last instructions on the path (line 16 and line 18) are executed and the end of the path "i<=j ∧ ¬(i=j)" is reached with symbolic state: ["i" → i; "j" → j; "k" → 1; "Result" → j-i; "result" → j-i]. (Not (Equal (Var "i") (Var "j")))) 16

(Assign "result" (Sub (Var "j") (Var "i"))) 17

(Assign "result" (Sub (Var "i") (Var "j")))) 18

(Assign "Result" (Var "result")))))) 19 (λs1 s2. (s1^"i" < s1^"j" ==> s2^"Result" = s1^"j" -s1^"i") ∧ 20 (s1^"i" >= s1^"j" ==> s2^"Result" = s1^"i" -s1^"j"))

Fig. 2. Relational specification of AbsMinus program

E. Now we compute the postcondition relation between the initial and final states by β-reducing the application of the λ-expression (lines 19-20) to the symbolic initial and final state, resulting in:

3 i >= j ==> (j -i = i -j).
We then show that the precondition and the path imply the postcondition:

(i<=j ∧ ¬(i=j)) ==> ( i >= j ==> (j -i = i -j)).
This is easily proved using simplification in the theorem prover (see part 3.3).

F. The next step is to backtrack to the previous conditional instruction to explore another path in the program. Execution goes to step D.(e) and tests if the negation of the condition is possible. Since it is possible, execution continues on the 'else' part which gives a correct path.

G. The next backtrack goes to step D.(c). Condition ¬(i <= j) is possible so symbolic execution continues on the Skip instruction (line 11), which does not modify the current state. Then the conditional on line 13 is reached. Since the value of "k" in the current state is 0, the condition:

(And (Equal (Var "k") (Const 1)) (Not (Equal (Var "i") (Var "j"))))

is evaluated to false and so only the 'else' part is explored. This again gives a correct path.

The symbolic execution returns a conditional term that represents the paths that have been successively explored. Each possible value of this term is an outcome which gives the final value of the state. This outcome is preceded by RESULT when the path is correct, and by ERROR when the path contains an error or if i <= j then (if ¬(i = j) then RESULT["i" →i; "j" →j; "k" →1; "Result" →j-i; "result" →j-i] else RESULT["i" →i; "j" →j; "k" →1; "Result" →i-j; "result" →i-j]) else RESULT["i" →i; "j" →j; "k" →0; "Result" →i-j; "result" →i-j] Fig. 3. Result of symbolic execution of AbsMinus if i <= j then (if ¬(i = j) then RESULT["i" →i; "j" →j; "k" →1; "Result" →j-i; "result" →j-i] else RESULT["i" →i; "j" →j; "k" →1; "Result" →j-i; "result" →j-i]) else ERROR["k" →0; "Result" →j-i; "result" →j-i; "i" →(-32767); "j" →(-32768)]

Fig. 4. Result of symbolic execution of AbsMinus program with an error

TIMEOUT if symbolic execution failed to reach the end of the program for the given number of steps (see 4.2). Figure 3 shows the result of the symbolic execution of AbsMinus program.

AbsMinus program with an error

We now consider another version of AbsMinus where a 'copy-paste' error results in j-i being returned instead of i-j (see line 11 in Figure 1). When taking path i>j (line 8, Figure 1) in the program, the symbolic execution ends with final state: ["i" → i; "j" → j; "k" → 1; "Result" → j-i; "result" → j-i] The relational postcondition is then evaluated to i >= j ==> (j -i = ij) but the theorem prover fails to show that i > j ==> (i >= j ==> (j -i = ij)) so the constraint solver is called and it trivially finds a first solution (i,-32767) and (j,-32768). This provides a counterexample to the correctness of the program. Figure 4 shows the result of the symbolic execution of AbsMinus with this error.

Integrating theorem prover and constraint solver

Before presenting the algorithm of symbolic execution in more detail, we first explain how our theorem prover and constraint solver can be integrated. The goal is to get benefit of both: the theorem prover is good for proving theorems on (infinite precision) integers, but is not able to provide values that satisfies an existentially quantified formula. 4 On the other hand, constraint solvers can efficiently find witnesses for existential quantifications over finite domains and can be slow when the system has no solution, since a complete search through the data domain could be performed.

We first briefly explain constraint programming, then describe some tools implemented in our theorem prover (HOL4) and finally describe our heuristics to combine constraint solving and theorem prover to test the feasibility or correctness of program execution paths.

Constraint programming

Principles Constraint programming is a method for solving hard search problems. Applications include complex scheduling, sequencing, timetabling, routing and dispatching [START_REF] Dechter | Constraint Processing[END_REF]. Constraint programming solvers are based on a branch and prune algorithm that combines local consistencies and efficient search heuristics.

A Constraint Satisfaction Problem (CSP) is defined as: a set of variables X = {x 1 , ..., x n }, a finite set D i of possible values for each variable x i , called domain, a set of constraints C = {c 1 , ..., c n } where c i expresses a relation between some variables A solution of a CSP is an assignment of a value from its domain to every variable that satisfies all the constraints.

Arc-consistency [START_REF] Mackworth | Consistency in networks of relations[END_REF][START_REF] Bessiere | Using constraint metaknowledge to reduce arc consistency computation[END_REF] is the local consistency used for pruning CSP with finite domains. Let X j denotes the set of variables that occur in constraint c j . Constraint c j is arc-consistent if for any variable x i in X j , each value in domain D i has a support in the domains of all other variables of X j .

We illustrate arc-consistency based branch and prune to solve the CSP:

C = {c 1 : x 1 + x 2 < 2, c 2 : x 2 1 + x 2 2 ≤ 4, D 1 = {0, 1, 2, 3}, D 2 = {0, 1, 2, 3}}
. The pruning step starts by checking if constraint c 1 is arc-consistent. If value 0 is assigned to x 1 then value 1 for x 2 satisfies constraint c 1 (i.e. value 1 in D 2 is a support for value 0 in D 0 ). In the same way, value 1 has support 0 in D 2 . But values 2 and 3 have no support in D 2 so c 1 is not arc-consistent and the filtering step removes values 2 and 3 from domain D 1 . For the same reasons, values 2 and 3 are removed from D 2 . Then arc-consistency of constraint c 2 is checked. It is arc-consistent for the new domain. Thus, after the filtering step, the domain is:

D 1 = {0, 1}, D 2 = {0, 1}.
Then the search step is enabled. Value 0 is first selected for variable x 1 and solutions (0, 0), (0, 1) are found. Then value 1 is selected for variable x 1 to get the last solution (1, 0).

Calling the solver from the HOL4 theorem prover. Theorem proving tools are implemented as functions written in Standard ML ("ML" for "metalanguage"). The HOL4 system provides many predefined functions for proving theorems (e.g. various decision procedures, first-order resolution solvers, commands for user-guided interactive proof search). We have augmented these by defining an ML function extSolv to invoke an external constraint solver. Invoking "extSolv tm to f" returns a tagged theorem, where the tag (which is propagated whenever the theorem is used) indicates how the theorem was proved. The first argument, tm, is an existentially quantified term whose satisfiability is to be checked, the second argument, to, is a timeout used to stop the search and the third argument, f, is the integer format used to set the domains of variables in the constraint system. The tagged theorem is built as follows:

-If the constraint solver does not find any solution, then the theorem (tm=F) tagged with the string CSPSolver:f is returned. This means that external constraint solver has shown that there exists no value in [-2 f -1 , 2 f -1 -1] that satisfies tm and thus that ¬tm is true for integers coded on f bits.

-If the constraint solver finds a solution, then this solution is used to instantiate the existentially quantified variables in tm and the theorem (tm=T) is proved. This theorem is not tagged as externally generated since its proof has been done inside HOL4 using the witness from the solver.

Heuristics for testing feasibility of paths

A key point of symbolic execution, compared to bounded model checking methods, is that only semantically feasible paths are explored. But this is an improvement only if feasibility testing is very fast. Our heuristic for testing feasibility first uses the faster external solver and then, if necessary, slower theorem proving facilities provided by the HOL4 system are tried.

Let Φ be the formula to test, where Φ = ∃i. pre(i) ∧ path(i) ∧ test(i) and i represents input data, pre is the precondition, path is the current path (i.e conjunction of decisions that have been previously taken) and test is the Boolean expression test occurring in a conditional branch. The following two-stage heuristic method is used to decide feasibility of Φ.

Evaluate test on the current state by symbolically executing the semantics

Boolean expressions of the language (see 4.1). If it is true or false then return the corresponding value and stop.

2. Call the constraint solver with a small timeout and a small integer format. (a) If there is a solution, then return true. (b) It there is no solution, or a timeout, use HOL4's simplification and integer decision procedures to try to decide the satisfiability of Φ.

Symbolic evaluation (1) is quite efficient and is usually successful when the current state implies the condition. The constraint solver (2) is also efficient because the domains are small and a timeout is used. Furthermore, if the path is possible for a value inside [-2 f -1 , 2 f -1 -1] it is a fortiori true for a larger domain.

The timeout is useful when the path is not possible. In this case, the constraint solver could be very slow to show that there is no solution, since a complete search could be necessary. In this case theorem proving can be faster.

Heuristic for testing correctness of paths

While efficiency is the key point when testing feasibility of paths, soundness is a priority when testing their correctness. So the theorem prover is called first and only if that fails the constraint solver is called using a large timeout and large integer format. If the solver succeeds then a tagged theorem is returned. If the timeout is reached, or if higher assurance than that provided by the solver is required, then interactive proof can be done.

Symbolic execution

We represent programs and specifications as terms in higher order logic and use derived rules and tactics from the HOL4 system to perform parts of the computation, but other parts are programmed directly in ML and Java.

In earlier work (see [START_REF] Collavizza | A Constraint-Programming Framework for Bounded Program Verification[END_REF]), semantics preserving transformations, e.g. converting pre and postconditions to a form suitable to submitting to a constraint solver, were performed by unverified Java programs. We have replaced many of these with formal rewriting or custom derived rules 5 . The implementations of such truth preserving term manipulations is straightforward, so is not elaborated here.

Operational semantics

We use mechanised proof to compute symbolic single steps when executing a path (see Point D in Section 2). The formal representation of programs shown in Figure 2 has a standard big-step operational semantics [START_REF] Camilleri | Reasoning with Inductively Defined Relations in the HOL Theorem Prover[END_REF] shown in Figure 5. The relation EVAL is the least relation satisfying the conjunction of rules shown in the semantics. A term EVAL c s1 s2 means that executing command c in an initial state s 1 terminates in a state s 2 (a more standard notation is c, s 1 ⇓ s 2 ); neval e s is the value of integer expression e in state s; beval b s is the value of Boolean expression b in s; s+(v,n) is the state obtained from s by making variable v have value n; s^v is the value of v in s, v ∈ s means v is defined in s and s-v is the result of removing v from s. The big-step semantics is not efficient to execute directly,6 so we defined a small-step semantic function STEP1 (see Figure 6) and interactively proved that this corresponds to EVAL [START_REF] Nipkow | Winskel is (almost) Right: Towards a Mechanized Semantics Textbook[END_REF]. Define a small-step transition relation by:

SMALL EVAL (l1,s1) (l2,s2) = (STEP1 (l1,s1) = (l2,RESULT s2))
where l1 and l2 are lists of commands ([] is the empty list and [c] is the singleton list containing c). A routine mechanical proof then establishes:

∀c s1 s2. EVAL c s1 s2 = TC SMALL EVAL ([c],s1) ([],s2)
where TC SMALL EVAL is the transitive closure of SMALL EVAL The function STEP1 is efficiently executed inside HOL4 using a call-by-value reduction engine due to Barras [START_REF] Barras | Programming and Computing in HOL[END_REF]. If STEP1(l1,s1) = (l2,r) then executing one step of the command at the head of l1 in state s1 results in (l2,r), where l2 are the remaining commands to be executed and r is the result, which can either be RESULT(s2) if the step succeeds or ERROR(s2) if there is an assertion failure. There is a third kind of result, TIMEOUT(s2), which is not generated by STEP1 but can arise when executing sequence of steps (see below).

Symbolic execution algorithm

Symbolic execution is by depth first search of feasible paths. A user-specified parameter count bounds the number of steps. (e.g. when programs contain loops). Let pre, path, s 1 , s 2 , post be terms as follows:

pre: precondition (predicate on states represented as a λ-expression) path: current path (conjunction of decisions taken so far) s 1 : initial state before program execution s 2 : current state after execution of the current path post: postcondition (predicate on pairs of states represented as a λ-expression)

The initial state s 1 is automatically built from the program, with logical variables representing the symbolic values of the program variables. Let l be the list of terms that represent the instructions of the program (initially this will be [c], where c is the program being symbolically executed). Let valP re be the precondition evaluated on s 1 , and valP ost be the postcondition evaluated on the pair (s 1 , s 2 ). We assume that we have two functions:

-testPath tests if condition b is feasible on the current path i.e if valP re ∧ path ∧ b has a solution, -verifyPath tests the correctness of the path i.e if valP re ∧ path ∧ ¬valP ost has no solution 7 . This function returns the outcome (RESULT s) if the program is correct along the path and otherwise returns the outcome (ERROR serr) where s err contains the error that has been found.

These two functions call the constraint solver and the theorem prover according to the heuristics described in part 3.2 and 3.3.

The symbolic execution algorithm is detailed in Figure 7. If the last instruction has been reached (point 1) then the correctness of the path is tested. If the maximum number of steps (count) reaches zero (point 3) then an outcome TIMEOUT(s) is generated. If the first instruction is not a conditional (point 5), then next state is computed and execution continues on the next instruction. If the first instruction is a conditional instruction (point 6) then the feasibility of the condition and the feasibility of the negation of the condition are tested. Note that backtracking is performed when the instruction is a conditional instruction or a While-instruction because the two possible paths are explored (i.e points 6 and 13 are both executed).

Experimental results

In this section, we report experimental results for a set of textbook algorithms. All experiments were performed on an Intel(R) Pentium(R) M processor 1.86GHz with 1.5G of memory. The theorem prover used is HOL4 and the constraint solver is constraint-programming tool Ilog JSOLVER. Parser from Java to internal syntax is built on Eclipse JDT (Java Development Tool).

We first introduce the whole set of examples, then illustrate the main points of our approach and finally discuss related work.

Set of programs

Tritype Our first example is not a textbook algorithm, however we selected it because it illustrates programs that do not contain loops but have complex conditional statements. This kind of control structure is frequently found in command and control systems. Tritype is a standard benchmark in test case generation since it contains numerous non-feasible paths. This program takes three positive integers as inputs (the triangle sides) and returns a value that determine the type of the triangle (the Java program is given in Appendix 1). This example illustrates how unfeasible paths are cut.

execSymb(pre, path, l, s1, s2, count, post) = 1. If l=[] the end of a path is reached so result is verifyPath(pre, path, s1, s2, post) 2. else 3. if count = 0 then the program can't be executed with the given number of execution steps, so the result is (TIMEOUT s2). 4. else let l = [c,l'] 5. if c is not a control instruction (Cond or While) then call STEP1 to compute the next state s according to the small-step semantics, then recursively call execSymb(pre, path, l , s1, s , count-1, post) to continue symbolic execution. 12. If c is the loop instruction (While b c while ) then recursively call execSymb(pre, (path ∧ ¬b), l , s1, s2, count, post) to exit the loop. 13. Call testPath(pre, s1, path, ¬b) to know if the negation of the condition is possible on the current path and take the corresponding path as explained above.

Fig. 7. Symbolic execution algorithm

Sum of the n first integers computes the sum of the n first integers. The specification is that it returns n × (n + 1)/2 (where n is the data input). This illustrates how loops are handled and how symbolic execution sets a constant value to n and thus avoids getting a non-linear term at the end of the path.

Sum of integers from P to N computes the sum of the integers from p to n where p and n are input data (see Appendix 2). The precondition is that p is less or equal to n and the postcondition is that the value returned is n × (n + 1)/2 -(p -1) × p/2. This example illustrates how the constraint solver is called when the term to be verified at the end of the path is non-linear.

Binary search is the well known binary search program that determines if a value x is present in a sorted array a. We also consider an incorrect version of this program where a copy-paste error has been inserted (see Appendix 3).

Bubble sort with precondition is a bubble sort algorithm where a precondition sets the values of the array to be sorted in decreasing order and to contain the values from a.length -1 to 0. This example is from Mantovani et al. [START_REF] Mantovani | Bounded Model Checking of C Programs using a SMT solver instead of a SAT solver[END_REF].

Discussion

Table 1 shows statistics on the solving process for our set of examples. In this table, #cond (resp. #condEval and #cut) is the number of conditions reached in the program (resp. that have been decided using simplification in HOL4 and that have been proven false). #path is the number of feasible paths. #verifHOL (resp. #verifCSP) is the number of paths that that have been verified using HOL4 (resp. using the constraint solver). HOLtime (resp. CSPtime) is the time spent by HOL4 for proofs and symbolic execution (resp. with the CSP solver).

For Sum and SumPtoN, we verified all numbers of loop steps from 0 to 10, and for Bsearch and BubbleSort program, the length of the array has been set to 10.

Tritype As shown in table 1, half of the conditions were decided by evaluating the condition on the current state. This is due to the fact that many tests in the Tritype program (see Appendix 1) are on a local variable which is assigned constant values, according to the number of triangle sides which are equal.

Sum of the n first integers This example illustrates how loops are handled.

Our symbolic execution algorithm is bounded by the maximum number of instructions that can be executed, which provides a bound for loop unwinding. All paths through the loop containing less than this maximum number are explored.

For the Sum example, adding loop entrance and exit conditions (see points 9 and 12 in figure 7) sets a constant value to variable n. For example, when the loop has been entered 5 times, the term to be verified is:

∃n.(n ≥ 0) ∧ (0 ≤ n ∧ 1 ≤ n ∧ 2 ≤ n ∧ 3 ≤ n ∧ 4 ≤ n ∧ ¬(5 ≤ n)) ∧ ¬(10 = n * (n + 1)/2).
Since n must satisfy both 4 ≤ n and ¬(5 ≤ n) it follows that n = 4, so the postcondition ¬(10 = n * (n + 1)/2) trivially holds.

The results in Table 1 show that 11 paths have been explored (entering 0, 1, 2, ..., 10 times into the loop) and that all the paths were solved with the constraint solver. This is because simplification in HOL4 doesn't handle non linear terms. However, since the value of n is constant as explained above, the constraint solver efficiently verifies this term.

Sum of integers from p to n If we now start the sum with input data p, the decisions taken to enter the loop, or not, won't set the value of n, since it will depend on p. For example, the term below is the term to be verified when the loop has been entered 5 times:

∃np.(n ≥ 0 ∧ p ≥ 0 ∧ p ≤ n) ∧ (p ≤ n ∧ p + 1 ≤ n ∧ p + 2 ≤ n ∧ p + 3 ≤ n ∧ p + 4 ∧ ¬(p + 5 ≤ n)) ∧ ¬(p + (p + 1) + (p + 2) + (p + 3) + (p + 4) = n * (n + 1)/2 -(p -1) * p/2)
The conditions on the path imply that n = p + 4, but this does not set any constant value for n. The results in Table 1 show that execution time for HOL4 is 20 times slower than time for the Sum program. This is due to the fact that simplification rules take more time trying to simplify the term before they finally fail. Also, the constraint solver takes 100 more times than for the Sum program because here, the term to be verified is not instantiated.

Binary search Table 1 shows that all paths were solved with the theoremprover and that more time was spent with the constraint solver for the Bsearch with an error since it was called to find the errors.

Two errors were found in the incorrect Bsearch program (Appendix 3). The first for path ¬(a 4 =x)∧x<a 4 ∧¬(a 1 =x)∧¬(x<a 1 ) for data input x = -32768 and a = [-32768,-32768,-32768,-32767,-32766,-32766,-32766,-32766,-32766,-32766]. Value x is first searched on the left part of the array, so index lef t = 0 and right=3. Then it is searched on the right part, but the error in the program set the right index instead of the left one and so lef t = 0 and right=0. Since the array is initially sorted, a 0 ≤ a 1 and the condition ¬(x < a 1 ) in the path implies that a 0 ≤ x. Thus the value is then searched on the right. Again the error in the program modifies the right index to get lef t = 0 and right = -1. So the execution stops with result = -1 while value -32768 is in the array.

Note that this example also illustrates our heuristic for testing paths: the theorem-prover has been called for testing two paths because a time-out was reached with the constraint solver.

Bubble sort Table 1 shows that we explored the unique feasible path in this program and that all conditions were decided by evaluating the condition on the current state. In fact, the precondition set the initial values of the array. The 10 conditions that were false correspond to the 10 times where condition j < a.length -i -1 was false (i.e. exiting the inner loop).

Discussion of related work

We first discuss previous work based on constraint programming for software validation. Then we contrast our symbolic execution algorithm to bounded-model checking (BMC). And last we discuss other approaches that merge theorem proving and automatic formal verification methods.

Constraint logic programming was first used for test generation of programs [START_REF] Gotlieb | Automatic Test Data Generation using Constraint Solving Techniques[END_REF][START_REF] Jackson | Finding Bugs with a Constraint Solver[END_REF][START_REF] Sy | Automatic Test Data Generation for Programs with Integer and Float Variables[END_REF]. Gotlieb et al. [START_REF] Botella | Symbolic execution of floating-point computations[END_REF] showed how to represent imperative programs as constraint logic programs and used predicate abstraction and conditional constraints within a constraint logic programming framework. This test-generation methodology was generalised and applied to bounded program verification in [START_REF] Collavizza | Software Verification using Constraint Programming Techniques[END_REF], where a hybrid constraint system including Booleans for control and integers for data was generated and solved. In order to avoid exploring spurious execution paths, the approach presented in [START_REF] Collavizza | A Constraint-Programming Framework for Bounded Program Verification[END_REF] introduces the symbolic execution algorithm used here which prunes unfeasible paths using constraint-based solvers 8 . This symbolic execution algorithm is similar to bounded-model checking approaches in the sense that it explores paths of bounded length (see [START_REF] Vijay | A Survey of Automated Techniques for Formal Software Verification[END_REF] for a recent survey). But it differs in at least two ways. First, the feasibility of paths is tested with efficient solvers and thus only feasible paths are explored. Second, each path is verified separately and thus the formulas to be proven are smaller. This is better adapted to theorem proving or constraint solving methods, which are not tailored to handle large formula with a complex Boolean structure.

The alternative BMC method for software consists in building a formula whose models correspond to program execution paths of bounded length that violate a property. The satisfiability of this formula is checked by replacing arithmetic operators by bit-vectors operators to obtain a propositional formula which is solved using efficient SAT solvers. CBMC [START_REF] Kroening | A Tool for Checking ANSI-C programs[END_REF] is one of the most popular tools that implements BMC for checking C programs. In recent work [START_REF] Mantovani | Bounded Model Checking of C Programs using a SMT solver instead of a SAT solver[END_REF], Armando et al. used SMT solvers to verify linear programs with arrays.

A comparison of performances between BMC and our previous approach that combines symbolic execution and constraint programming is provided in [START_REF] Collavizza | A Constraint-Programming Framework for Bounded Program Verification[END_REF]. Performances of the approach presented in this paper are in average two hundred times slower. But most of the proofs are done within the theorem prover.

Another interesting piece of work that combines theorem proving with automatic solvers is presented in [START_REF] Fillitre | The Why/Krakatoa/Caduceus Platform for Deductive Program Verification Proc. CAV[END_REF]. The Why/Krakatoa/Caduceus platform is based on the Why language, which is dedicated to program verification. Both Java and C programs are translated to Why programs. A tool based on a Weakest Precondition calculus generates verification conditions for interactive provers, such as Coq or Isabelle and automatic provers such as Simplify or SMT solvers Yces. This approach differs from ours because it doesn't combine dynamic theorem proving with other automatic solvers. On the contrary, it generates a set of verification conditions, a subset of which can be checked by a theorem prover. Experiments with the Why platform, showed that our approach is less efficient on the tritype program (8.85s with Why and 39.8s for our approach), but that our approach was applicable to the binary search program while Why approach was not (unless an invariant is provided).

Future work

We mentioned in the introduction that the work reported here lies in the middle of a verification tool implementation spectrum with unverified tools at one end and everything computed by deduction inside a theorem prover at the other end. In the future we plan to explore other points in this spectrum. In particular we would like to perform the complete symbolic execution and path extraction within a theorem prover and compare performance and scalability with the approach described here. Preliminary experiments suggest that this is feasible, but there are efficiency challenges. However, in applications requiring certification, having high assurance that verification is sound is valuable, so it is useful to calibrate the cost of increasing soundness assurance, even if for some applications the price is too high.

Fig. 1 .

 1 Fig. 1. AbsMinus program in Java D. Symbolically execute a path in the program (a) The first instruction (line 4 in Figure2) is (Assign "result" (Const 0))).The new state is computed directly from a small-step semantics that has been formally verified (by interactive proof) to correspond to the big-step reference semantics (see part 4.1). The new state is: ["i" → i; "j" → j; "k" → k; "Result" → Result; "result" → 0] (b) The next instruction (line 6) is executed in the same way to get state:["i" → i; "j" → j; "k" → 0; "Result" → Result; "result" → 0] (c) The conditional instruction (line 8) is executed using a heuristic that combines the theorem prover (HOL4) and constraint solver to test if the path is feasible (see part 3.2). The condition is first evaluated on the current state, using the semantics of Boolean operations defined for the language (see part 4.1). The result is: i <= j. We then test if this condition is possible according to the precondition (which is T) and the current path (which is also T). First the constraint solver is called to solve the constraint system: i[-128..127] <= j[-128..127]. It trivially finds solution (i,-128) (j,-128) (note that the integer format has been fixed to 8 bits here using the heuristic described in 3.2). So condition i <= j is added into the current path and execution continues on the 'then' part of the conditional instruction (line 10). (d) (Assign "k" (Plus (Var "k") (Const 1))) (line 10) is executed to get:["i" → i; "j" → j; "k" → 1; "Result" → Result; "result" → 0] (e) The next instruction (line 13) is a conditional branching on:

  i[-128..127] <= j[-128..127] not(i[-128..127] = j[-128..127])

(Fig. 5 .

 5 Fig. 5. Big-step semantics

(Fig. 6 .

 6 Fig. 6. Small-step semantics

6 .

 6 else let b be the condition of c, then call testPath(pre, s1, path, b) to know if the condition is possible on the current path 7. if b is possible, take the corresponding path in the program. 8. If c is the conditional (Cond b c then c else ) then recursively call execSymb(pre, (path ∧ b), [c then , l ], s1, s2, count, post) to execute the then part. 9. If c is the loop instruction (While b c while ) then recursively call execSymb(pre, (path ∧ b), [(While b c while ), l ], s1, s2, count, post) to enter the loop. 10. if b is not possible, take the corresponding path in the program. 11. If c is the conditional (Cond b c then c else ) then recursively call execSymb(pre, (path ∧ ¬c), [c else , l ], s1, s2, count, post) to execute the else part.

  In this initial state, i, j, k, Result and result are integer variables, representing the symbolic value in the state of the strings (corresponding to program variables) with the same name. Result is the value returned by the program and represents both \result of the JML specification and the expression returned by the Java program.

B. Evaluate the precondition on this initial state: T.

Table 1 .

 1 Experimental results

	name	#cond #condEval #cut #path #verifHOL #verifCSP HOLtime CSPtime
	Tritype	27	15	16	10	10	0	39.410s 0.481s
	Sum	12	0	1	11	0	11	17.433s 0.119s
	SumPtoN	12	0	1	11	0	11	344.878s 13.501s
	Bsearch	51	31	21	21	21	0	237.071s 0.315s
	BsearchKO 25	13	13	7	7	0	119.499s 0.514s
	BubbleSort 109	109	10	1	1	0	526.989s	0.0s

Note that the first part of the conjunction in the lambda expression has been evaluated to true because Result = j-i

There are theorem provers that can produce counterexamples, but not ours.

Example: converting formulas of the form ¬((A1 ⇒ B1) ∧ • • • ∧ (An ⇒ Bn) ∧ t) to (A1 ∧ ¬B1) ∨ • • • ∨ (An ∧ ¬Bn) ∨ ¬t), or converting \forall JML statements to finite conjunctions.

There are methods of executing inductive relations using techniques adapted from Prolog interpreters, but our theorem prover does not support these.

this means that valP re ∧ path ∧ ¬valP ost is false for each input value and so that valP re ∧ path ⇒ valP ost is true

More precisely, this previous approach combined the ILOG CPLEX MIP Mixed Integer Programming tool which is based on the simplex algorithm with ILOG JSOLVER we used in this paper

Acknowledgements

We would like to thank Michel Leconte for much help and advice with JSOLVER. Many thanks also to Andreas Podelski for fruitful discussions on bounded model checking and for suggesting one of the examples.


Guillaume Feuillade

Andreas Herzig

Christos Rantsoudis

Knowledge Base Repair: From Active Integrity Constraints to Active TBoxes

Keywords: database repair, knowledge base repair, active integrity constraints, description logic, dynamic logic

In the database literature it has been proposed to resort to active integrity constraints in order to restore database integrity. Such active integrity constraints consist of a classical integrity constraint together with a set of preferred update actions that can be triggered when the constraint is violated. In this overview paper we start by reviewing the main repairing routes that have been proposed in the literature. We do so from the perspective of Dynamic Logic, viewing active integrity constraints as programs that test whether a constraint is violated and if so perform appropriate update actions. We then discuss how these ideas can be adapted to Description Logics. We assume extensions of TBox axioms by update actions that denote the preferred ways an ABox should be repaired in case of inconsistency with the axioms of the TBox. The extension of the TBox axioms with these update actions constitute new, active TBoxes.

Introduction

One of the most important and notoriously difficult issues in the database and AI literature is the problem of updating a database under a set of integrity constraints. In the course of database maintenance several changes are applied to the databases and checking whether these constraints are still entailed is of fundamental importance.

The TBoxes of Description Logic knowledge bases bear resemblances with integrity constraints. However, due to the open world assumption the TBox axioms do not have to be entailed by the ABox; instead, their role is to infer more than what is literally written in the ABox. TBoxes therefore only have to be consistent with the ABox. Hence the counterpart of checking whether the updated database still entails the integrity constraints is the problem of checking whether the updated ABox is still consistent with the TBox. 1 When a database fails to satisfy the integrity constraints then there are basically two different options: one may either live with the inconsistency or repair the database in order to restore integrity. If one chooses the latter option then one has to explicitly construct the repaired database. The former option requires the definition of non-standard inconsistency-tolerant semantics that are a priori in the spirit of paraconsistent logics; one may in particular rely on hypothetical repairs. The two options therefore lead to solutions that are technically quite similar.

Procedures restoring the consistency of a database with respect to a set of integrity constraints were extensively studied in the last decades [START_REF] Abiteboul | Updates, A new frontier[END_REF][START_REF] Ceri | Automatic generation of production rules for integrity maintenance[END_REF][START_REF] Bertossi | Database Repairing and Consistent Query Answering[END_REF]. These approaches propose several possible repairs as candidates for integrity maintenance and it seems essential to identify which types of repairs are more suitable, all the more the number of all possible repairs can be remarkably large. Given this, the most prevalent have become those that are based on the minimality of change principle [START_REF] Winslett | Updating Logical Databases[END_REF][START_REF] Herzig | Propositional belief base update and minimal change[END_REF][START_REF] Chomicki | Minimal-change integrity maintenance using tuple deletions[END_REF].

The situation is similar for description logic knowledge bases when an ABox is updated in a way such that it becomes inconsistent with a given TBox. For DL knowledge bases, the most widespread methods to repair inconsistencies are based on the so-called justifications, which are minimal subsets of the KB containing the terminological and assertional axioms from which an undesirable consequence is inferred. Axiom pinpointing through justifications became an important topic of research within the DL community and several results were quickly established [START_REF] Schlobach | Non-standard reasoning services for the debugging of description logic terminologies[END_REF][START_REF] Kalyanpur | Finding all justifications of OWL DL entailments[END_REF][START_REF] Suntisrivaraporn | A modularization-based approach to finding all justifications for OWL DL entailments[END_REF]. Both black-box [START_REF] Schlobach | Debugging incoherent terminologies[END_REF]2] and glass-box [START_REF] Parsia | Debugging OWL ontologies[END_REF][START_REF] Meyer | Finding maximally satisfiable terminologies for the description logic ALC[END_REF] methods emerged for computing justifications. The former have a more universal approach and are used independently of the reasoner at hand, while the latter have a more delicate construction that is tied to specific reasoners and usually require less calls. After computing all justifications of an undesirable consequence, the next step is to obtain a minimal hitting set [START_REF] Reiter | A theory of diagnosis from first principles[END_REF] made up of one axiom per justification and remove it from the knowledge base. More recent approaches have focused on providing methods for weakening the axioms instead of removing them, since the latter can prove to be too big of a change [START_REF] Troquard | Repairing ontologies via axiom weakening[END_REF]. Another research avenue investigates repair-based semantics for query answering [START_REF] Bienvenu | Query-driven repairing of inconsistent dl-lite knowledge bases[END_REF][START_REF] Bienvenu | Computing and explaining query answers over inconsistent dl-lite knowledge bases[END_REF].

It seems fair to say that for the time being there is no consensus on the 'right' way of repairing inconsistent knowledge bases. Given these long-standing difficulties to define appropriate repairs, it seems reasonable to resort to more modest approaches where more information is fed into the repair process. In the present paper we take inspiration from a research avenue in the database literature where integrity constraints are equipped with additional information about the preferred way to maintain consistency: in [START_REF] Flesca | Active integrity constraints[END_REF] Active Integrity Constraints 1 We note that there are approaches combining integrity constraints with TBoxes.

The most prominent ones are based on the extension of KBs with constraint axioms. These axioms are however used for validation purposes only and do not share the same semantics as regular TBox axioms [START_REF] Motik | Bridging the gap between OWL and relational databases[END_REF][START_REF] Tao | Integrity constraints in OWL[END_REF].

(AICs) were proposed as an enhancement of classical integrity constraints with update actions. This research avenue was further pursued in a series of publications [7,[START_REF] Caroprese | Active integrity constraints and revision programming[END_REF][START_REF] Cruz-Filipe | Optimizing computation of repairs from active integrity constraints[END_REF]. AICs extend classical integrity constraints with preferred update actions. This introduces a dynamic view of the concept of integrity constraint.

From now on we therefore call classical integrity constraints static constraints and will talk about the static part of an AIC.

For instance, consider the classical integrity constraint:

∀(E, S 1 , S 2 )[Employee(E, S 1 ) ∧ Employee(E, S 2 ) → S 1 = S 2 ]
which says that every employee should only have one salary. It can be extended into the active constraint:

∀(E, S 1 , S 2 )[Employee(E, S 1 )∧Employee(E, S 2 )∧S 1 > S 2 → -Employee(E, S 1 )]
which states that if there is an employee with two salaries then the preference is to remove the highest salary (instead of removing one randomly).

Another example is the static integrity constraint:

(∀X)[Bachelor(X) ∧ Married(X) → ⊥]
which says that no one should have the property of being a bachelor and married at the same time. It can be turned into the active constraint:

(∀X)[Bachelor(X) ∧ Married(X) → ⊥, {-Bachelor(X)}]
whose meaning is that when there is a person in the database who has both the status of being a bachelor and the status of being married then the preferred repair is to remove from the database the bachelor status (as opposed to removing the married status) since married status can be achieved from being bachelor but not the other way. In this way, the possible repairs better match designer preferences when maintaining the database. Moreover, it can be expected that their number is narrowed down. In the propositional case, an active integrity constraint can be represented as a couple:

r = C(r), R(r)
where C(r) is a boolean formula (called the static part of r and denoting a static constraint) and R(r) is a set of update actions, each of which is of the form +p or -p for some atomic formula p. The idea is that (1) when the static constraint C(r) is false then the constraint r is violated, and (2) a violation of r can be repaired by performing one or more of the update actions in R(r).

The Semantics of Active Integrity Constraints

It remains to give a semantics to a given set of active integrity constraints in terms of the repairs it induces. The two most important ones that were proposed in the literature are the founded and the justified repairs. While both semantics greatly reduce the number of possible repairs, different choices between update actions in R(r) can still lead to different repairing routes, or even no repairs at all. This is for example trivially the case when R(r) is the empty set.

In the first paper about AICs the authors introduce founded repairs [START_REF] Flesca | Active integrity constraints[END_REF]. The idea is that any update action applied to the database should be supported by the 'active part' of an AIC, i.e., by a preferred update action of a violated constraint. They also obtain complexity results for the problem of existence of founded repairs, both in the general case (Σ 2 P -complete) as well as in the case that AICs comprise 'single heads', i.e., only one preferred update action is allowed in each constraint (NP-complete). Recognizing that the existence of founded repairs is not always guaranteed though, they go on to define preferred repairs as an intermediate repairing route between founded and standard repairs that always exist. The complexity for the problem of existence of preferred repairs is shown to be Σ 2 P -complete. Further research on AICs also ensued [START_REF] Caroprese | Declarative semantics of production rules for integrity maintenance[END_REF]7] that reviewed and expanded upon the aforementioned results.

The first new definitions on repairing procedures that are based on preferences between update routes came in [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF], an attempt to relate the seemingly different approaches to AICs and revision programming. There, the authors distinguish between the various repairs that they propose (standard repairs, founded repairs, justified repairs) and their weaker versions (weak repairs, founded weak repairs, justified weak repairs), with only the former complying to the minimality of change principle that the previous approaches took by default. The definitions of justified weak repairs and justified repairs were introduced as a response to the so-called circularity of support defect that founded repairs cannot evade and which the authors argue against. Furthermore, they leave the first-order setting of the previous papers and use a propositional one. The propositional setting of [START_REF] Caroprese | Active integrity constraints and revision programming[END_REF] provides a valuable stepping stone to present and discuss our own approach. Another distinguishing feature in their work is that they investigate properties of normalization, i.e., 'breaking' all active integrity constraints into many copies such that each one has at most one preferred update action. They denote the differences that exist in these two different classes of AICs, both in practice (resulting in more or fewer repairs) as well as in the complexity of deciding the existence of repairs under normal AICs. The consensus on complexity results is very interesting, with all of the different kinds of repairs, being either weak or minimal, and being applied on either normal AICs or standard AICs, to fall either on the NP-complete or Σ 2 P -complete territory. Last but not least, further approaches to refine or extend active integrity constraints have been investigated in [12,[START_REF] Cruz-Filipe | Optimizing computation of repairs from active integrity constraints[END_REF] with analyses of algorithms on trees, extensions to knowledge bases outside databases, as well as independence/precedence relations among active integrity constraints.

In the paper [START_REF] Feuillade | A dynamic logic account of active integrity constraints[END_REF] we have recast these different semantics in Dynamic Logic. More precisely, we have shown that active integrity constraints can be viewed as particular programs in Dynamic Logic of Propositional Assignments DL-PA: they consist in a test of the negation of the static part of the AIC that is followed by a nondeterministic composition of the possible update actions. The latter are identified with sets of assignments of propositional variables to truth values. Given an AIC r = C(r), R(r) , the associated DL-PA program is therefore:

¬C(r) ? ; R(r)
These are the building blocks of programs capturing all the above semantics, as shown in [START_REF] Feuillade | A dynamic logic account of active integrity constraints[END_REF]. Furthermore, a new kind of repair program is defined there as:

r ¬C(r) ? ; R(r)
and is compared to the existing semantics.

3 From Active Integrity Constraints to Active TBoxes

It seems natural to us to transfer the active integrity constraint idea to the Description Logic setting. If we identify ABoxes with databases and TBoxes with integrity constraints then the axioms of the latter should be extended with preferred update actions. These update actions should prescribe the changes the ABox should undergo in order to reestablish consistency whenever it is inconsistent with the TBox. We call these extended TBoxes active TBoxes. They enable ontology engineers to easily express preferred update actions, thereby avoiding that unwanted repairing routes are followed. The idea is to repair inconsistent KBs by updating ABox assertions in order to comply with (preferred update actions indicated by) the axioms of the active TBox. Somewhat surprisingly, this research avenue had not been tried in the DL literature. For example, consider the following static TBox: We can witness how, through these enhanced concept inclusions, one can be more specific in the update actions that s/he prefers when repairing an ABox that is inconsistent with T : the active axioms of aT 1 dictate that an individual who is a father should remain a father in case of inconsistency, whereas an individual who has siblings should change its status and not be an only child anymore. Similarly for aT 2 , where '-hasSibling. ' removes all relations between individuals that violate the axiom and individuals satisfying (i.e., all individuals), thus stating that an only child who has siblings should drop its 'sibling' relationship with everyone and stay an only child. Now consider the following ABox:

T = {Father
A = {John : Male Father ¬Parent, Mary : OnlyChild, hasSibling(Mary, John)}

A repaired ABox then according to aT 1 should be the following:

A 1 = {John : Male Father Parent, Mary : ¬OnlyChild, hasSibling(Mary, John)} whereas a repaired ABox according to aT 2 should be the following:

A 2 = {John : Male ¬Father ¬Parent, Mary : OnlyChild}

Contributions

We have attempted to materialize the above intuitions in a number of different formats and examine how the various definitions of repairs from the database literature translate and behave in the DL setting. This has resulted in several publications as well as the PhD thesis [START_REF] Rantsoudis | Knowledge Bases and Preferred Update Actions : Searching for Consistency through Dynamic Logic Programs[END_REF].

Our main goal was to apply the idea behind active integrity constraints in the Description Logic setting and, in particular, to provide extensions of TBox axioms so that they are able to suggest preferred repairing routes in case of inconsistencies. We started by overviewing active integrity constraints in the propositional setting through the DL-PA lens. Embeddings of weak, founded and justified repairs into DL-PA were proposed and studied in [START_REF] Feuillade | A dynamic view of active integrity constraints[END_REF][START_REF] Feuillade | A dynamic logic account of active integrity constraints[END_REF]. The DL-PA framework moreover naturally leads to a a new, dynamic way of integrity maintenance, dynamic repairs. We have analysed the properties of all these repairs and provides complexity results for the problem of existence of dynamic repairs. We also took advantage of the dynamic framework-i.e., the logic DL-PA-in order to explore an extension on databases with history and adjust the behavior of the various repairs so that they work in this setting. Finally, we provided DL-PA counterparts of all the reasoning and decision problems arising in the repair setting, such as the existence of a repair or the existence of a unique repair.

In the paper [START_REF] Rantsoudis | Repairing ABoxes through active integrity constraints[END_REF] we have started to lift the idea behind AICs to Description Logics. There, the first definition of 'active' TBoxes was introduced. After a brief discussion on the differences and difficulties of leaving the propositional setting, we examine preliminary steps into repairing ABoxes syntactically so that they conform to the preferences denoted by the active axioms. These syntactic repairs are inspired by (and correspond to) the weak and founded repairs of the database literature. Proving to be quite impractical though, we suggest that a semantic approach seems more viable.

In the paper [START_REF] Feuillade | A dynamic extension of ALCO for repairing via preferred updates[END_REF] we went on to pursue this semantic approach and investigated how the dynamic logic-based framework can be transferred to the DL level. We use a more local approach, where preferred update actions in the active axioms behave similarly to the update actions introduced before, i.e., they have the form ±A for an atomic concept A denoting either the addition or the removal of an individual from the set of individuals that have property A. This approach, although more expressive and well-behaved than the syntactic one of [START_REF] Rantsoudis | Repairing ABoxes through active integrity constraints[END_REF], still leaves a lot of repairing scenarios unattainable, mainly because of its boolean nature and close similarity to the repairs of the database literature.

In Rantsoudis's Phd thesis a more elaborate logic and techniques are introduced and discussed which apply changes globally, in the sense that preferred update actions of the form ±C can be applied to all individuals violating an axiom and C is not necessarily atomic [START_REF] Rantsoudis | Knowledge Bases and Preferred Update Actions : Searching for Consistency through Dynamic Logic Programs[END_REF]Chapter 5]. As before, a dynamic logic framework that is influenced by the logic DL-PA is used. Furthermore, although the resulting logics are extensions of ALCO and ALCIO respectively with dynamic operators, they are shown to be as expressive as their static counterparts (with the addition of the universal role).

The Phd thesis [START_REF] Rantsoudis | Knowledge Bases and Preferred Update Actions : Searching for Consistency through Dynamic Logic Programs[END_REF]Chapter 6] concludes with a proposal to connect the approaches of the syntactic approach in [START_REF] Rantsoudis | Repairing ABoxes through active integrity constraints[END_REF] and the semantic approach in [START_REF] Feuillade | A dynamic extension of ALCO for repairing via preferred updates[END_REF], thus completing the picture on active TBox-based ABox repairs. It also briefly discusses future work, with possible applications of the proposed repairing methods on nonmonotonic scenarios.

1 : 3 : 4 :

 134 Male Parent, OnlyChild ∀hasSibling.⊥} An ontology engineer may wish to enhance it to two possible active TBoxes, viz. aT 1 = {η 1 , η 2 } and aT 2 = {η 3 , η 4 } where: η Father Male Parent, {+Male, +Parent} ; η 2 : OnlyChild ∀hasSibling.⊥, {-OnlyChild} ; η Father Male Parent, {-Father} ; η OnlyChild ∀hasSibling.⊥, {-hasSibling. }