A. Parosh, A. Abdulla, B. Bouajjani, M. Jonsson, and . Nilsson, Handling global conditions in parameterized system verification, Proceedings of the 11th International Conference on Computer Aided Verification, pp.134-145, 1999.

P. Aziz-abdulla, K. Cerans, B. Jonsson, and Y. Tsay, General decidability theorems for infinite-state systems, Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp.313-321, 1996.
DOI : 10.1109/LICS.1996.561359

A. Armando, S. Ranise, and M. Rusinowitch, A rewriting approach to satisfiability procedures, Information and Computation, vol.183, issue.2, pp.140-164, 2003.
DOI : 10.1016/S0890-5401(03)00020-8

A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz, New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic, vol.10, issue.1, 2007.
DOI : 10.1145/1459010.1459014

URL : https://hal.archives-ouvertes.fr/inria-00576862

F. Baader and S. Ghilardi, Connecting many-sorted theories, Journal of Symbolic Logic, 2006.
DOI : 10.1007/11532231_21

URL : http://lat.inf.tu-dresden.de/research/papers/2007/BaaGi-JSL-07.pdf

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

F. Baader and C. Tinelli, Deciding the Word Problem in the Union of Equational Theories, Information and Computation, vol.178, issue.2, pp.346-390, 2002.
DOI : 10.1006/inco.2001.3118

F. Baader, C. Lutz, H. Sturm, and F. Wolter, Fusions of description logics and abstract description systems, Journal of Artificial Intelligence Research, vol.16, pp.1-58, 2002.

F. Baader, S. Ghilardi, and C. Tinelli, A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Information and Computation, vol.204, issue.10, pp.1413-1452, 2006.
DOI : 10.1016/j.ic.2005.05.009

L. Bachmair and H. Ganzinger, On restrictions of ordered paramodulation with simplification, Proceedings of 10th International Conference on Automated Deduction, pp.427-441, 1990.
DOI : 10.1007/3-540-52885-7_105

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994.
DOI : 10.1093/logcom/4.3.217

T. Ball and S. K. Rajamani, The SLAM Toolkit, Proceedings of the 13th International Conference on Computer Aided Verification, pp.260-264, 2001.
DOI : 10.1007/3-540-44585-4_25

C. W. Barrett, D. L. Dill, and A. Stump, A Generalization of Shostak#x2019;s Method for Combining Decision Procedures, Proceedings of the 4th International Workshop on Frontiers of Combining Systems, pp.132-147, 2002.
DOI : 10.1007/3-540-45988-X_11

P. Baumgartner, U. Furbach, and U. Petermann, A unified approach to theory reasoning, 1992.

S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis, Property preserving simulations, Proceedings of the 4th International Workshop on Computer Aided Verification, pp.260-273, 1992.
DOI : 10.1007/3-540-56496-9_21

O. Bernholtz, M. Y. Vardi, and P. Wolper, An automata-theoretic approach to branching-time model checking (Extended abstract), Proceedings of 6th International Conference on Computer Aided Verification, pp.142-155, 1994.
DOI : 10.1007/3-540-58179-0_50

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th Conference on Design Automation, pp.317-320, 1999.

N. Bjørner, M. E. Stickel, and T. E. Uribe, A practical integration of first-order reasoning and decision procedures, Proceedings of the 14th International Conference on Automated Deduction, pp.101-115, 1997.
DOI : 10.1007/3-540-63104-6_13

S. Nikolaj and . Bjørner, Integrating Decision Procedures for Temporal Verification, 1998.

P. Blackburn, Y. Maarten-de-rijke, and . Venema, Modal Logic, 2002.
DOI : 10.1017/CBO9781107050884

URL : https://hal.archives-ouvertes.fr/inria-00100503

B. Blast, Berkeley Lazy Abstraction Software Verification Tool

M. P. Bonacina, S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures, Proceedings of the 3rd International Joint Conference on Automated Reasoning, pp.513-527, 2006.
DOI : 10.1007/11814771_42

