Constantin Enea

Ondřej Lengál

Mihaela Sighireanu

Tomáš Vojnar

SPEN: A Solver for Separation Logic

SPEN is a solver for a fragment of separation logic (SL) with inductively-defined predicates covering both (nested) list structures as well as various kinds of trees, possibly extended with data. The main functionalities of SPEN are deciding the satisfiability of a formula and the validity of an entailment between two formulas, which are essential for verification of heap manipulating programs. The solver also provides models for satisfiable formulas and diagnosis for invalid entailments. SPEN combines several concepts in a modular way, such as boolean abstractions of SL formulas, SAT and SMT solving, and tree automata membership testing. The solver has been successfully applied to a rather large benchmark of various problems issued from program verification tools.

Introduction

For analyzing programs with dynamic memory, separation logic (SL) is an established and fairly popular logic introduced by Reynolds [START_REF] O'hearn | Local Reasoning about Programs that Alter Data Structures[END_REF]. The high expressivity of SL, its ability to generate compact proofs, and its support for local reasoning motivated development of many tools for automatic reasoning about programs with complex dynamic linked data structures. These tools aim at establishing memory safety properties and/or inferring shape properties of the heap. The tools often build on (semi-)decision procedures for checking satisfiability and entailment problems in SL.

Our tool SPEN 3 provides (semi-)decision procedures for the most commonly considered symbolic heaps fragment of SL, extended with user-defined inductive predicates to specify data structures of an unbounded size. Because unrestricted definitions of inductive predicates make the entailment problem for the fragment undecidable [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF], only semi-decision procedures have been proposed, e.g., in [START_REF] Brotherston | A Generic Cyclic Theorem Prover[END_REF][START_REF] Chin | Automated Verification of Shape, Size and Bag Properties via User-defined Predicates in Separation Logic[END_REF]. Iosif et al. [START_REF] Iosif | The Tree Width of Separation Logic with Recursive Definitions[END_REF] identified a rather large class of inductive definitions for which the entailment problem is decidable, although with a high complexity. SPEN focuses on a smaller class of inductive definitions that is, however, expressive enough to specify complex dynamic data structures, such as skip lists, lists of circular lists, AVL trees, or binary search trees.

The chosen class of inductive definitions enables the design of efficient (semi-)decision procedures for satisfiability and entailment [START_REF] Enea | Compositional Entailment Checking for a Fragment of Separation Logic[END_REF][START_REF] Enea | On Automated Lemma Generation for Separation Logic with Inductive Definitions[END_REF]. The key idea used for satisfiability checking in SPEN is to exploit the semantics of restricted inductive definitions and of separating conjunction to build an equisatisfiable boolean abstraction of the formula. For entailment checking, the idea is to reduce the problem of checking ϕ ⇒ ψ to the problem of checking a set of simple entailments where the right-hand side is an inductive predicate atom. The compositionality of this reduction leads to high efficiency (the simple entailments can be checked independently) and to a capability to provide fine diagnosis for invalid entailments.

The current version of SPEN improves on the ones reported in [START_REF] Enea | Compositional Entailment Checking for a Fragment of Separation Logic[END_REF][START_REF] Enea | On Automated Lemma Generation for Separation Logic with Inductive Definitions[END_REF] in several directions. First, we introduced caching of constructions and results obtained from checking simple entailments in order to increase its efficiency. Second, the wrappers calling the SAT and SMT solvers have been refined to generate smaller formulas and to exploit the incrementality feature of underlying solvers. Third, we improved the diagnosis produced by SPEN. For satisfiability checking, SPEN now provides either a model of a satisfiable formula or an unsatisfiable core; for entailment checking, SPEN provides a proof witness for valid entailments and a diagnostic information otherwise.

SPEN has been successfully tested on a quite large benchmark. The first version of SPEN participated in the SL-COMP'14 contest [START_REF] Sighireanu | Report on SL-COMP'14[END_REF] where it won one of its divisions and was second in another one. The later extensions now allow SPEN to handle a richer fragment than those considered in the competition. Moreover, the improvements above lead to better execution times (e.g., by 10 % within the SL-COMP'14 division won by the first version of SPEN and by 30 % on the division where SPEN was the second).

SPEN is not the only solver for SL. The existing solvers differ in the fragment considered (CYCLIST [START_REF] Brotherston | A Generic Cyclic Theorem Prover[END_REF], SLIDE [START_REF] Iosif | Deciding Entailments in Inductive Separation Logic with Tree Automata[END_REF]) and/or the techniques used (ASTERIX [START_REF] Pérez | Separation Logic Modulo Theories[END_REF], DRYAD [START_REF] Qiu | Natural Proofs for Structure, Data, and Separation[END_REF], GRASSHOPPER [START_REF] Piskac | Automating Separation Logic Using SMT[END_REF], SLEEK [START_REF] Chin | Automated Verification of Shape, Size and Bag Properties via User-defined Predicates in Separation Logic[END_REF]). A detailed comparison with these solvers is beyond the scope of this paper-we refer the reader to the survey in [START_REF] Enea | Compositional Entailment Checking for a Fragment of Separation Logic[END_REF][START_REF] Enea | On Automated Lemma Generation for Separation Logic with Inductive Definitions[END_REF][START_REF] Sighireanu | Report on SL-COMP'14[END_REF].

Logic Fragment

SPEN deals with decision problems in a fragment of SL, denoted as SL ID , that combines the symbolic heaps fragment of SL [START_REF] Berdine | A decidable fragment of separation logic[END_REF] with user-defined inductive predicates describing various kinds of lists (possibly nested, cyclic, or equipped with skip links) or trees, possibly extended with data constraints. Syntax: We write X, Y, Z to denote location variables, d to denote data variables, and x, y, z for both kinds of variables. We use the vector notation x to abbreviate tuples. We denote by ρ the tuples built from pairs of field labels and variables that specify structured values. We assume a finite set P = {P 1 , . . . , P n } of predicate symbols, each with an associated arity, and a special location variable nil. A symbolic heap formula ψ is a formula of the form ∃ x • Π ∧ Σ where Π is a pure formula and Σ is a spatial formula with the following syntax:

Π ::= X = Y | X = Y | ∆ | Π∧ Π Σ ::= emp | X → ρ | P (X, x) | Σ * Σ
Here, ∆ is a constraint over data variables. We let it unspecified, though SPEN presently supports the first-order theory over multisets of integers with integer linear constraints. The spatial atoms (i.e., the empty heap, the heap cell allocated at X, resp. the heap region shaped by some predicate P ∈ P) are composed by the separating conjunction " * ". An SL ID formula ϕ is a set of symbolic heaps interpreted as a disjunction ∨ i ψ i .

Predicates P ∈ P are defined by a set of inductive rules of the form ψ ⇒ P (X, x) where (X, x) is a tuple of distinct variables including all free variables in the symbolic heap ψ (the rule body). X is called the root node of the heap segment defined by P . A rule is called a base rule if its spatial part is emp, i.e., an empty heap; otherwise, it is an inductive rule. Fragments: SPEN considers a restricted class of inductive rules such that the defined predicates specify (possibly empty) heap segments connecting (by location fields) the root location X with all locations in the heap or nil. The restrictions have been defined formally in [START_REF] Enea | Compositional Entailment Checking for a Fragment of Separation Logic[END_REF][START_REF] Enea | On Automated Lemma Generation for Separation Logic with Inductive Definitions[END_REF]. They mainly require, for each inductive predicate P , the presence of a unique base rule and inductive rules where the root X points to a memory cell that contains at least one field from which another heap specified by P starts. The fragment defined in [START_REF] Enea | Compositional Entailment Checking for a Fragment of Separation Logic[END_REF], called SL ID L , can describe various kinds of lists that can be singly-or doubly-linked, cyclic, nested, and can have skip links. It does not permit data constraints and inductive tree structures. On the other hand, the fragment SL ID D defined in [START_REF] Enea | On Automated Lemma Generation for Separation Logic with Inductive Definitions[END_REF] permits data constraints and can describe tree structures of bounded width, such as sorted list segments, AVL trees, binary search trees, but not nested cyclic lists.

Decision problems: For both fragments above, SPEN considers the problems of checking satisfiability of a formula, i.e., checking whether |= ϕ holds, and the validity of an entailment ϕ ⇒ ϕ where the symbolic heaps of ϕ can be quantified only over data variables. A simple example of an entailment problem in SL ID L considered by SPEN is:

∃Y, W. X = Z ∧ X → {(next, Y )} * sll(Y, W ) * W → {(next, Z)} ? ⇒ sll(X, Z),
which, intuitively, checks whether a composition of two memory cells specified by the points-to atoms X → {(next, Y )} and W → {(next, Z)} and the predicate atom sll(Y, W ) describes a set of heaps that are all also models of the predicate sll(X, Z) defining an acyclic singly-linked list segment between X and Z. L , SPEN has the option of returning a model of ψ obtained from a model of B[ψ] by unfolding predicate atoms corresponding to non-empty heap segments. The unfolding of predicate atoms is done twice to emphasize the non-emptiness of the segment. For ψ ∈ SL ID D , the satisfiability checking continues by constructing a formula ∆ ψ that conjuncts the data part of ψ with the data parts obtained by unfolding the non-empty heap segments given by the model of B[ψ]. To check the satisfiability of ∆ ψ , SPEN queries an SMT solver for the theory of multisets with integer data (currently, SPEN implements a wrapper for the UFLIA theory of Z3 [START_REF] Moura | Z3: An Efficient SMT Solver[END_REF]).

Satisfiability Checking

If the boolean abstraction B[ψ] is satisfiable, it is then used to normalize the spatial part of ψ, which is a step used by entailment checking too. This process saturates the pure part of ψ with (dis-)equalities between locations variables and removes predicate atoms that correspond to empty heap segments, producing a normalized formula ψ .

Entailment Checking

Spen {P 1 . . . , P n }, ψ 1 ⇒ ψ 2
Parsing and typing

ψ 1 P i P i

Build tree automata

ψ 2 Boolean abstraction B[ψ 1 ] B[ψ 2 ]
Normalization & building SL graphs

G[ψ 1 ] G[ψ 2 ]
TA i Solving simple entl.

Reduction to simple entl.

SAT solver

    

Proof witness or failure diagnostics

Vata tree automata library Fig. 2: SPEN workflow for entailment SL L To check the validity of an entailment ϕ 1 ⇒ ϕ 2 , SPEN uses a sound procedure to deal with disjunctive formulas: it checks that for every disjunct ψ 1 in ϕ 1 , there is a disjunct ψ 2 of ϕ 2 such that ψ 1 ⇒ ψ 2 . The procedure for deciding the validity of entailments between symbolic heaps follows the workflows given in Fig. 2 and Fig. 3 (the theoretical foundations were established in [START_REF] Enea | Compositional Entailment Checking for a Fragment of Separation Logic[END_REF][START_REF] Enea | On Automated Lemma Generation for Separation Logic with Inductive Definitions[END_REF]). The two formulas are first checked for satisfiability and normalized using the procedures from Section 3. If one of the two formulas is unsatisfiable, then the validity of the entailment can be already determined, e.g., if ψ 1 is unsatisfiable then the entailment is valid. When both formulas are satisfiable, SPEN offers two different procedures tuned for each fragment of SL ID .

For the fragment SL ID L , SPEN reduces the entailment problem ψ 1 ⇒ ψ 2 to a set of entailment queries of the form ψ 1 [a] ⇒ a, called simple entailments, where ψ 1 [a] is a sub-formula of ψ 1 and a is a (points-to or inductive) spatial atom of ψ 2 (there will be one such entailment for each spatial atom a in ψ 2 ). Intuitively, the sub-formula ψ 1 [a] describes the region of a heap modelled by ψ 1 that should satisfy a. The procedures for computing ψ 1 [a] and testing simple entailments use an intermediary graph representation of symbolic heap formulas, called an SL-graph and denoted G[ψ]. Basically, nodes of G[ψ] represent sets of aliased variables according to the pure part of ψ, and edges represent dis-equalities and spatial atoms of ψ, e.g., a spatial atom P (X, Y, x) is represented by a directed edge from X to Y labeled by P ( x). Thus, when a is a predicate atom P (X, Y, x), ψ 1 [a] is obtained from the SL-graph of ψ 1 by selecting the edges reachable from X and co-reachable from Y . The graph selected for ψ 1 [a] is transformed 1) are obtained by applying the inductive rules and lemmas obtained automatically thanks to restriction required on inductive definitions. The procedure requires to check entailments between data constraints, which is done using the previously mentioned wrapper to the SMT solver.

