Handling global conditions in parameterized system verification, Proceedings of the 11th International Conference on Computer Aided Verification, pp.134-145, 1999. ,
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 rewriting approach to satisfiability procedures, Information and Computation, vol.183, issue.2, pp.140-164, 2003. ,
DOI : 10.1016/S0890-5401(03)00020-8
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
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
Term Rewriting and All That, 1998. ,
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
Fusions of description logics and abstract description systems, Journal of Artificial Intelligence Research, vol.16, pp.1-58, 2002. ,
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
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
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
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
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
A unified approach to theory reasoning, 1992. ,
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
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
Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th Conference on Design Automation, pp.317-320, 1999. ,
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
Integrating Decision Procedures for Temporal Verification, 1998. ,
Modal Logic, 2002. ,
DOI : 10.1017/CBO9781107050884
URL : https://hal.archives-ouvertes.fr/inria-00100503
Berkeley Lazy Abstraction Software Verification Tool ,
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
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
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
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
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
Radu Iosif, Pierre Moro, and Tomás Vojnar. Programs with lists are counter automata ,
A Computational Logic Handbook, 1997. ,
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
Safety Analysis of Systems, 2007. ,
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
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
9 First-order modal logic, Handbook of Modal Logic, pp.549-620, 2007. ,
DOI : 10.1016/S1570-2464(07)80012-7
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
A semantics for concurrent separation logic, Proceedings of the 15th International Conference on Concurrency Theory, pp.16-34, 2004. ,
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
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
Verification of infinite state structures, Handbook of Process Algebras, pp.545-623, 2001. ,
Modal Logic, 1997. ,
Model Theory. North-Holland, 1990. ,
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
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
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
Model checking and abstraction, ACM Transactions on Programming Languages and Systems, vol.16, issue.5, pp.1512-1542, 1994. ,
DOI : 10.1145/186025.186051
Orna Grumberg, and Doron A. Peled. Model Checking, 1999. ,
Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, pp.154-169, 2000. ,
DOI : 10.1007/10722167_15
Abstraction Refinement for Termination, Proceedings of the 12th International Symposium on Static Analysis, pp.87-101, 2005. ,
DOI : 10.1007/11547662_8
The Coq proof assistant Reference manual, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00069919
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
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
Lazy theorem proving for bounded model checking over infinite domains, Proceedings of the 18th International Conference on Automated Deduction, pp.438-455, 2002. ,
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
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
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
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
Assignment commands with array references, Journal of the ACM, vol.25, issue.4, pp.652-666, 1978. ,
Mathematical logic. Undergraduate Texts in Mathematics, 1994. ,
A Mathematical Introduction to Logic, 1972. ,
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
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
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
Extended static checking for Java, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.234-245, 2002. ,
Many- Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic and the Foundations of Mathematics, 2003. ,
Logic for Computer Science: Foundations of Automatic Theorem Proving, 1986. ,
Shostak Light, Proceedings of the 18th International Conference on Automated Deduction, pp.332-346, 2002. ,
DOI : 10.1007/3-540-45620-1_28
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
Reasoning about systems with many processes, Journal of the ACM, vol.39, issue.3, pp.675-735, 1992. ,
Reasoners' cooperation and quantifiers elimination, 2003. ,
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
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
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
A Comprehensive Framework for Combined Decision Procedures, ACM Transactions on Computational Logic, 2006. ,
DOI : 10.1007/11559306_1
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
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
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
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
Open Graph Transformation Systems: A New Approach to the Compositional Modelling of Concurrent and Reactive Systems, 1998. ,
Lazy abstraction, Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.58-70, 2002. ,
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
Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.232-244, 2004. ,
Model Theory. Number 42 in Encyclopedia of Mathematics and its Applications, 1993. ,
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
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
Finding bugs with a constraint solver, Proceedings of the International Symposium on Software Testing and Analysis, pp.14-25, 2000. ,
Presburger arithmetic with array segments, Information Processing Letters, vol.12, issue.2, pp.79-82, 1981. ,
DOI : 10.1016/0020-0190(81)90007-7
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
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
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
On Fourier's algorithm for linear arithmetic constraints, Journal of Automated Reasoning, vol.38, issue.3, pp.373-379, 1992. ,
DOI : 10.1007/BFb0121242
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
Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, vol.55, issue.1, 1995. ,
DOI : 10.1007/BF01384313
Model checking, Abstraction and Compositional Verification, 1993. ,
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
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
Temporal Verification of Reactive Systems: Safety, 1995. ,
DOI : 10.1007/978-1-4612-4222-2
STeP: The Stanford Temporal Prover, 1994. ,
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
Decidability and Complexity of Model Checking Problems for Infinite- State Systems, 1998. ,
Towards a mathematical theory of computation, Proceedings of IFIP Congress, pp.21-28, 1962. ,
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. ,
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. ,
Symbolic model checking: An approach to the state explosion problem, 1992. ,
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
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
On the logic of TLA, Computing and Informatics, vol.22, pp.351-379, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00099800
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. ,
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
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
Combined decision procedures for constraint satisfiability, 2007. ,
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
Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006. ,
DOI : 10.1145/1217856.1217859
Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2002. ,
Resources, concurrency, and local reasoning, Theoretical Computer Science, vol.375, issue.1-3, pp.271-307, 2007. ,
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
Verification of concurrent systems: function and timing, 1981. ,
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 decision procedure for combination of propositional temporal logic and other specialized theories, Journal of Automated Reasoning, vol.2, issue.2, pp.171-190, 1986. ,
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
Decidability of second-order theories and automata on infinite trees. Transactions of the, pp.1-35, 1969. ,
Satisfiability modulo theories, IEEE Magazine on Intelligent Systems, vol.21, issue.6, pp.71-81, 2006. ,
Separation logic: A logic for shared mutable data structures, Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp.55-74, 2002. ,
Reasoning about arrays, Communications of the ACM, vol.22, issue.5, pp.290-299, 1979. ,
Démonstration Automatique (Techniques de réécriture). InterEditions, 1989. ,
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
Theory of Linear and Integer Programming, 1986. ,
Deductive model checking. Formal Methods in System Design, pp.49-74, 1999. ,
The complexity of propositional linear temporal logics, Journal of the ACM, vol.32, issue.3, pp.733-749, 1985. ,
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 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
Verification Decidability of Presburger Array Programs, Journal of the ACM, vol.27, issue.1, pp.191-205, 1980. ,
DOI : 10.1145/322169.322185
Cooperation of background reasoners in theory reasoning by residue sharing, Journal of Automated Reasoning, vol.3, issue.1, pp.1-31, 2003. ,
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
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
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
Logic and Structure, 1989. ,
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
An automata-theoretic approach to automatic program verification, Proceedings of Symposium on Logic in Computer Science (LICS 1986), pp.332-344, 1986. ,
Model-companions and definability in existentially complete structures, Israel Journal of Mathematics, vol.25, pp.305-330, 1976. ,
Fusions of modal logics revisited, Advances in Modal Logic. CSLI, 1998. ,