A. Bouajjani, J. Esparza, and O. Maler, Reachability analysis of pushdown automata: Application to model-checking, Proceedings of the 8th International Conference on Concurrency Theory, pp.135-150, 1997.
DOI : 10.1007/3-540-63141-0_10

A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili, Regular Model Checking, Proceedings of the 12th International Conference on Computer Aided Verification, pp.403-418, 2000.
DOI : 10.1007/10722167_31

URL : https://hal.archives-ouvertes.fr/hal-00161119

A. Bouajjani, P. Habermehl, and T. Vojnar, Abstract Regular Model Checking, Proceedings of the 16th International Conference on Computer Aided Verification, pp.372-386, 2004.
DOI : 10.1007/978-3-540-27813-9_29

URL : https://hal.archives-ouvertes.fr/hal-00159512

A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar, Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.13-29, 2005.
DOI : 10.1007/978-3-540-31980-1_2

URL : https://hal.archives-ouvertes.fr/hal-00147978

A. Bouajjani, M. Bozga, and P. Habermehl, Radu Iosif, Pierre Moro, and Tomás Vojnar. Programs with lists are counter automata

S. Robert, J. Boyer, and . Strother-moore, A Computational Logic Handbook, 1997.

M. Bozzano, R. Bruttomesso, A. Cimatti, T. A. Junttila, S. Ranise et al., Efficient theory combination via boolean search, Information and Computation, vol.204, issue.10, pp.1493-1525, 2006.
DOI : 10.1016/j.ic.2005.05.011

URL : https://doi.org/10.1016/j.ic.2005.05.011

A. R. Bradley, Safety Analysis of Systems, 2007.

A. R. Bradley, Z. Manna, and H. B. Sipma, Termination of Polynomial Programs, Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, pp.113-129, 2005.
DOI : 10.1007/978-3-540-30579-8_8

A. R. Bradley, Z. Manna, and H. B. Sipma, What???s Decidable About Arrays?, Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, pp.427-442, 2006.
DOI : 10.1007/11609773_28

URL : http://theory.stanford.edu/~sipma/papers/avmcai06.pdf

T. Bräuner and S. Ghilardi, 9 First-order modal logic, Handbook of Modal Logic, pp.549-620, 2007.
DOI : 10.1016/S1570-2464(07)80012-7

A. Brodnik, S. Carlsson, E. D. Demaine, J. I. Munro, and R. Sedgewick, Resizable Arrays in Optimal Time and Space, Proceedings of the 6th International Workshop on Algorithms and Data Structures, pp.37-48, 1999.
DOI : 10.1007/3-540-48447-7_4

URL : http://algonquin.uwaterloo.ca/~imunro/resize.ps

D. Stephen and . Brookes, A semantics for concurrent separation logic, Proceedings of the 15th International Conference on Concurrency Theory, pp.16-34, 2004.

R. E. Bryant, S. K. Lahiri, and S. A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, pp.78-92, 2002.
DOI : 10.1007/3-540-45657-0_7

R. J. Büchi, On a Decision Method in Restricted Second Order Arithmetic, Proceedings of the International Congress on Logic, Math, and Philosophy of Science, 1962.
DOI : 10.1007/978-1-4613-8928-6_23

O. Burkart, D. Caucal, F. Moller, and B. Steffen, Verification of infinite state structures, Handbook of Process Algebras, pp.545-623, 2001.

A. Chagrov and M. Zakharyaschev, Modal Logic, 1997.

C. Cheng, J. H. Chang, and . Keisler, Model Theory. North-Holland, 1990.

A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, pp.359-364, 2002.
DOI : 10.1007/3-540-45657-0_29

E. M. Clarke, A. E. Emerson, and P. A. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-263, 1986.
DOI : 10.1145/5397.5399