For both procedures, when the input entailment ψ 1 ⇒ ∃ d. ψ 2 holds, SPEN has the option of providing a proof witness that either indicates the fact that ψ 1 is unsatisfiable or it consists of the normalized forms of ψ 1 and ψ 2 and the mapping of sub-fomulas in ψ 1 to atoms of ψ 2 . When the input entailment is not valid and the procedure terminates, SPEN provides a diagnosis that explains why the entailment fails.

Experimental Results

SPEN has been applied to a benchmark of 578 problems (available in the repository), 90 % obtained from verification conditions of iterative programs on complex dynamic data structures. The remaining problems are crafted to test the capabilities of the solver. Tables 1 and2 provide an overview of results obtained by SPEN on this benchmark.

The benchmark of SL ID L problems includes three divisions of SL-COMP'14: satisfiability and entailment problems for acyclic singly linked lists (sll0 sat resp. sll0 entl), and entailment checking for formulas describing more complicated types of linked lists, e.g., doubly-linked lists, skip lists, and nested lists (FDB entl). SPEN spends less than 0.05 s on 90 % of the problems with the maximum time of 0.5 s; these times include calls to a SAT solver. The benchmark FDB entl + includes the problems not in the SL-COMP'14 benchmark (e.g., formulas describing lists of cyclic lists). The reported times in the last column have been obtained in 2014 on the StarExec5 platform. The benchmark of SL ID D problems (see Table 2) includes verification conditions for proving the correctness of iterative procedures (delete, insert, search) over recursive data structures storing integer data: sorted lists, binary search trees, AVL trees, and red-black trees. SPEN spends less than 0.4 s on each problem, including calls to SAT and SMT solvers. The first three lines of Table 1 demonstrate that the two approaches implemented in SPEN (based on tree automata-column "SPEN L "-and on proof search-column "SPEN D ") are not only complementary but also comparable on the common fragment. The improvements discussed in this paper reduce the execution times by 10 % within the division sll0 entl and by 30 % within FDB entl w.r.t. the old version [START_REF] Enea | Compositional Entailment Checking for a Fragment of Separation Logic[END_REF].

