Publications GECCOO 2003-2006

[1] Alessandro A, S. Ranise, and Michaël Rusinowitch. A rewriting approach to satisfiability procedures. Information and Computation, 183(2):140-164, 2003. [ bib ]
[2] A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures (extended abstract). In Notes of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), co-located with CAV'05, Edinburgh, Scotland (UK), 2005. [ bib ]
[3] A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In B. Gramlich, editor, Proc. of the 5th Int. Workshop on Frontiers of Combining Systems (FroCoS'2005), volume 3717 of Lecture Notes in Computer Science, pages 65-80, Vienna, Austria, September 2005. Springer. [ bib ]
[4] A. Armando, L. Compagna, and S. Ranise. Rewriting and decision procedure laboratory: Combining rewriting, satisfiability checking, and lemma speculation. In Dieter Hutter and Werner Stephan, editors, Mechanizing Mathematical Reasoning. Essays in Honor of J. H. Siekmann on the Occasion of his 60th Birthday, volume 2605 of LNAI, pages 30-45. Springer-Verlag, 2005. [ bib ]
[5] Nicolas Ayache. Coopération d'outils de preuve interactifs et automatiques. Master's thesis, Université Paris 7, 2005. [ bib ]
[6] G. Barthe, L. Burdy, J. Charles, B. Grégoire, M. Huisman, J.-L. Lanet, M. Pavlova, and A. Requet. JACK: a tool for validation of security and behaviour of java applications, 2006. Abstract for tutorial, longer version to appear. [ bib ]
[7] G. Barthe, M. Pavlova, and G. Schneider. Precise analysis of memory consumption using program logics. In B. Aichernig and B. Beckert, editors, Proceedings of SEFM'05. IEEE Press, 2005. [ bib ]
[8] Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. Secure Information Flow by Self-Composition. In R. Foccardi, editor, 17th IEEE Computer Security Foundations Workshop (CSFW'04), pages 100-114, Los Alamitos, CA, USA, June 2004. IEEE Computer Society. [ bib ]
[9] F. Bellegarde, C. Charlet, and O. Kouchnarenko. How to compute the refinement relation for parameterized systems. In R. Gupta, Le Guenic P., and Talpin J.P., editors, Formal Methods and Models for System Design, chapter 2. Springer-Verlag, 2004. [ bib ]
[10] F. Bellegarde, J. Groslambert, M. Huisman, O. Kouchnarenko, and J. Julliand. Verification of liveness properties with JML. Technical report, INRIA, 2004. [ bib ]
[11] D. Bert, M-L. Potet, and N. Stouls. GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties. In H. Treharne, S. King, M. C. Henson, and S. A. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users, volume 3455 of LNCS, pages 299-318. Springer-Verlag, 2005. [ bib ]
[12] Didier Bert, Marie-Laure Potet, and Nicolas Stouls. Génésyst: a tool to reason about behavioral aspects of B Event Specifications. application to security properties. In Proceedings of the International Conference on Formal Specification and Development in Z and B (ZB'05), volume 3455 of LNCS, pages 299-318, Guildford, United Kingdom, April 2005. Springer-Verlag. [ bib ]
[13] M. P. Bonacina, S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli. Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. In Proc. of the 3rd Int. Conference on Automated Reasoning (IJCAR), number 4130 in LNAI, pages 513-527, Seattle, WA, USA, August 2006. [ bib ]
[14] N. Boughanmi, S. Ranise, and C. Ringeissen. On Structural Information and the Experimental Evaluation of SMT Tools. In Proc. of the International Workshop on First-Order Theorem Proving (FTP'05), Koblenz, Germany, 2005. [ bib ]
[15] Sylvain Boulmé. Specifying and reasoning in Coq with high-order impure programs using specifications a la Dijkstra and refinement. Technical report, LSR laboratory, 2006.
http://www-lsr.imag.fr/Les.Personnes/Sylvain.Boulme/horefinement. [ bib ]
[16] Sylvain Boulmé and Marie-Laure Potet. Interpreting invariant composition in the B method using the Spec# ownership relation: a way to explain and relax B restrictions. In Julliand and Kouchnarenko [64]. [ bib ]
[17] F. Bouquet, F. Dadeau, and J. Groslambert. Checking JML Specifications with B Machines. In Proceedings of the International Conference on Formal Specification and Development in Z and B (ZB'05), volume 3455 of LNCS, pages 435-454, Guildford, United Kingdom, April 2005. Springer-Verlag. [ bib ]
[18] F. Bouquet, F. Dadeau, and J. Groslambert. JML2B: Checking JML specifications with B machines. In Julliand and Kouchnarenko [64]. [ bib ]
[19] F. Bouquet, F. Dadeau, J. Groslambert, and J. Julliand. Safety property driven test generation from JML specifications. In FATES/RV'06, 1st Int. Workshop on Formal Approaches to Testing and Runtime Verification, volume 4262 of LNCS, pages 225-239, Seattle, WA, USA, August 2006. Springer. [ bib ]
[20] F. Bouquet, F. Dadeau, and B. Legeard. How symbolic animation can help designing an efficient formal model. In Procs of the 7th Int. Conf. on Formal Engineering Methods (ICFEM'05), volume 3785 of LNCS, pages 96-110, Manchester, UK, November 2005. Springer-Verlag. [ bib ]
[21] F. Bouquet, F. Dadeau, and B. Legeard. Using constraint logic programming for the symbolic animation of formal models. In J. Marques-Silva and M. Velev, editors, Procs of the Int. Workshop on Constraints in Formal Verification (CFV'05) - Co-located with the Int. Conf. on Automated Deduction (CADE'05), pages 32-46, Tallinn, Estonia, July 2005. [ bib ]
[22] F. Bouquet, F. Dadeau, and B. Legeard. Automated boundary test generation from JML specifications. In FM'06, 14th Int. Conf. on Formal Methods, volume 4085 of LNCS, pages 428-443, Hamilton, Canada, August 2006. Springer-Verlag. [ bib ]
[23] F. Bouquet, F. Dadeau, and B. Legeard. JML-Testing-Tools, un animateur symbolique de spécifications JML. In AFADL'06, Approches Formelles dans l'Assistance au Développement de Logiciels, Paris, France, March 2006. Session outils. [ bib ]
[24] F. Bouquet, F. Dadeau, B. Legeard, and M. Utting. JML-testing-tools: a symbolic animator for JML specifications using CLP. In Proceedings of 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Tool session (TACAS'05), volume 3440 of LNCS, pages 551-556, Edinburgh, United Kingdom, April 2005. Springer-Verlag. [ bib ]
[25] F. Bouquet, F. Dadeau, B. Legeard, and M. Utting. Symbolic animation of JML specifications. In Proceedings of the International Conference on Formal Methods (FM'2005), volume 3582 of LNCS, pages 75-90, Newcastle Upon Tyne, United Kingdom, July 2005. Springer-Verlag. [ bib ]
[26] M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Ranise, and R. Sebastiani. Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In Proc. of the Int. Conf. on Computer-Aided Verification (CAV 2005), number 3576 in Lecture Notes in Computer Science, Edinburg, Scotland (UK), 2005. Springer-Verlag. [ bib ]
[27] M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. van Rossum, S. Ranise, and R. Sebastiani. Efficient Theory Combination via Boolean Search. Journal of Information and Computation, 10(204):1411-1596, 2006. Special Issue on Combining Logical Systems. [ bib ]
[28] C.-B. Breunesse, N. Catan o, M. Huisman, and B.P.F. Jacobs. Formal methods for smart cards: an experience report. Science of Computer Programming, 55(1-3):53-80, 2005. [ bib ]
[29] Lilian Burdy, Jean-Louis Lanet, and Antoine Requet. Jack: Java applet correctness kit, 2004. http://www-sop.inria.fr/everest/soft/Jack/jack.html. [ bib ]
[30] Lilian Burdy and Mariela Pavlova. Java bytecode specification and verification. In L.M. Liebrock, editor, 21st Annual ACM Symposium on Applied Computing (SAC'06), Dijon, April 2006. ACM Press. [ bib ]
[31] J. Charles. Vérification d'un composant Java: Le vérificateur de bytecode. Master's thesis, Université de Nice, 2005. [ bib ]
[32] J. Charles. Adding native specifications to JML. In Proceedings of the ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP'2006), 2006. [ bib ]
[33] Vikrant Chaudhary. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML : A case study. Technical report, IIT internship report, July 2004. [ bib ]
[34] S. Chouali, J. Julliand, P.-A. Masson, and F. Bellegarde. PLTL Partitionned Model-Checking for Reactive Systems under Fairness Assumptions. ACM - Transactions in Embedded Computing Systems (TECS), 4(2):267-301, 2005. [ bib ]
[35] Sylvain Conchon and Jean-Christophe Filliâtre. Type-Safe Modular Hash-Consing. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | .ps.gz ]
[36] Sylvain Conchon and Jean-Christophe Filliâtre. Union-Find Persistant. In Dix-huitièmes Journées Francophones des Langages Applicatifs. INRIA, January 2007. to appear. [ bib | .ps.gz ]
[37] Evelyne Contejean and Pierre Corbineau. Reflecting proofs in first-order logic with equality. In 20th International Conference on Automated Deduction (CADE-20), number 3632 in LNAI, pages 7-22, Tallinn, Estonia, July 2005. Springer-Verlag. [ bib ]
[38] J.-F. Couchot, F. Dadeau, D. Déharbe, A. Giorgetti, and S. Ranise. Proving and debugging set-based specifications. In A. Cavalcanti and P. Machado, editors, Electronic Notes in Theoretical Computer Science, proceedings of the Sixth Brazilian Workshop on Formal Methods (WMF'03), volume 95, pages 189-208, Campina Grande, Brazil, May 2004. [ bib | http ]
[39] J.-F. Couchot, D. Déharbe, A. Giorgetti, and S. Ranise. Scalable automated proving and debugging of set-based specifications. Journal of the Brazilian Computer Society, 9(2):17-36, November 2003. ISSN 0104-6500. [ bib | .ps.gz ]
[40] J.-F. Couchot, D. Déharbe, A. Giorgetti, and S. Ranise. Barvey : Vérification automatique de consistance de machines abstraites B. In J. Julliand, editor, Sessions Outils, Congrès Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL'04, pages 369-372, Besançon, France, June 2004. [ bib | .ps.gz ]
[41] J.-F. Couchot and A. Giorgetti. Analyse d'atteignabilité déductive. In J. Julliand, editor, Congrès Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL'04, pages 269-283, Besançon, France, June 2004. [ bib | .ps.gz ]
[42] A. Courbot, M. Pavlova, G. Grimaud, and J.J. Vandewalle. A low-footprint Java-to-native compilation scheme using formal methods. In J. Domingo-Ferrer, J. Posegga, and D. Schreckling, editors, Smart Card Research and Advanced Applications, 7th IFIP WG 8.8/11.2 International Conference, CARDIS 2006, volume 3928 of LNCS, pages 329-344. Springer-Verlag, April 2006. [ bib ]
[43] F. Dadeau. Animation de modèles JML et génération de tests fonctionnels. In MAJECSTIC'06, MAnifestation de JEunes Chercheurs STIC, Lorient, France, November 2006. [ bib | http ]
[44] F. Dadeau. √Čvaluation symbolique √† contraintes pour la validation, application √† Java/JML. PhD thesis, Université de Franche-Comté, 2006. [ bib ]
[45] F. Dadeau and A. Giorgetti. Vérification de machines abstraites B en logique monadique du second ordre. Rapport de Recherche RR2003-01, LIFC - Laboratoire d'Informatique de l'Université de Franche Comté, October 2003. [ bib | .pdf ]
[46] D. Déharbe and S. Ranise. Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In Proc. of the International Conference on Software Engineering and Formal Methods (SEFM03), Brisbane, Australia, September 2003. IEEE Computer Society Press. [ bib | .ps.gz ]
[47] D. Déharbe and S. Ranise. Satisfiability Solving for Software Verification. In ISoLA-2005: 2005 IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation, Columbia, Maryland, 2005. [ bib ]
[48] David Déharbe, Pascal Fontaine, Silvio Ranise, and Christophe Ringeissen. Decision Procedures for the Formal Analysis of Software. In 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, volume 4281 of Lecture Notes in Computer Science, Tunis, Tunisia, November 2006. Springer. Tutorial. [ bib ]
[49] David Déharbe and Sylvio Ranise. haRVey, 2004. http://www.loria.fr/~ranise/haRVey. [ bib ]
[50] Jean-Christophe Filliâtre. The Why certification tool. http://why.lri.fr/. [ bib ]
[51] Jean-Christophe Filliâtre. Backtracking iterators. In ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006. [ bib | .ps.gz ]
[52] Pascal Fontaine, Silvio Ranise, and Calogero G. Zarba. Combining lists with non-stably infinite theories. In Franz Baader and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 3452 of Lecture Notes in Computer Science, pages 51-66. Springer-Verlag, 2005. [ bib ]
[53] S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli. Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies. In B. Cook and R. Sebastiani, editors, Proc. of the IJCAR'06 Ws. PDPAR: Pragmatical Aspects of Decision Procedures in Automated Reasoning, Seattle, WA, USA, August 2006. [ bib ]
[54] S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli. Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies. In Proc. of the 10th European Conference on Logics in Artificial Intelligence (Jelia), number 4160 in Lecture Notes in Computer Science, September 2006. Extended version with full proofs, motivations, and examples in a technical report available at http://www.loria.fr/~ranise/pubs. [ bib ]
[55] A. Giorgetti and J. Groslambert. JAG : Génération d'annotations JML pour vérifier des propriétés temporelles. In AFADL'06, Approches Formelles dans l'Assistance au Développement de Logiciels, Paris, France, March 2006. Session outils. [ bib | .pdf ]
[56] A. Giorgetti and J. Groslambert. JAG: JML Annotation Generation for verifying temporal properties. In FASE'2006, Fundamental Approaches to Software Engineering, volume 3922 of LNCS, pages 373-376, Vienna, Austria, March 2006. Springer. [ bib | http ]
[57] J. Groslambert. A JAG extension for verifying LTL properties on B event systems. In Julliand and Kouchnarenko [64], pages 262-265. [ bib ]
[58] J. Groslambert. Verification of LTL on B event systems. In Julliand and Kouchnarenko [64]. [ bib ]
[59] J. Groslambert, J. Julliand, and O. Kouchnarenko. JML-based verification of liveness properties on a class. In SAVCBS'06, Specification and Verification of Component-Based Systems, Portland, Oregon, USA, November 2006. [ bib ]
[60] Amal Haddad. Modélisation et vérification de politiques de sécurité. Technical report, LSR laboratory, 2005.
http://www-lsr.imag.fr/Les.Personnes/Marie-Laure.Potet/PUBLI/DEA_Amal_HADDAD.pdf. [ bib ]
[61] Amal Haddad. Meca: a tool for Access Control Models. In Julliand and Kouchnarenko [64]. Tool session. [ bib | .pdf ]
[62] M. Huisman, P. Worah, and K. Sunesen. A temporal logic characterisation of observational determinism. In 19th IEEE Computer Security Foundations Workshop. IEEE Computer Society, July 2006. [ bib ]
[63] A. Imine, D. Déharbe, and S. Ranise. Abstraction-Driven Verification of Array Programs. In Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Computation (AISC'04), number 3249 in LNCS, pages 271-275, Linz, Austria, September 2004. Springer-Verlag. [ bib ]
[64] Jacques Julliand and Olga Kouchnarenko, editors. The 7th International B Conference (B'2007), volume 4355 of LNCS. Springer-Verlag, 2007. [ bib ]
[65] H. Kirchner, S. Ranise, C. Ringeissen, and D.-K. Tran. On Superposition-Based Satisfiability Procedures and their Combination. In Dang Van Hung and Martin Wirsing, editors, Proc. of the 2nd International Conference on Theoretical Aspects of Computing (ICTAC'05), volume 3722 of Lecture Notes in Computer Science, pages 594-608, Hanoi, Vietnam, October 2005. Springer. [ bib ]
[66] Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran. Automatic Combinability of Rewriting-Based Satisfiability Procedures. In Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), Lecture Notes in Artificial Intelligence, Phnom Penh, Cambodia, November 2006. Springer-Verlag. [ bib ]
[67] Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran. Building and Combining Satisfiability Procedures for Software Verification. In Proceedings of 3rd Taiwanese-French Conference on Information Technology (TFIT), pages 125-139, Nancy, France, March 2006. [ bib ]
[68] Stéphane Lescuyer. Codage de la logique du premier ordre polymorphe multi-sortée dans la logique sans sortes. Master's thesis, MPRI, 2006. [ bib ]
[69] Claude Marché and Christine Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, LNCS. Springer-Verlag, August 2005. [ bib ]
[70] Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1-2):89-106, 2004. [ bib | http ]
[71] Claude Marché and Nicolas Rousset. Verification of Java Card applets behavior with respect to transactions and card tears. In Dang Van Hung and Paritosh Pandya, editors, 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), Pune, India, September 2006. [ bib | .ps ]
[72] F. Mehta and S. Ranise. Automated provers doing (higher-order) proof search: A case study in the verification of pointer programs. In Proc. of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'04), 2004. [ bib ]
[73] Xavier Morselli, Marie-Laure Potet, and Nicolas Stouls. Génésyst : Génération d'un système de transitions étiquetées à partir d'une spécification B événementiel. In AFADL'2004, pages 317-320, June 2004. [ bib | .ps.gz ]
[74] M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet. Enforcing high-level security properties for applets. In J.-J. Quisquater, P. Paradinas, Y. Deswarte, and A.A. El Kalam, editors, CARDIS'04. Kluwer, 2004. An earlier version appeared as INRIA Technical Report, nr. RR-5061. [ bib ]
[75] Mariela Pavlova. Bytecode Verification and its Applications. PhD thesis, Université de Nice Sophia-Antipolis, January 2007. [ bib ]
[76] Marie-Laure Potet and Nicolas Stouls. Explicitation du contrôle de développement B événementiel. In J. Julliand, editor, AFADL'2004, pages 13-27, June 2004. [ bib | .ps.gz ]
[77] S. Ranise. Satisfiability Solving for Program Verification: towards the efficient Combination of Automated Theorem Provers and Satisfiability Modulo Theory Tools. In W. Ahrendt, P. Baumgartner, and H. de Nivelle, editors, Proc. of the IJCAR'06 Ws. DISPROVING: Non-Theorems, Non-Validity, Non-Provability, pages 49-58, Seattle, WA, USA, August 2006. Invited paper. [ bib ]
[78] S. Ranise, C. Ringeissen, and C. G. Zarba. Combining data structures with nonstably infinite theories using many-sorted logic. In B. Gramlich, editor, Proc. of the 5th Int. Workshop on Frontiers of Combining Systems (FroCoS'2005), volume 3717 of Lecture Notes in Computer Science, pages 48-64, Vienna, Austria, September 2005. Springer. [ bib ]
[79] S. Ranise and C. Tinelli. Satisfiability Modulo Theories. IEEE Magazine on Intelligent Systems, November 2006. To appear. [ bib ]
[80] S. Ranise and C. Zarba. A Theory of Singly-Linked Lists and its Extensible Decision Procedure. In Proc. of the 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM), Pune, India, September 2006. IEEE Computer Society Press. Extended version with full proofs, motivations, and examples in a technical report available at http://www.loria.fr/~ranise/pubs. [ bib ]
[81] Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran. Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn. In Keijiro Araki and Zhiming Liu, editors, First International Colloquium on Theoretical Aspects of Computing - ICTAC 2004, LNCS, Guiyang, Chine, September 2004. Springer-Verlag. In post-event proceedings. Also available as Research Report A04-R-193, LORIA, France. [ bib ]
[82] Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran. Producing Conflict Sets for Combination of Theories. In B. Cook and R. Sebastiani, editors, Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Seattle (WA), August 2006. Workshop affiliated to the 3rd International Joint Conference on Automated Reasoning, IJCAR. [ bib ]
[83] Silvio Ranise and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2006. [ bib ]
[84] Silvio Ranise and Cesare Tinelli. The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa, 2006. Available at www.SMT-LIB.org. [ bib ]
[85] Nicolas Stouls. Documentation d'introduction aux critères communs. Technical report, LSR laboratory, 2004.
http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/Productions/CC/CriteresCommuns.pdf. [ bib ]
[86] Nicolas Stouls and Vianney Darmaillacq. Développement formel d'un moniteur détectant les violations de politiques de sécurité de réseaux. In S. Vignes and V. Viguié Donzeau-Gouge, editors, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'06), pages 179-193, March 2006. http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/Productions/2005-09-AFADL06/AFADL06.pdf. [ bib ]
[87] Nicolas Stouls and Marie-Laure Potet. Security Policy Enforcement Through Refinement Process. pages 216-231, 2007. [ bib ]
[88] Cesare Tinelli and Calogero G. Zarba. Combining decision procedures for sorted theories. In José Júlio Alferes and Joao Alexandre Leite, editors, Logics in Artificial Intelligence, volume 3229 of Lecture Notes in Computer Science, pages 641-653. Springer-Verlag, 2004. [ bib ]
[89] Cesare Tinelli and Calogero G. Zarba. Combining non-stably infinite theories. Journal of Automated Reasoning, 34(3):209-238, 2005. [ bib ]
[90] Calogero G. Zarba, Domenico Cantone, and Jacob T. Schwartz. A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions, I. The: two-level case. Journal of Automated Reasoning, 33(3-4):251-269, 2004. [ bib ]

This file has been generated by bibtex2html 1.85.