E. M. Clarke, T. Filkorn, and S. Jha, Exploiting symmetry in temporal logic model checking, Proceedings of the 5th International Conference on Computer Aided Verification (CAV 1993) Elounda (Greece), pp.450-462, 1993.
DOI : 10.1007/3-540-56922-7_37

E. M. Clarke, O. Grumberg, and D. E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1512-1542, 1994.
DOI : 10.1145/186025.186051

E. M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking, 1999.

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, pp.154-169, 2000.
DOI : 10.1007/10722167_15

B. Cook, A. Podelski, and A. Rybalchenko, Abstraction Refinement for Termination, Proceedings of the 12th International Symposium on Static Analysis, pp.87-101, 2005.
DOI : 10.1007/11547662_8

. Coq, The Coq proof assistant Reference manual, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00069919

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/hal-01108790

D. Cyrluk and P. Narendran, Ground temporal logic: A logic for hardware verification, Proceedings of the 6th International Conference on Computer Aided Verification, pp.247-259, 1994.
DOI : 10.1007/3-540-58179-0_59

M. Leonardo, H. De-moura, M. Rueß, and . Sorea, Lazy theorem proving for bounded model checking over infinite domains, Proceedings of the 18th International Conference on Automated Deduction, pp.438-455, 2002.

A. Degtyarev, M. Fisher, and B. Konev, Monodic temporal resolution, ACM Transactions on Computational Logic, vol.7, issue.1, pp.108-150, 2006.
DOI : 10.1145/1119439.1119443

URL : http://arxiv.org/pdf/cs/0306041

G. Delzanno, J. Esparza, and A. Podelski, Constraint-Based Analysis of Broadcast Protocols, Proceedings of the 13th International Workshop on Computer Science Logic, pp.50-66, 1999.
DOI : 10.1007/3-540-48168-0_5

S. Demri, Linear-time temporal logics with Presburger constraints: an overview ???, Journal of Applied Non-Classical Logics, vol.118, issue.133, pp.3-4311, 2006.
DOI : 10.1006/inco.2000.2894

S. Demri, A. Finkel, V. Goranko, and G. Van-drimmelen, Towards a Model-Checker for Counter Systems, Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, pp.493-507, 2006.
DOI : 10.1007/11901914_36

J. Peter, R. Downey, and . Sethi, Assignment commands with array references, Journal of the ACM, vol.25, issue.4, pp.652-666, 1978.

H. Ebbinghaus, J. Flum, and W. Thomas, Mathematical logic. Undergraduate Texts in Mathematics, 1994.

B. Herbert and . Enderton, A Mathematical Introduction to Logic, 1972.

J. Esparza and S. Schwoon, A BDD-Based Model Checker for Recursive Programs, Proceedings of the 13th International Conference on Computer Aided Verification, pp.324-336, 2001.
DOI : 10.1007/3-540-44585-4_30

J. Esparza, A. Finkel, and R. Mayr, On the verification of broadcast protocols, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.352-359, 1999.
DOI : 10.1109/LICS.1999.782630

M. Finger and D. M. Gabbay, Adding a temporal dimension to a logic system, Journal of Logic, Language and Information, vol.17, issue.4, pp.203-233, 1992.
DOI : 10.1007/978-94-009-6259-0_3

R. Saxe and . Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.234-245, 2002.

D. M. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev, Many- Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic and the Foundations of Mathematics, 2003.

H. Jean and . Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, 1986.

H. Ganzinger and . Shostak-light, Shostak Light, Proceedings of the 18th International Conference on Automated Deduction, pp.332-346, 2002.
DOI : 10.1007/3-540-45620-1_28

H. Ganzinger and K. Korovin, Integrating Equational Reasoning into Instantiation-Based Theorem Proving, Proceedings of the 18th International Workshop on Computer Science Logic, pp.71-84, 2004.
DOI : 10.1007/978-3-540-30124-0_9