Spen {P 1 Fig. 1 :

 11 Fig. 1: SPEN workflow for satisfiability checkingGiven a set of inductive definitions P and a symbolic heap ψ, the procedures for checking satisfiability in SPEN follow the workflow given in Fig.1. The satisfiability checking of an SL ID formula ϕ makes a classic use of this basic procedure. The crux of the procedures for both fragments is the definition of a boolean formula B[ψ], called boolean abstraction, such that the data-free part of ψ is satisfiable iff B[ψ] is satisfiable[START_REF] Enea | Compositional Entailment Checking for a Fragment of Separation Logic[END_REF][START_REF] Enea | Compositional Invariant Checking for Overlaid and Nested Linked Lists[END_REF].Once the boolean abstraction B[ψ] is computed, SPEN queries a SAT solver (currently, MINISAT4 ) for the satisfiability of B[ψ]. If B[ψ] is unsatisfiable, SPEN can return an unsatisfiable core of ψ, deduced from an unsatisfiable core of B[ψ]. If B[ψ] is satisfiable and ψ ∈ SL ID L , SPEN has the option of returning a model of ψ obtained from a model of B[ψ] by unfolding predicate atoms corresponding to non-empty heap segments. The unfolding of predicate atoms is done twice to emphasize the non-emptiness

Table 1 :

 1 Experimental results on an Intel(R) Core(TM) i7-2600 CPU at 1.60GHz , which is tested for membership in the language of a tree automaton built from the rules defining P for the atom a = P (X, Y, x).

	Fragments		Time [s]	SL-COMP'14 results
	SL ID L SL ID D	Benchmark Size SPEN L SPEN D	Time [s] StarExec/solver
		sll0 sat 110 11.20 11.28 (I) 1.06 / Asterix, (II) 3.27 / SPEN
		sll0 entl 292 34.45 34.94 (I) 2.98 / Asterix, (II) 7.58 / SPEN
		FDB entl 43	1.08 1.00 (I) 0.61 / SPEN, (II) 43.65 / SLEEK
		FDB entl + 55	0.65 -	-
	{P 1 , . . . , P n }, ψ 1 ⇒ ψ 2 into a tree t 1 Spen For the fragment SL ID D , SPEN implements a proof search strat-egy for the entailment problem Parsing and typing ψ 1 ⇒ ∃ d. ψ 2 . The strategy computes a sequence of formulas
	∃ d 1 . ψ 1 1 , . . , ∃ d n . ψ n 1 such that (1) ∃ d i . ψ i 1 and 1 ⇒ ∃ d i+1 . ψ i+1 1 is syntactically equiv-(2) ∃ d n . ψ n alent to ∃ d. ψ 2 . The entailments in point (	P i P i Build lemmas	ψ 1 Boolean abstraction ψ 2 B[ψ 1 ] B[ψ 2 ] Normalization	  	Proof witness SAT solver SMT solver
				Proof search	 	or failure diagnostics
			Fig. 3: SPEN workflow for entailment in SL ID D

Table 2 :

 2 Results for SL ID

			D
	Benchmark	Size Time [s]
	sll0 sorted 16	0.45
	BST	45	1.67
	AVL	22	1.21
	RBT	21	3.61

https://github.com/mihasighi/spen

Available at http://minisat.se.

www.starexec.org, an Intel(R) Xeon(R) CPU E5-2609 at 2.40GHz of and 10 MB cache.

Acknowledgement. This work was supported by the French ANR project Vecolib, the Czech Science Foundation (project 17-12465S), the BUT FIT project FIT-S-17-4014, the IT4IXS: IT4Innovations Excellence in Science project (LQ1602), and by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 678177).


Georis Creuseveau
email: jade_creuseveau@yahoo.fr

F Gourmelon

M Rouan

THE CIAO: WEB PORTAL OF GEOGRAPHIC INFORMATION FOR WEST AFRICA

Keywords: ICZM, GEOGRAPHICAL INFORMATION, METADATA, WEB PORTAL, WEST AFRICA

This paper describes the "CIAO" project, based on an international initiative, part of the « Programme Régional de Conservation de la Zone Côtière et Marine d'Afrique de l'Ouest » or PRCM (Regional Program for the Conservation of the Coastal and Marine Area of West Africa). It leads to a web portal of information for the West African coastal zone. Investigations among the main producers of information have led to a first inventory of available geographical information. The information has been described in metadata files (ISO 19115) which have been collected into a catalogue based on a generic, multi-language client server application (MDWEB). The first version of CIAO gathers 236 metadata files that deliver information about geographical data on natural, human and regulatory parameters from local to regional levels and with various quality standards.

INTRODUCTION

The West African coastal region is an area of strategic development. Important economic activities such as fisheries, tourism, transportation and the oil industry are concentrated on the littoral zone, resulting in a high level of degradation. In many cases, rapid development has been dictated by climactic and political crises, and it has taken place without any planning or cross-industry consultation. This has led to significant territorial changes which have resulted, in turn, in the degradation of the coastal area and its resources. It has also created conflicts of interests across the various industries involved. Within this framework, the need for appropriate coastal management in West Africa is both obvious and urgent if the environment and its resources are to be preserved. In response to this need, the PRCM has been established. Its aim is to coordinate the efforts of institutions and individuals involved in conserving the coastal region of the following West African coastal countries: Mauritania, Senegal, Gambia, Guinea-Bissau, Guinea, Sierra Leone and Cape Verde [START_REF] Prcm | Stratégie régionale pour les Aires Marines Protégées en Afrique de l'Ouest[END_REF].

With this in mind, the "Bilan Prospectif," anchor of the PRCM research's activities [START_REF] Quensière | Un réseau ouest-africain de recherche sur la gestion durable des zones côtières : le projet « Bilan prospectif[END_REF], seeks to achieve a synthesis of the West African coastal zone by establishing a Geographical Information Base driven by a Geographical Information System (GIS).

The first phase of this synthesis is an inventory of geographical information on the studied zone. This document introduces the implementation of this phase1 which resulted in a web-based catalogue of geographic information on West Africa.

METHOD

The method is based on simultaneous steps: creating the information inventory and choosing the catalogue application.

Data inventory

Interviews conducted between February and June 2006 with 38 West African public institutions and two French research organizations resulted in the first non-exhaustive inventory of available geographical information. Further to preliminary contacts, often based on recommendations from PRCM or Bilan Prospectif coordinators, interviews with the director or his or her representative and the person in charge of the database were held in the office of the institution. We preferred this kind of approach instead of using a standard survey sent by mail or email, so that we could guarantee answers and possibly consult existing databases [START_REF] Guineberteau | Approche des relevés terrain, Entretiens et enquêtes[END_REF]. During the interviews, geographical information were often presented, along with other related databases. We therefore decided to extend the inventory of geographical information to include databases that were formatted and managed coherently and that contained sufficient data to allow us to locate information and to consider integrating it later on within a geographic information base (e.g., fishing statistics that include the names of landing sites, weather data structured by station, etc.). This first inventory was supplemented by research on the Web which lead us to include five free, downloadable world-wide databases available for research and educational purposes.

Selection of the catalogue application

Four catalogue applications were tested in order to select the one best suited to the needs for the project (Table 1). For the study, the choice of the catalogue application is based on the following six criteria that are important so that end-users can make use of it: respect of the standard, free application, ease of use, possibility of archiving the resource, level of appropriation in West Africa, languages proposed by the catalogue application. In order to meet the needs of the catalogue of geographic information in West Africa, the comparison of the various tools led us to choose MDweb, which allows for the online management, consultation and diffusion of standardized metadata. Moreover, this choice also allows to capitalize the approach that Cape Verde has undertaken within the framework of the Sistema de informação Ambiental (SIA), or environmental information system. The structure of the described metadata is based on ISO standard 19115. This standard recommends that a large number of data be captured, not all of which are pertinent for all types of resources. The MDweb solution allows for the construction of templates, kinds of filters applied to the standard, according to the needs of each type of resource. The templates can also contain additional elements that extend the standard. This kind of template is used as model to structure the metadata captured [START_REF] Granouillac | Construction et usages d'infrastructures liées à l'information géographique ou comment « servir » l'information géographique[END_REF]. Moreover in MDweb, numerous functionalities ensure that certain fields of the input forms are reduced, automated or defined. Among these is an XML import module that allows metadata coming from other catalogue applications, including ArcCatalog, to be imported.

Adaptation of MDweb

The MDweb 1.4 version, developed by the Institute of Research and Development (IRD-France) and its partners, has been modified for CIAO to allow the development of a tailored catalogue which offers the possibility of online metadata file consultation, described resource archiving, and cataloguing. In particular, the consultation and cataloguing functions propose a cartographic interface that allows a geographical area to be defined about which the data files can be questioned or localized2 .

THE CIAO: MAIN FUNCTIONALITIES AND RESOURCES

The CIAO is based on six types of resources (templates) 3 : geographical information bases, relational databases, digital charts, vectors, rasters, spreadsheets. Geographical information bases and relational databases are classified as data collection. Other resources (vector and raster, numerical chart and sorter) are data sets (Roselt/OSS, 2004). Moreover, through the parent and daughter files, accessible via the cataloguing interface, the CIAO allows the possibility of creating connections between certain resources, as is the case, for example, between a geographical database and a vector to which it is attached. The "vector" and "raster" templates were completed in order to integrate the concepts of description, maintenance and conditions of use of the resource.

French metadata files, validated by the institutions that manage the data, are available at www.prcmarine.org/ciao. The CIAO homepage leads to the SIA portal, allowing a consultation of the Cape Verde metadata.

Functionalities

The CIAO offers three principal online functions: metadata file consultation, described resources archiving, and cataloguing.

To consult metadata, three types of search can be used: map searches, data-type searches, and multi-criteria search. Users can search with their own key words or the ones suggested by three thesaurus included within the CIAO. As a complement to the default GEMET 4 and AGROVOC 5 thesauruses offered by MDweb, the CIAO gives access to a list of specific key words related to the specific West African information gathered.

The CIAO can also be used as an archiving tool for the described resources. This function allows a physical hosting of the information (images, maps, vector layers, etc.) within the server, to ensure survivability. Downloading is controlled by the institution manager of the data, due to the private/public option suggested during the "hanging" of the resource within the metadata file. In its first version, the CIAO contains no resources; conventions will have to be established between the PRCM and the producers.

The choice of what type of resource to tag will give the user access to a form to capture the metadata. The cataloguing interface guides the user throughout the process. The cartographic interface is always available throughout cataloguing so that the batch of data can be easily located. Some of the cataloguing fields of the form are mandatory. They correspond to the core of ISO standard 19115, which consolidates the elements necessary to identify the resource and to obtain an appreciation of its contents. Online assistance is CIAO was approved by the UNEP-WCMC (http://www.unep-wcmc.org/) which is the manager and the conservator. The layer of information about the protected areas was supplemented by some polygons provided by the network of PRCM-protected areas. The other vector layers are extracted from the Vector Map Level 0 Vmap 0 (DIGITAL Chart of the World), Edition: 5, zone SOAMAFR (Africa and South America) of the NGA (National Geospatial Intelligence Agency), whose data are in the public domain.

3

The resources of the type "chart paper" and "presentation" were not regarded as priority in this first phase. The gauges relating to these resources, proposed by defect in MDweb, were withdrawn from the current version of the CIAO 4 GEMET: General European Multilingual Environmental Thesaurus, developed by the European Environment Agency, which contains approximately 5,000 words relating to the environment. http://www.eionet.europa.eu/gemet 5 AGROVOC: multilingual thesaurus concerning agriculture, forestry, fishing, food and associated fields (like the environment) developed by FAO. http://www.fao.org/aims/ag_intro.htm accessible any time through the drop-down menus of each window. The home page also offers consultation assistance and step-by-step details of the consultation function.

Resources

Interviews with the main producers of information involved in West Africa (public institutions, research organizations from the South and the North, etc.) have allowed us to draw up a first, non-exhaustive inventory of available geographical information. This information has generally been produced for several space scales and at different points in time, within a well defined framework established by the research programs and the development or conservation projects.

The first version of CIAO, online in early 2007 (www.prcmarine.org/ciao), includes 236 metadata files that provide information on different types of resources (geographical information bases, relational databases, digital charts, vectors, rasters, spreadsheets) representing (Figure 1) : -three different areas: natural, human and regulatory; -various levels of space scales: from local to regional; and -variable quality standards: levels of precision, exhaustiveness, and timeliness. A first analysis of the CIAO resources gives a picture of the geographical information available within the surveyed institutions. Identified information relates mainly to the "natural" factor (40%) and "human" factor (39%). Information established at the territorial space scale (between ½ 000 and 1/200 000) and the national space scale (between 1/200 000 and 1/500 000) are also most numerous.

Senegal seems to have more data than other countries. Most of the resources relate to the marine protected areas and other zones of ecological interest (53 resources). This finding is supported by the many studies carried out about national parks and reserves. Mauritania, which also has a great deal of data, shows a predominance of resources on a national scale (43), due to the number of studies of coastal zone management. Cape Verde, thanks to the inventory completed within the framework of the SIA project, is also well endowed with data, especially on the national scale (45). Guinea-Bissau mainly has data concerning the archipelago of Bijagos (38). Gambia, with only two geographical information bases on the national scale, shares with the other countries the data established across West Africa (13) and the world data bases in the public domain ( 21).

OUTLOOK

The catalogue, currently located on a server based in France (University of Bretagne Occidentale) will be transferred during 2007 to a West African institution that will have the responsibility for managing the tool and its associated databases. PRCM will have to choose this institution by taking into account various technical, financial and human parameters to guarantee the continuity of the catalogue. This first version of CIAO will grow gradually through the integration of new metadata files. The cataloguing interface allows the description of the resource via forms accessible to the users referred by the system administrator. Newly produced data or data that do not yet have metadata will thus be integrated, online, in the database of the CIAO catalogue. If the interactive updating of the catalogue by the producers isn't operative, annual interviews could be planned, as they were for the original implementation, to meet the information producers and create new metadata files. This method would, on one hand, validate the metadata created online independently by the institution. On the other hand, it would be able to meet new data producers and integrate them into the CIAO user networks.

Other data inventories relating to the West African coastal zone are currently being developed: SIA in Cape Verde [START_REF] Raulin | Mise en oeuvre du Sistema de Informação Ambiental (SIA) au Cap-Vert[END_REF], OLM in Mauritania [START_REF] Pennober | La démarche SIG de planification côtière en Mauritanie[END_REF], Metalinus of C3EDOA/IRD Dakar, Canary Current Large Marine Ecosystem. Although some of these initiatives already collaborate with the CIAO with respect to tools or metadata, a harmonization of the existing catalogues could be planned in order to offer a unique global portal giving access to all information available on the study zone.

CONCLUSION

Investigations among the main producers of information for West Africa (public institutions, research organizations from the South and the North, etc.) have allowed a first, non-exhaustive inventory of available geographical information to be drawn up.

Because of the wide range of data listed among the 40 institutions visited, the information has been described in standard metadata files (ISO 19115 format) to ensure its coherence and comparability and that it can be shared by the stakeholders involved in the West African coastal zone. The metadata files have been collected into a Catalogue of Information for West Africa (CIAO), thanks to MDWEB, and they are accessible online, free of charge, at www.prcmarine.org/ciao. The first version of CIAO includes 236 metadata files that offer information on different types of resources representing different areas: natural, human and regulatory; various levels of space scales and variable quality standards. CIAO is a dynamic tool which will grow and gain from increased collaboration with all "coastal players". Nevertheless, its operation depends now on the involvement of the African western organization that will take responsibility for hosting the CIAO and on the availability of an administrator who will ensure its management.

The main aim of this type of application is to increase the opportunities to gather and exchange dispersed and heterogeneous information. This is likely to support multi-sector and interdisciplinary approaches as well as increase the level of knowledge of local stakeholders and decision makers [START_REF] Gourmelon | Apports des SIG à la connaissance et à la gestion de l'environnement côtier, exemples choisis en Mauritanie, Guinée-Bissau et Côte d'Ivoire[END_REF].The creation of the CIAO constitutes the first stage of the feasibility study of a Geographical Information System dedicated to the coastal zones of the PRCM.

Figure 1 :

 1 Figure 1: The CIAO structure and its resources

Table 1 . Comparison of the catalogue applications Tool Iso 19115 Open source / free Ease of use Resource archiving Level of appropriation in West Africa

 1

	Language

This joint study was completed within a cooperative and conventional framework between the UICN, the FIBA and the CNRS-University of Bretagne Occidentale (France).

The cartographic interface is based on four layers of information (coastline, country of the PRCM countries, capitals, and network of PRCM-protected areas) in order to guarantee an easy access whatever the quality of the Internet connection. The data relating to the protected areas result from the World Database on Protected Areas (WPDA) of the UNEP-WCMC and the WCPA consortium. The use of this information within the framework of the

Acknowledgements:

We would to thank all those from the South and the North who took part in the implementation of the steps presented in this article.


Marta Galera Martinez

Doan Pham
email: doan.phamminh@mines-albi.fr

Ange Nzihou

Patrick Sharrock

Marta Galera Martínez

Valorization of calcium carbonate-based solid wastes for the treatment of hydrogen sulfide in a semi-continuous reactor

Keywords:

come

Introduction

Hydrogen sulfide (H 2 S) is an acid gas pollutant released by several industrial process and agricultural activities. Some of them are petroleum refineries, natural gas plants, petrochemical plants, coke oven plants, biogas plants and geothermal power plants, pulp and paper operations, municipal sewers and sewage treatment plants, swine containment and manure-handling operations, food processing plants, tanneries, etc. [START_REF] Cullis | Atmospheric sulphur: natural and man-made sources[END_REF][START_REF] Ros | Dried sludges and sludge-based chars for H 2 S removal at low temperature: influence of sewage sludge characteristics[END_REF][START_REF] Pham Xuan | Valorization of calcium carbonate-based solid wastes for the treatment of hydrogen sulfide from the gas phase[END_REF][START_REF] Kim | Mechanisms of hydrogen sulfide removal with steel making slag[END_REF]. H 2 S emissions concentration varies in a large range from ppmv to volume percentages, which depends on the industrial facility. These emissions are considered as sources of obnoxious odors, perceptible even at very low levels. In fact, the odor threshold of H 2 S can range from 0.5 ppb to 0.3 ppmv [5] that usually causes a nuisance to neighbors of above-mentioned industrial sites. However, the perception of the odor disappears at higher concentrations (150-200 ppmv [5]) when the gas becomes an extreme health hazard. In fact, the exposure under these concentration levels for some hours is enough to produce severe and irreversible injuries or even death. Thus, smell is not a reliable indicator to recognize the presence of this toxic gas. H 2 S is also associated with environmental problems. The oxidation of H 2 S results in the release of sulfur dioxide (SO 2 ) that is the principal culprit of acid rain [START_REF] Seinfeld | Atmospheric Chemistry and Physics: From Air Pollution to Climate Change[END_REF]. Even at lower concentration, in the order of dozens to hundreds of ppmv, H 2 S causes extensive damage in piping and equipment by corrosion. This leads to a rise in maintenance cost due to repair or/and replacement of affected facilities.

Several methods for the H 2 S treatment were studied. Standard technologies are chemical absorption using basic reactants and/or oxidizing agents, the adsorption on activated carbon or other adsorbents, and biological processes. The efficiency of these processes has been demonstrated at industrial pilot scale [START_REF] Biard | Hydrogen sulphide removal in waste water treatment plant by compact oxidative scrubbing in Aquilair Plus TM process[END_REF][START_REF] Kerc | Ozonation of odorous air in wastewater treatment plants[END_REF][START_REF] Wu | A pilot study of a biotrickling filter for the treatment of odorous sewage air[END_REF]. However, these processes still need to be improved, in particular to reduce operational cost and overcome limits of operation conditions. For example, the performance of biofilters depends strongly on the weather conditions because bacteria work under a determined temperature range [START_REF] Cox | Odor and volatile organic compound treatment by biotrickling filters: pilot-scale studies at Hyperion treatment plant[END_REF][START_REF] Van Der Heyden | Mitigating emissions from pig and poultry housing facilities through air scrubbers and biofilters: state-of-the-art and perspectives[END_REF].

Several industrial processes (soda-ash process, oil and gas production, etc.) produce a large volume of residual brines with important amounts of calcium-rich and/or magnesium-rich minerals. The accelerated carbonation of these residual brines has been proposed as a method for CO 2 sequestration. During this process, called "mineral carbonation", CO 2 reacts with the alkali divalent cations Ca 2+ and/or Mg 2+ and their oxides (CaO and/or MgO) to produce carbonates particles that are stable at atmospheric conditions [START_REF] Kirchofer | Assessing the potential of mineral carbonation with industrial alkalinity sources in the U.S[END_REF][START_REF] Liu | Experimental studies on mineral sequestration of CO 2 with buffer solution and fly ash in brines[END_REF]. These carbonates can be valorized for acid gas neutralization in dry or semi-dry flue gas treatment [START_REF] Filippova | Carbonation of residual brines produced by ammonia-soda process[END_REF][START_REF] Soong | CO 2 sequestration with brine solution and fly ashes[END_REF].

In this work, we show the efficiency of calcium carbonate-based solids, which have been precipitated during the carbonation of residual brines from industrial facilities, in triphasic gas-liquid-solid process for removing H 2 S from the gas phase. Results obtained are very interesting from the performance standpoint. This offers the possibility for a future application at large pilot or industrial scale. The advantages of this process are triple: 1) The process uses environmentally-friendly materials taking into account the fact that carbonated-based solids are obtained by the stable sequestration of CO 2 into alkaline residual streams. This reduces the CO 2 emissions as the main greenhouse gas. 2) The carbonated-based solids can be valorized without further pre-treatment. This provides economic benefits. 3) H 2 S is efficiently removed even at trace amount under ambient conditions of temperature and pressure from the air atmosphere. Thus this triphasic process is interesting for the treatment of H 2 S emission from other sources, i.e. H 2 S in biogas, natural gas or syngas from pyro-gasification of wastes and/or biomass.