M. Steven, A. P. German, and . Sistla, Reasoning about systems with many processes, Journal of the ACM, vol.39, issue.3, pp.675-735, 1992.

S. Ghilardi, Reasoners' cooperation and quantifiers elimination, 2003.

S. Ghilardi, Model-Theoretic Methods in Combined Constraint Satisfiability, Journal of Automated Reasoning, vol.5, issue.1?2, pp.221-249, 2004.
DOI : 10.1007/s10817-004-6241-5

S. Ghilardi and L. Santocanale, Algebraic and Model Theoretic Techniques for Fusion Decidability in Modal Logics, Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp.152-166, 2003.
DOI : 10.1007/978-3-540-39813-4_10

URL : https://hal.archives-ouvertes.fr/hal-01281233

S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies, Proceedings of the 10th European Conference on Logic in Artificial Intelligence, pp.177-189, 2006.
DOI : 10.1007/11853886_16

S. Ghilardi, E. Nicolini, and D. Zucchelli, A Comprehensive Framework for Combined Decision Procedures, ACM Transactions on Computational Logic, 2006.
DOI : 10.1007/11559306_1

S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Decision procedures for extensions of the theory of arrays, Annals of Mathematics and Artificial Intelligence, vol.27, issue.1, pp.3-4231, 2007.
DOI : 10.1007/s10472-007-9078-x

URL : https://hal.archives-ouvertes.fr/inria-00576588

S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems, Proceedings of the 21st Conference on Automated Deduction, pp.362-378, 2007.
DOI : 10.1007/978-3-540-73595-3_25

URL : https://hal.archives-ouvertes.fr/inria-00576597

S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Noetherianity and Combination Problems, Proceedings of the 6th International Workshop on Frontiers of Combining Systems, pp.206-220, 2007.
DOI : 10.1007/978-3-540-74621-8_14

URL : https://hal.archives-ouvertes.fr/inria-00576594

S. Graf and H. Sa¨?disa¨?di, Construction of abstract state graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

R. Heckel, Open Graph Transformation Systems: A New Approach to the Compositional Modelling of Concurrent and Reactive Systems, 1998.

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Lazy abstraction, Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.58-70, 2002.

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Software Verification with BLAST, Proceedings of the 10th International SPIN Workshop on Model Checking Software, pp.235-239, 2003.
DOI : 10.1007/3-540-44829-2_17

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. Mcmillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.232-244, 2004.

W. Hodges, Model Theory. Number 42 in Encyclopedia of Mathematics and its Applications, 1993.

I. M. Hodkinson, F. Wolter, and M. Zakharyaschev, Decidable fragments of first-order temporal logics, Annals of Pure and Applied Logic, vol.106, issue.1-3, pp.1-385, 2000.
DOI : 10.1016/S0168-0072(00)00018-X

C. Norris, D. L. Ip, L. J. Dill-agnew, R. Claesen, and . Camposano, Better verification through symmetry, Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications (CHDL 1993), volume A-32 of IFIP Transactions, pp.97-111, 1993.
DOI : 10.1007/BF00625968

D. Jackson and M. Vaziri, Finding bugs with a constraint solver, Proceedings of the International Symposium on Software Testing and Analysis, pp.14-25, 2000.

J. Jaffar, Presburger arithmetic with array segments, Information Processing Letters, vol.12, issue.2, pp.79-82, 1981.
DOI : 10.1016/0020-0190(81)90007-7

S. Katz and D. A. Peled, An efficient verification method for parallel and distributed programs, Proceedings of the Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, pp.489-507, 1988.
DOI : 10.1007/BFb0013032

S. Héì-ene-kirchner, C. Ranise, D. Ringeissen, and . Tran, On Superposition-Based Satisfiability Procedures and Their Combination, Proceedings of the 2nd International Colloquium on Theoretical Aspects of Computing, pp.594-608, 2005.
DOI : 10.1007/11560647_39

L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

J. Lassez and M. J. Maher, On Fourier's algorithm for linear arithmetic constraints, Journal of Automated Reasoning, vol.38, issue.3, pp.373-379, 1992.
DOI : 10.1007/BFb0121242

J. Lassez and K. Mcaloon, A canonical form for generalized linear constraints, Journal of Symbolic Computation, vol.13, issue.1, pp.1-24, 1992.
DOI : 10.1016/0747-7171(92)90002-L

C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem, Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, vol.55, issue.1, 1995.
DOI : 10.1007/BF01384313

E. David and . Long, Model checking, Abstraction and Compositional Verification, 1993.

M. Maidl, A Unifying Model Checking Approach for Safety Properties of Parameterized Systems, Proceedings of the 13th International Conference on Computer Aided Verification, pp.311-323, 2001.
DOI : 10.1007/3-540-44585-4_29

M. Makkai and G. E. Reyes, First Order Categorical Logic: Model- Theoretical Methods in the Theory of Topoi and Related Categories, Number 611 in Lecture Notes in Mathematics, 1977.
DOI : 10.1007/BFb0066201

Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety, 1995.
DOI : 10.1007/978-1-4612-4222-2

Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E. Chang et al., STeP: The Stanford Temporal Prover, 1994.

P. Mateti, A Decision Procedure for the Correctness of a Class of Programs, Journal of the ACM, vol.28, issue.2, pp.215-232, 1981.
DOI : 10.1145/322248.322250

R. Mayr, Decidability and Complexity of Model Checking Problems for Infinite- State Systems, 1998.

J. Mccarthy, Towards a mathematical theory of computation, Proceedings of IFIP Congress, pp.21-28, 1962.

L. Kenneth and . Mcmillan, Applications of Craig interpolants in model checking, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), pp.1-12, 2005.

L. Kenneth and . Mcmillan, Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits, Proceedings of the 4th International Workshop on Computer Aided Verification, pp.164-177, 1992.

L. Kenneth and . Mcmillan, Symbolic model checking: An approach to the state explosion problem, 1992.

S. Mcpeak and G. C. Necula, Data Structure Specifications via Local Equality Axioms, Proceedings of the 17th International Conference on Computer Aided Verification (CAV 2005), pp.476-490, 2005.
DOI : 10.1007/11513988_47

S. Merz, Model Checking: A Tutorial Overview, 4th Summer School on Modeling and Verification of Parallel Processes, pp.3-38, 2000.
DOI : 10.1007/3-540-45510-8_1

S. Merz, On the logic of TLA, Computing and Informatics, vol.22, pp.351-379, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099800

L. Marvin and . Minsky, Recursive unsolvability of Post's problem of " tag " and other topics in the theory of Turing machines, Annals of Mathematics, vol.74, issue.3, pp.437-455, 1961.

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079

URL : http://www.cse.iitb.ac.in/~sangramraje/references/4-NelsonOppen.pdf

G. Nelson and D. C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980.
DOI : 10.1145/322186.322198

URL : http://www.cs.virginia.edu/~weimer/2006-655/reading/nelson-oppen-congruence.pdf

E. Nicolini, Combined decision procedures for constraint satisfiability, 2007.

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Handbook of Automated Reasoning, volume I, chapter 7, pp.371-443, 2001.
DOI : 10.1016/B978-044450813-3/50009-6

URL : http://www-lsi.upc.es/~albert/papers/handbook.ps.gz

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2002.

W. O. Peter and . Hearn, Resources, concurrency, and local reasoning, Theoretical Computer Science, vol.375, issue.1-3, pp.271-307, 2007.

D. C. Oppen, Complexity, convexity and combinations of theories, Theoretical Computer Science, vol.12, issue.3, pp.291-302, 1980.
DOI : 10.1016/0304-3975(80)90059-6

T. William and . Overman, Verification of concurrent systems: function and timing, 1981.

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, Proceedings of the 11th International Conference on Automated Deduction, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