Materials and methods

Materials

Two solid wastes containing mainly calcium carbonate were used. The first one was formed by slow and natural carbonation of residual brines with atmospheric CO 2 for years. This solid is called thereafter NPC. The second one came from the artificial carbonation by CO 2 bubbling of the similar residual brines. This solid is designated thereafter APC. Both solid wastes existed in fine powder form. After drying at room temperature, they are sieved to eliminate the eventual particles larger than 315 µm (less than 1 wt%). No further treatment was done before characterization and use in H 2 S removal tests. A commercial calcium carbonate under fine powder form from Fischer Scientific (calcite, CaCO 3 , > 98%, ref. 10101710) was also used as reference material.

Analysis and characterization

Specific surface area was determined using the BET method. Samples were firstly degased in Micrometrics Vacprep 061. The adsorption-desorption isotherms were measured with a Micrometrics Tristar II 3020 using nitrogen as gas adsorbate. Scanning electron microscopy coupled with energy dispersive spectroscopy (SEM-EDX) was carried out on a Philips XL30 ESEM apparatus. Particle size distribution of solid powder was measured by laser scattering in a Mastersizer 3000 (Malvern Instruments Ltd) in the range of 0.020-2000 µm. Infrared spectroscopy (IR) was recorded on a Shimadzu FTIR 8400S spectrometer using a sensitive pyroelectric detector with an L-alanine-doped deuterated triglycine sulfate element. Thermogravimetry analysis (TG) was performed in a TA Instruments SDT Q600 analyzer with a heating rate of 5 °C/min under air flux (100 mL min -1 ). X-rays diffraction of solid samples was carried out using a Phillips Panalytical X'pert Pro MPD diffractometer, equipped with a copper X-rays source (K α of 1.543 Å). The data were collected in the 2θ ranges from 10 to 75°with a step size of 0.0167°. The identification of crystalline phases was based on the JCPDS database. Inductively coupled plasma atomic emission spectroscopy (ICP-AES) was performed using a HORIBA Jobin-Yvon Ultima 2. After test, the suspension was filtered and the liquid phase was analyzed by ion chromatography (ICS3000 DIONEX). Sulfide (S 2-) was measured with an amperometric detector using the column PA1 (250 × 4 mm) and the mobile phase containing 0.1 M NaOH and 0.5 M CH 3 COONa at the flow rate of 1 mL min