A. David and . Plaisted, A decision procedure for combination of propositional temporal logic and other specialized theories, Journal of Automated Reasoning, vol.2, issue.2, pp.171-190, 1986.

A. Pnueli, S. Ruath, and L. D. Zuck, Automatic Deductive Verification with Invisible Invariants, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.82-97, 2001.
DOI : 10.1007/3-540-45319-9_7

URL : https://link.springer.com/content/pdf/10.1007%2F3-540-45319-9_7.pdf

O. Michael and . Rabin, Decidability of second-order theories and automata on infinite trees. Transactions of the, pp.1-35, 1969.

S. Ranise and C. Tinelli, Satisfiability modulo theories, IEEE Magazine on Intelligent Systems, vol.21, issue.6, pp.71-81, 2006.

C. John and . Reynolds, Separation logic: A logic for shared mutable data structures, Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp.55-74, 2002.

C. John and . Reynolds, Reasoning about arrays, Communications of the ACM, vol.22, issue.5, pp.290-299, 1979.

M. Rusinowitch, Démonstration Automatique (Techniques de réécriture). InterEditions, 1989.

H. Sa¨?disa¨?di and N. Shankar, Abstract and Model Check while You Prove, Proceedings of the 11th International Conference on Computer Aided Verification, pp.443-454, 1999.
DOI : 10.1007/3-540-48683-6_38

A. Schrijver, Theory of Linear and Integer Programming, 1986.

B. Henny, T. E. Sipma, Z. Uribe, and . Manna, Deductive model checking. Formal Methods in System Design, pp.49-74, 1999.

A. , P. Sistla, and E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM, vol.32, issue.3, pp.733-749, 1985.

V. Sofronie-stokkermans, Interpolation in Local Theory Extensions, Proceedings of the 3rd International Joint Conference on Automated Reasoning, pp.235-250, 2006.
DOI : 10.1007/11814771_21

A. Stump, C. W. Barrett, D. L. Dill, and J. R. Levitt, A decision procedure for an extensional theory of arrays, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.29-37, 2001.
DOI : 10.1109/LICS.2001.932480

N. Suzuki and D. R. Jefferson, Verification Decidability of Presburger Array Programs, Journal of the ACM, vol.27, issue.1, pp.191-205, 1980.
DOI : 10.1145/322169.322185

C. Tinelli, Cooperation of background reasoners in theory reasoning by residue sharing, Journal of Automated Reasoning, vol.3, issue.1, pp.1-31, 2003.

C. Tinelli and M. T. Harandi, A New Correctness Proof of the Nelson-Oppen Combination Procedure, Proceedings of the 1st International Workshop on Frontiers of Combining Systems Applied Logic, pp.103-120, 1996.
DOI : 10.1007/978-94-009-0349-4_5

C. Tinelli and C. G. Zarba, Combining Non-Stably Infinite Theories, Electronic Notes in Theoretical Computer Science, vol.86, issue.1, pp.209-238, 2005.
DOI : 10.1016/S1571-0661(04)80651-0

A. Tiwari, Termination of Linear Programs, Proceedings of the 16th International Conference on Computer Aided Verification, pp.70-82, 2004.
DOI : 10.1007/978-3-540-27813-9_6

D. Van-dalen, Logic and Structure, 1989.

M. Y. Vardi, Verification of concurrent programs: the automata-theoretic framework*, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.79-98, 1991.
DOI : 10.1016/0168-0072(91)90066-U

Y. Moshe, P. Vardi, and . Wolper, An automata-theoretic approach to automatic program verification, Proceedings of Symposium on Logic in Computer Science (LICS 1986), pp.332-344, 1986.

H. William and . Wheeler, Model-companions and definability in existentially complete structures, Israel Journal of Mathematics, vol.25, pp.305-330, 1976.

F. Wolter, Fusions of modal logics revisited, Advances in Modal Logic. CSLI, 1998.