-1 . Sulfite (SO 3 2- ), thiosulfate (S 2 O 3 2-
) and sulfate (SO 4 2-) ions were measured with a conductimetric detector using the column AS11 (250 mm × 4 mm) and the mobile phase containing 30 mM KOH.

H 2 S removal test 2.3.1. Reactor and experimental procedure

Tests were carried out in a 250 mL glass stirred reactor (Fig. 1). For a given test, the reactor was firstly purged with dry air flow containing 200 ppmv of H 2 S (p.a. grade from Air Liquide), which is called thereafter waste air. It was fed to the reactor from the bottom via a porous glass disk. A desired volume of double-distilled water was fed into the reactor, under waste air flow (100 mL min -1 ) and under stirring (limited at 600 rpm for the glass reactor used in this work). When the double-distilled water was saturated in H 2 S, a desired quantity of sorbent was added to the reactor to start the H 2 S removal test.

Fig. 2 illustrates the different steps of a given H 2 S removal test in this work.

In Fig. 2, Zone 1 corresponds to the purging step of the reactor with the waste air stream. Zone 2 shows the dissolution of H 2 S in water, after filling the reactor with double-distilled water under stirring. When this water was saturated with H 2 S, sorption test was started by adding a sorbent to the reactor. The moment for solid addition to the reactor was considered as the zero time of H 2 S removal test (t o , Fig. 2). Zone 3 corresponds to the abatement of H 2 S by the sorbent added into the reactor. Typically, in Zone 3, the outlet concentration of H 2 S abruptly Fig. 1. Tri-phasic system for H 2 S removal at laboratory scale. dropped to zero within less than 2 min. Then, a plateau of outlet H 2 S concentration was observed. Within this plateau, the variation of outlet H 2 S concentration was small (+/-3 ppmv). This concentration was used to calculate the efficiency of H 2 S removal (Eq. ( 1)).

The outlet concentration of H 2 S was monitored every minute by a H 2 S analyzer (Gas Alert QUATTRO, from BW Technologies). All the experiments were carried out at room temperature and atmospheric pressure. The pH of the suspension was measured at the beginning and at the end of each experiment. Each experiment was carried out for at least 8 h with a semi-continuous process, wherein the volume of the active medium (suspension of solid waste) is practically unchanged, while the waste air continuously passes through the suspension. Each test was repeated at least three times to verify the repeatability. The standard deviation was found to be smaller than 1%.

For the study on the influence of experimental conditions on the removal of H 2 S, the efficiency of H 2 S removal is defined by the following equation:

= × - Eff H S H S H S (%) 100 [ ] [ ] [ ] G i G o G i 2 , 2 , 2 , (1)
where

H S [ ] G i 2
, was the concentration of H 2 S at the inlet of the reactor (200 ppmv); and

H S [ ] G o 2
, was the concentration of H 2 S at the outlet of the reactor, after reaching the plateau as shown in Fig. 2.

Choice of operational parameters

According to the 'Arrhenius low', the kinetic constant of a reaction increases as temperature increases. Nevertheless, increasing the temperature has a negative effect on gas and solid solubility. As the temperature increases, the solubility of a gas decreases. Similarly, the solubility of calcite (the major component in the solid wastes) decreases as the temperature increases. In order to promote the mass transfer of the solid and the gas to the liquid phase, low temperatures are recommended. In this work, the ambient temperature was chosen.

Pressure does not significantly affect the calcite solubility. However, gas solubility is improved at higher pressures but this may result in higher operating and maintenance costs for industrial-scale applications. Thus, atmospheric pressure was chosen in view of the development of an economically-competitive process.

The optimal gas flow rate was obtained experimentally and set at 100 mL/min for this triphasic reactor [START_REF] Galera-Martinez | Valorisation des residus carbonates industriels pour le traitement de sulfure d'hydrogene dans les effluents gazeux[END_REF]. Lower values of the gas flow rate produced preferential flow paths in the gas diffuser (because of the various pore diameter of the glass porous disk), as well as solid decantation. For higher values the gas flow rate, the stirring speed should be increased to ensure good dispersion of the waste air in the liquid phase which increases operational cost. Moreover, the impact of the hydrodynamic of the system must be considered. If the stirring speed and the physicochemical properties of the suspension are supposed constant, an increase in the gas flow makes bubbles diameter larger and consequently the gas-liquid interfacial area a is reduced (Eq. ( 3)). Also, a high gas flow rate increases the rising speed of bubbles thus the contact time between three phases is reduced. Both have a negative impact on the mass transfer and consequently on the efficiency of the process.

The Eq. ( 1) could be transformed as follows:

= Eff T P Q ( / ) H S G H S 2 2 R N (2)
where N H2S is the rate of mass transfer of H 2 S (mol H 2 S/s) at a given time t of the H 2 S removal process, P H2S is the partial pressure of H 2 S in the inlet gas (atm), Q G is the volumetric flow rate of the gas (L/s), R is the universal gas constant (0.0814 atm L/mol K) and T the temperature (K). At the same time, N H2S is defined as follow [START_REF] Cussler | Diffusion: Mass Transfer in Fluid Systems[END_REF][START_REF] Vilmain | Kinetic study of hydrogen sulfide absorption in aqueous chlorine solution[END_REF]:

= - K a C C EV ( ) H S L L E L 2 N ( 3
)
where K L is the liquid phase mass transfer (m/s), a is the gas-liquid interfacial area per unit of volume (m 2 /m 3 ), C L E is the equilibrium concentration of H 2 S in the liquid (mol/m 3 ) and C L is the concentrations of H 2 S in the bulk of the liquid (mol/m 3 ), E is the enhancement factor by the solid and V is the suspension volume. Mass transfer parameters as K L and a are dependent of hydrodynamics. In consequence, some hydrodynamic parameters like stirring speed are also considered in the study.

In this work, stirring speed was varied from 200 to 600 rpm, which is the limit of the glass reactor. Other experimental parameters like the residues loading, the suspension volume, and the inlet concentration of H 2 S were also investigated and are mentioned in the next sections.

Results and discussion

Characterization of calcium carbonate-based solids

Fig. 3 shows the particle size distribution of these three sorbents, obtained by the laser scattering (Mastersizer 3000, Malvern Instruments Ltd). Both solid wastes (APC and NPC) had the similar particle size distribution with different populations of particles, rising up to around 400 µm. On the other hand, the commercial calcite from Fisher Scientific contained smaller particles (< 35 µm) compared to the solid wastes with a bimodal distribution. In all cases, these solids are favorable for the preparation of aqueous suspension in batch reactor.

Table 1 shows that both solid wastes contained calcium carbonate as the main component. Several impurities were also present in these solid wastes. In most of cases, APC contained more impurities than NPC, except for Fe. In addition to these main elements, both APC and NPC contained other minerals at trace amounts including Si (up to 2000 ppm), Al, Zn, Ni and Cu (up to 100 ppm). The presence of chlorine was due to the residual CaCl 2 and/or NaCl from the brine, which are all water soluble. NPC contained less chlorine than APC because NPC was landfilled for years and thus, most of chlorine compounds were leached under natural conditions. To check this hypothesis, aqueous suspensions of 10 wt% of APC and NPC were prepared. They were then filtered and the filtrates were analyzed by ICP-AES and ion chromatography (Table 2). The results obtained confirmed that chlorine-containing and sulfur-containing compounds were more present in APC than in NPC. The specific surface area (S BET ) of the solid before and after dispersing in the aqueous solution was analyzed by BET method (Table 3). Both APC and NPC were non-porous solids with low specific surface area. No significant change was observed for NPC after dispersion in an aqueous suspension. For APC, the specific surface area slightly increased from 2 to 5 m 2 g -1 , probably due to the leaching of various species as shown in Table 2. For comparison, the commercial calcite used in this work was also non-porous and had the specific surface area of 2 m 2 g -1 .

XRD analysis (not shown in this paper) showed that calcite was the principal crystalline phase of calcium carbonate [START_REF] Galera-Martinez | Valorisation des residus carbonates industriels pour le traitement de sulfure d'hydrogene dans les effluents gazeux[END_REF]. The presence of calcite in NPC and APC is also confirmed by FTIR analysis (Fig. 4). All samples had the characteristic peaks of calcite at 1390, 872 and 712 cm -1 . Commercial calcite and NPC showed another small characteristic peak at 848 cm -1 . No presence of vaterite was identified [START_REF] Sato | Structure of vaterite and infrared spectra[END_REF]. The peak at 854 cm -1 in APC is characteristic of aragonite, a polymorph of calcium carbonate. Peaks at 1136 and 1012 cm -1 which were due to the presence of CaSO 4 -based compounds (anhydrite, basanite: CaSO 4 •0.5H 2 O, and gypsum: CaSO 4 •2H 2 O) were also observed for APC [START_REF] Grandjean | Reactivity and valorization of products issued from carbonation of saline waste solution[END_REF].

Influence of stirring speed

Stirring speed is a hydrodynamic parameter that impacts the mass transfer. Fig. 5 shows the dependency of the efficiency on the stirring speed. According to Whitman's theory, transfer coefficient k is directly proportional to the diffusion coefficient and inversely proportional to the film thickness (k = D/δ). The stirring speed improves the turbulence reducing δ and increasing k (for both gas-liquid and solid-liquid transfer). Also, the stirring speed can improve gas-liquid mass transfer by increasing the gas-liquid interfacial area a and the gas hold-up.

Fig. 5 shows that APC was more reactive than NPC. Adsorption must be negligible because of the low specific surface of the solids. On the other hand, the chemical absorption of H 2 S by species from the dissolution of the solid must be considered. The solid dissolution rate J B is described by the Noyes-Whitney equation [START_REF] Cussler | Diffusion: Mass Transfer in Fluid Systems[END_REF]:

= - J k a C C ( ) B S S B s B (4)
where k S is the solid-liquid mass transfer coefficient, a S is the solidliquid interfacial area per unit of volume, C BS is the saturated solubility of the solid in dissolution media and C B is the concentrations of the solid in dissolution media.

k S can be strongly influenced by stirring speed. It is usually estimated by the Sherwood equation [START_REF] Baehr | Heat and Mass Transfer[END_REF]:

= Sh cSc Re n n 1 2
(5)

where Sh, Re and Sc are the Sherwood, Reynolds and Schmidt dimensionless numbers. Sherwood number represents the ratio of the mass transfer rate to the diffusive rate. Schmidt number is the ratio of kinematic viscosity to the diffusive rate. Reynolds number depends on stirring speed. c, n1 and n2 are constants whose values depends on Re.

The viscosity and density of the suspensions are involved in the dimensionless numbers. These properties can be considered similar in both cases. Thus, the influence of the agitation on Re and consequently on k S is similar for both NPC and APC (0.7 10 -5 ≤ k S ≤ 3 10 -5 m/s depending on the speed agitation).

Considering the fact that all solids particles are under suspension, a S is not affected by the stirring speed. However, a S and C Bs of the two solid wastes were different from each other. APC was more soluble and had more impurities than NPC. For this reason, APC had a higher dissolution rate than NPC. In consequence, APC were more available to react with H 2 S in the liquid media.

Influence of solid loading and suspension volume

Aqueous suspensions containing various contents of solid wastes were tested for the removal of H 2 S. In the range of 0.2-9.5 wt% of solid, the initial pH of the suspensions varied slightly from 9.5 to 9.9. In all cases, the final pH of the suspension was found within the pH range of 8-9 thanks to the omnipresence of CaCO 3 -based particles which conditioned the pH of the suspension. The effect of ionic strength on gas solubility was assumed negligible.

Fig. 6(a) shows the efficiency of H 2 S removal as a function of the solid loading in aqueous suspension. For both solid wastes, the efficiency of the system increased with the increase of the solid loading. At 2.5 wt% of solid loading, the reactivity of these solid wastes was found to be higher than that of the commercial calcite. For each solid loading and under the similar operational conditions, APC also showed higher reactivity compared to that of NPC. The highest efficiency of H 2 S removal reached 95 and 98% at 5 and 10 wt% of APC, respectively. These values were close to the thermodynamic equilibrium of H 2 S in the aqueous and the gas phases. The difference on the reactivity of these solid wastes can be explained by their composition and structure. As mentioned before, APC was more soluble than NPC. Thus, the suspension of APC contained more reactive soluble species than that of NPC. These species, in particular metallic cations such as Ca 2+ , Mg 2+ , can catalyze the oxidation of sulfide-based species (S 2-, HS -) into sulfur compounds of higher oxidation state (elemental sulfur for example) [START_REF] Morse | The chemistry of the hydrogen sulfide and iron sulfide systems in natural waters[END_REF]. In addition, carbonate anions (CO 3

2-

), which were more available in the suspension of APC, could also neutralize soluble species of H 2 S (aq)s . This will be discussed in the next section.

Fig. 6(b) shows the influence of suspension volume of APC on the removal of the H 2 S. For each solid loading, H 2 S removal increased with the increase of suspension volume. However, the effect of suspension volume was less important at high solid loading because the abatement got close to the thermodynamic limit, as mentioned above.

Influence of the inlet concentration of H 2 S

The influence of the inlet concentration of H 2 S on the efficiency of the process is presented in Fig. 7. At the same inlet gas flow rate, the increase of concentration of H 2 S led to the increase of the rate of H 2 S removal (mmol min -1 , Fig. 7(a)). According to Henry's law, the solubility of a gas in a liquid is directly proportional to its partial pressure. As the inlet concentration of H 2 S increased, the concentration of soluble H 2 S increased. This favored the rate of H 2 S removal. Fig. 7(b) presents the efficiency of H 2 S removal as defined by Eq. (1). We found again that for each inlet concentration of H 2 S and under similar reaction conditions, APC was more reactive than NPC. For the suspension of NPC, H 2 S removal was close to 21% regardless the inlet concentration of H 2 S. On the other hand, H 2 S removal increased practically linearly with the suspension of APC, explained by the high reactivity of APC suspension.

Test of long reaction time

Fig. 8(a) shows the efficiency of H 2 S removal for 7 days test using the suspension containing only 0.2 wt% of APC. The choice of this diluted solution was for evaluating the sorbent saturation and/or the loss of reactivity of the suspension within a reasonable time of test (7 days). The first visual observation was the progressive consumption of APC particles. After 7 days of reaction, when the experiment was stopped, the solution was practically transparent. No solid particles were observed in suspension. There was only some "grey foam", which was deposited on the walls of the reactor (Fig. 8(d)).

Fig. 8(a) shows that H 2 S removal decreased with the reaction time from around 82% at the first day to around 32% at the last day of test. According to the consumption of APC particles, we suppose that the decrease of H 2 S removal must be related to the unavailability of reactive APC particles. APC particles were likely consumed during the test and this consumption was nearly completed after 7 days of test, under the reaction conditions used. After 7 days of test, the accumulated quantity of removed H 2 S reached 15 mg; the quantity of APC in this test being 200 mg for preparing 100 mL of suspension of 0.2 wt%. This means that the capacity of APC for H 2 S abatement according to this triphasic process can reach at least 75 mg per g of sorbent. This offers a new alternative solution to the conventional sorbents based on carbonaceous materials [START_REF] Seredych | Desulfurization of air at high and low H 2 S concentrations[END_REF][START_REF] Xiao | Catalytic steam gasification of biomass in fluidized bed at low temperature: conversion from livestock manure compost to hydrogen-rich syngas[END_REF][START_REF] Hervy | H 2 S removal from syngas using wastes pyrolysis chars[END_REF]. For example, Elsayed et al. [START_REF] Seredych | Desulfurization of air at high and low H 2 S concentrations[END_REF] showed that the sorption capacity of different activated carbons for the removal of H 2 S in humidified air varied in the range of 4.2-65.9 mg of H 2 S per g of sorbent.

"Foam" recovered from the walls of the reactor at the end of test was characterized by FTIR (Fig. 9) and SEM-EDX (Fig. 10). Fig. 9 compares the FTIR spectrum of the fresh APC with that of foam recovered after 7 days of test. Calcite was still found as the main component of foam. However, the peak of aragonite at 854 cm -1 was strongly reduced indicating that calcium carbonate dissolution really took place during the reaction. However, no notable signal was recorded for sulfur-based compounds by FTIR. with those of the initial APC. The initial APC contained particles and agglomerates of various particle sizes (Fig. 10(I)). Large particles of more than 50 µm were usually present in the fresh APC. These large particles were less present in the foam after test (Fig. 10(II)). In addition, particles with high contrast appeared after test (red arrows in Fig. 10(III)). EDX analysis allowed detecting the presence of sulfur for all the spots analyzed (Spots (a) and (b)). However, the concentration of sulfur was particularly important for the analyses on the particles of high contrast (Spot (c)). Imaging of sulfur was built by EDX analysis on a large zone for a global observation on the localization sulfur species (Fig. 11). This figure strongly evidences the formation of sulfur-containing compounds on the surface of the sorbent after test, and allowed explaining the abatement of H 2 S from the waste air in Fig. 8.

Reaction pathway for H 2 S abatement

We have shown that APC and NPC were active for the removal of H 2 S from the gas phase by a triphasic gas-liquid-solid process. Their performance was higher than that of the commercial calcite from Fisher Scientific. Absorption and adsorption phenomena could take place but they did not explain the plateau of the outlet concentration of H 2 S as illustrated in mixture, as suggested thereafter, in parallel with the "consumption" of calcium carbonate particles by these chemical reactions. The main steps suggested for this process are as follows:

-When the waste air passed through the suspension, the dissolution of gaseous H 2 S and O 2 took place ( 6) and ( 7)):

⇄ H S H S g a q 2 ( ) 2 ( ) (6)
⇄ O O g a q 2( ) 2( ) (7)
-When a solid sorbent was added to the reaction mixture, the dissociation/dissolution of calcium carbonate and other impurities present in the initial solid sorbent occured (Eqs. ( 8) and ( 9)), leading to the formation of soluble metallic cations in solution. Different ions such as Ca 2+ , Mg 2+ , Cl -, SO 4 2-were identified in aqueous suspension of calcium carbonate-based solids (Table 2):

⇄ + + - CaCO Ca CO s aq aq 3( ) ( ) 2 3( ) 2 (8)
⇄ + + - M A x M y A x y s aq n aq m ( ) ( ) ( ) (9)
-In the liquid phase, there was the dissociation and formation of different anions:

+ ⇄ + - + H S
-Soluble H 2 S (aq) dissociated and/or reacted with carbonate anions to form other sulfide species (Eqs. ( 10)-( 13)). The dissociation of hydrogensulfide (HS -) to form sulfide anion (S 2-) according to Eq. ( 11) must be negligible at pH around 9 (which was the pH of the suspensions prepared from the three sorbents used in this work), into account the second pK a2 of H 2 S in an aqueous solution (equal to 13 at 25 °C). Thus, the reaction between hydrogensulfide and carbonate anions must be also negligible at pH 9 (Eq. ( 13)). So, hydrogensulfide (HS -) must be the main sulfide species in the solution at this pH. The resulting soluble sulfide species ( - S aq n ( ) , equivalent to the sum of

- - H S HS S , a n d aq aq aq 2 ( ) ( ) ( )
2 ) were oxidized to higher oxidation states, according to Eq. ( 14):

+ ⇄ + + + - - - - S O
-This oxidation could be catalyzed by: 1) soluble metallic cations in solution including Ca 2+ , Mg 2+ [START_REF] Morse | The chemistry of the hydrogen sulfide and iron sulfide systems in natural waters[END_REF]; and 2) insoluble metals on the surface of the solid [START_REF] Ros | Dried sludges and sludge-based chars for H 2 S removal at low temperature: influence of sewage sludge characteristics[END_REF][START_REF] Kim | Mechanisms of hydrogen sulfide removal with steel making slag[END_REF][START_REF] Morse | The chemistry of the hydrogen sulfide and iron sulfide systems in natural waters[END_REF][START_REF] Tian | High performance of Fe nanoparticles/carbon aerogel sorbents for H 2 S removal[END_REF]. The presence of sulfite (SO ) were confirmed by analyzing the liquid fraction of the reaction mixture with ionic chromatography (Fig. 12). -Finally, the precipitation of sulfur species with metallic cations might also occur to form solid precipitates which could be metals sulfite, metals sulfate or metals thiosulfate:

+ + + + ⇄ + + - - - Ca M SO SO S O
APC was found to be more efficient than NPC under the same experimental conditions. This can be now confirmed by the higher solubility of calcium carbonate present in APC. This calcium carbonate was initially formed by an accelerated process of carbonation and thus was more easily dissolved in an aqueous solution. On the other hand, NPC was formed by the natural atmospheric carbonation process and became more difficult to dissolve. So, the suspension of APC contained more carbonate anions (CO 3

2-

) and calcium cations (Ca 2+ ), which were both useful for the dissociation of H 2 S (Eq. ( 12)) as well as the precipitation of sulfur species (Eq. ( 15)). The efficiency of the process decreased with the reaction time (Fig. 5) because calcium carbonate particles were progressively consumed. In addition, solid sulfur species were formed and could limit or prevent the contact of calcium carbonate particles with sulfide species.

According to the mechanism of H 2 S abatement in Eqs. ( 6)-( 15), the dissolved oxygen must play a very important role in this process. Dissolved oxygen reacted with soluble sulfide species ( - S aq n ( ) ) to form stable sulfite (SO ) species. This allows the continuous dissolution of gaseous H 2 S into the suspension Conditions: air flow rate of 100 mL min -1 , initial concentration of H 2 S in waste air of 200 ppmv, 100 mL of suspension, 0.2 wt% of solid using APC as reactive sorbent, room temperature and pressure.

and explains the plateau time of H 2 S outlet concentration in Fig. 2. To confirm this important role of the dissolved oxygen, two experiments were carried out under the same condition using H 2 S (50 ppmv) in the synthetic air (20%O 2 and 80% N 2 , vol.%) and pure N 2 . Fig. 13 shows the results obtained. After the first minutes of reaction wherein the efficiency of H 2 S abatement was similar to each of two gas matrices, the efficiency of H 2 S abatement in the synthetic air reached a plateau time, but this decreased progressively to zero in pure N 2 . In fact, the initial quantity of dissolved oxygen in 200 mL of water fed into the reactor was progressively consumed according to Eq. ( 14) and it was not renewed in the case of H 2 S diluted in pure N 2 . Thus, Eq. ( 14) did not further take place which explained the outlet H 2 S concentration profile in the case of H 2 S diluted in pure N 2 .

Comparison with the results reported in the literature

Carbon-based materials (i.e. activated carbon) are considered as references for H 2 S removal. Table 4 compares the performance of APC and NPC residues with those of carbon-based materials including activated carbon and biochar. Using fixed-bed or fluidized bed reactors, the capacity for H 2 S abatement of carbon-based materials is generally below 70 mg of H 2 S per g of material [START_REF] Ros | Dried sludges and sludge-based chars for H 2 S removal at low temperature: influence of sewage sludge characteristics[END_REF][START_REF] Xiao | Catalytic oxidation of hydrogen sulfide over unmodified and impregnated activated carbon[END_REF][START_REF] Sun | An enhanced approach for biochar preparation using fluidized bed and its application for H 2 S removal[END_REF][START_REF] Krischan | Design and scale-up of an oxidative scrubbing process for the selective removal of hydrogen sulfide from biogas[END_REF], in dry or humidified gas. The residues used in this showed the comparable reactivity of at least 75 mg of H 2 S per g of material.

Caustic scrubbing in the aqueous solution using reactants like NaOH, NaClO, NaHCO 3 is an efficient technology for the removal of H 2 S from the gas phase and has the similar operation mode compared to the reactor design of the present work. As a function of the inlet concentration of H 2 S, the feeding of caustic reactants, and the gas flow rate, the abatement of H 2 S can reach nearly 100% [START_REF] Krischan | Design and scale-up of an oxidative scrubbing process for the selective removal of hydrogen sulfide from biogas[END_REF][START_REF] Biard | Wet scrubbing intensification applied to hydrogen sulphide removal in waste water treatment plant[END_REF]. However, the cost of these caustic reactants is largely higher (5-10 times) than that of the residues used in this work [START_REF] Galera-Martinez | Valorisation des residus carbonates industriels pour le traitement de sulfure d'hydrogene dans les effluents gazeux[END_REF]. This demonstrates the interest of APC and NPC as the potential materials for H 2 S removal from the gas phase using the triphasic G/L/S process.

Conclusions

For the first time, a triphasic gas/liquid/solid process was designed for the abatement of H 2 S from the gas phase using calcium carbonatecontaining residues from industrial activities as reactive sorbents. Solid wastes containing high calcium carbonate contents under powder form could directly be used as sorbent for H 2 S abatement after a simple drying at room temperature. At room temperature and ambient pressure, this process was found to be very efficient for the abatement of H 2 S. The dissolution and dissociation of H 2 S from the gas phase to the liquid phase was of crucial importance, which allowed increasing the contact time of sulfur species with dissolved oxygen for further oxidation into stable sulfite (SO ) species. The sorption capacity of APC sorbent could reach at least 75 mg of H 2 S per gram of sorbent which is very competitive compared to that of the conventional sorbents, i.e. activated carbon.

The next step of this study would be focused on the trials at large industrial pilot scale with a real waste air from a wastewater treatment plant polluted by H 2 S.

Fig. 2 .Fig. 3 .

 23 Fig. 2. Example of profile of H 2 S concentration at the outlet of reactor. Conditions: gas flow rate of 100 mL min -1 , inlet concentration of H 2 S of 200 ppmv, 100 mL of suspension, 5 wt% of solid using APC as reactive sorbent, room temperature and pressure.

Fig. 4 .Fig. 5 .

 45 Fig. 4. FTIR spectra of APC, NPC and pure commercial calcite.

Fig. 6 .

 6 Fig. 6. (a) Efficiency of H 2 S removal at different solid loading. Conditions: Gas flow rate of 100 mL min -1 , inlet concentration of H 2 S of 200 ppmv, suspension volume of 100 mL, stirring speed of 600 rpm, room temperature and pressure. (b) Efficiency of H 2 S removal as a function of suspension volume of APC. Gas flow rate of 100 mL min -1 , inlet concentration of H 2 S of 200 ppmv, stirring speed of 600 rpm, room temperature and pressure; reaction time of at least 8 h for each test.

Fig. 10 comparesFig. 7 .

 107 Fig. 7. Influence of the inlet concentration of H 2 S. Conditions: Gas flow rate of 100 mL min -1 , solid loading of 0.2 wt%, suspension volume of 100 mL, stirring speed of 600 rpm, room temperature and pressure; (a) rate of H 2 S removal (mmol min -1 ); (b) Efficiency of H 2 S removal (%); reaction time of at least 8 h for each test.

Fig. 8 .Fig. 9 .

 89 Fig. 8. (a) of H 2 S removal during 7 days of test with APC. Gas flow rate of 100 min -1 , inlet concentration of H 2 S of 200 ppmv, solid content of 0.2 wt%, suspension volume of 100 mL, stirring speed of 600 rpm, room temperature and pressure; (b) and (c) and (d): Photos of the reactor wall after one, three and seven days of test, respectively.

  Fig. Chemical reactions must occur inside the reaction

Fig. 10 .

 10 Fig. 10. SEM-EDX analysis of the initial APC (I) and of the foam recovered after 7 days of test (II-III).

Fig. 11 .Fig. 12 .

 1112 Fig. 11. SEM image (left-hand-side) and imaging of sulfur (right-hand-side, blue color) of the foam recovered after 7 days of test. Images recorded at the same scale.

Fig. 13 .

 13 Fig.[START_REF] Liu | Experimental studies on mineral sequestration of CO 2 with buffer solution and fly ash in brines[END_REF]. Role of oxygen in the H 2 S abatement under the similar experimental condition by using two gas matrices. Conditions: 100 mL de suspension of APC at 0.2 wt%; 600 rpm ; gas flow rate of 100 mL/min ; 50 ppmv d'H 2 S in N 2 or air.

Table 1

 1 Chemical composition of APC and NPC obtained by ICP-AES and TG analyses.

	Solid	Concentration (g kg -1 )
		Ca	CO 3 2-	S	Mg	Na	Fe
	APC	357.4	532.0	7.2	2.4	9.9	1.6
	NPC	384.2	565.0	1.1	1.3	3.6	3.9

Table 2

 2 Analysis of the major species present in the filtrates of 10 wt% aqueous suspensions of APC and NPC.

	Solid	Concentration (mg kg -1 )
		Ca	Mg	Na	Cl	S
	APC	809.2	74.6	482.7	1830.0	286.4
	NPC	29.8	5.3	38.2	40.0	30.1

Table 3

 3 Specific

	Solid	NPC		APC		Commercial calcite
	S BET (m 2 g -1 )	Before	After	Before	After	Before	After
		3	4	2	5	2	2

surface areas of the raw solids (before) and the solids after dispersing in an aqueous suspension (after).

Table 4

 4 Example of results on H 2 S removal using carbon-based materials.

	Sorbent	Type of	Medium	Q (mg H2S /	Ref.
		reactor		g sorbent )
	Activated carbon	Fixed-bed	H 2 S in dry N 2	9	[27]
	Char from black	Fluidized	H 2 S in humidified	25-70	[28]
	liquor	bed	N 2
	carbonization
	Activated carbon	Fixed-bed	H 2 S in dry air	5-31	[23]
	Char from sludge	Fixed-bed	H 2 S in humidified	6-62	[2]
	pyrolysis		air
	APC and NPC	Triphasic	H 2 S in dry air	> 75	This
		G/L/S	scrubbed in		work
			suspension of
			CaCO 3 -based
			particles

Acknowledgments

The authors gratefully acknowledge the colleagues at RAPSODEE Research Center (UMR CNRS 5302, France) for their technical help.