Bibliography

Major publications by the team in recent years

• 1T. Bouton, D. C. B. de Oliveira, D. Déharbe, P. Fontaine.
  
  veriT: an open, trustable and efficient SMT-solver, in: Proc. Conference on Automated Deduction (CADE), Montreal, Canada, R. Schmidt (editor), Lecture Notes in Computer Science, Springer, 2009, vol. 5663, pp. 151-156.
• 2D. Cansell, D. Méry.
  
  The Event-B Modelling Method: Concepts and Case Studies, in: Logics of Specification Languages, Berlin-Heidelberg, D. Bjørner, M. C. Henson (editors), Monographs in Theoretical Computer Science, Springer, 2008, pp. 47-152.
• 3D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, H. Vanzetto.
  
  TLA+ Proofs, in: 18th International Symposium On Formal Methods - FM 2012, Paris, France, D. Giannakopoulou, D. Méry (editors), Lecture Notes in Computer Science, Springer, 2012, vol. 7436, pp. 147-154.
• 4A. Dolzmann, T. Sturm.
  
  Redlog: Computer algebra meets computer logic, in: ACM SIGSAM Bull., 1997, vol. 31, n^o 2, pp. 2-9.
• 5D. Déharbe, P. Fontaine, S. Merz, B. Woltzenlogel Paleo.
  
  Exploiting Symmetry in SMT Problems, in: 23rd Intl. Conf. Automated Deduction (CADE 2011), Wroclaw, Poland, N. Bjørner, V. Sofronie-Stokkermans (editors), LNCS, Springer, 2011, vol. 6803, pp. 222-236.
• 6A. Fietzke, C. Weidenbach.
  
  Superposition as a Decision Procedure for Timed Automata, in: Mathematics in Computer Science, 2012, vol. 6, n^o 4, pp. 409-425.
• 7E. Kruglov, C. Weidenbach.
  
  Superposition Decides the First-Order Logic Fragment Over Ground Theories, in: Mathematics in Computer Science, 2012, vol. 6, n^o 4, pp. 427-456.
• 8F. Kröger, S. Merz.
  
  Temporal Logic and State Systems, Texts in Theoretical Computer Science, Springer, 2008, 436 p.
  
  http://hal.inria.fr/inria-00274806/en/
• 9S. Merz.
  
  The Specification Language TLA⁺, in: Logics of Specification Languages, Berlin-Heidelberg, D. Bjørner, M. C. Henson (editors), Monographs in Theoretical Computer Science, Springer, 2008, pp. 401-451.
• 10C. Weidenbach, D. Dimova, A. Fietzke, M. Suda, P. Wischnewski.
  
  SPASS Version 3.5, in: 22nd International Conference on Automated Deduction (CADE-22), Montreal, Canada, R. Schmidt (editor), LNAI, Springer, 2009, vol. 5663, pp. 140-145.

Publications of the year

Doctoral Dissertations and Habilitation Theses

• 11M. B. Andriamiarina.
  
  Developing correct-by-construction distributed algorithms, Université de Lorraine ; Loria & Inria Grand Est, October 2015.
  
  https://hal.inria.fr/tel-01258363
• 12M. Guthmuller.
  
  Dynamic formal verification of temporal properties on legacy distributed applications, Université de Lorraine, June 2015.
  
  https://tel.archives-ouvertes.fr/tel-01231868

Articles in International Peer-Reviewed Journals

• 13Y. Ait Ameur, D. Méry.
  
  Making explicit domain knowledge in formal system development, in: Science of Computer Programming, December 2015.
  
  https://hal.inria.fr/hal-01245832
• 14P. Ballarini, B. Barbot, M. Duflot, S. Haddad, N. Pekergin.
  
  HASL: A new approach for performance evaluation and model checking from concepts to experimentation, in: Performance Evaluation, August 2015, vol. 90, pp. 53-77. [ DOI : 10.1016/j.peva.2015.04.003 ]
  
  https://hal.inria.fr/hal-01221815
• 15P. Ballarini, M. Duflot.
  
  Applications of an expressive statistical model checking approach to the analysis of genetic circuits, in: Journal of Theoretical Computer Science (TCS), 2015, vol. 599, 30 p. [ DOI : 10.1016/j.tcs.2015.05.018 ]
  
  https://hal.inria.fr/hal-01250521
• 16J. C. Blanchette, S. Böhme, M. Fleury, S. J. Smolka, A. Steckermeier.
  
  Semi-intelligible Isar Proofs from Machine-Generated Proofs, in: Journal of Automated Reasoning, 2016. [ DOI : 10.1007/s10817-015-9335-3 ]
  
  https://hal.inria.fr/hal-01211748
• 17H. Errami, M. Eiswirth, D. Grigoriev, W. M. Seiler, T. Sturm, A. Weber.
  
  Detection of Hopf bifurcations in chemical reaction networks using convex coordinates, in: Journal of Computational Physics, June 2015, vol. 291, pp. 279–302. [ DOI : 10.1016/j.jcp.2015.02.050 ]
  
  https://hal.inria.fr/hal-01239486

Invited Conferences

• 18J. C. Blanchette, M. Haslbeck, D. Matichuk, T. Nipkow.
  
  Mining the Archive of Formal Proofs, in: CICM 2015, Washington DC, United States, Intelligent Computer Mathematics - International Conference, CICM 2015, July 13-17, Proceedings, July 2015. [ DOI : 10.1007/978-3-319-20615-8_1 ]
  
  https://hal.inria.fr/hal-01212594

International Conferences with Proceedings

• 19G. Alagi, C. Weidenbach.
  
  NRCL - a model building approach to the Bernays-Schönfinkel fragment, in: Frontiers of Combining Systems, 10th International Symposium (FroCos 2015), Wroclaw, Poland, C. Lutz, S. Ranise (editors), Springer, 2015, vol. 9322, pp. 69-84. [ DOI : 10.1007/978-3-319-24246-0_5 ]
  
  https://hal.inria.fr/hal-01247991
• 20P. Baumgartner, J. Bax, U. Waldmann.
  
  Beagle – A Hierarchic Superposition Prover, in: 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, A. P. Felty, A. Middeldorp (editors), Lecture Notes in Computer Science, Springer, August 2015, vol. 9195, pp. 367-377. [ DOI : 10.1007/978-3-319-21401-6_25 ]
  
  https://hal.inria.fr/hal-01251377
• 21J. C. Blanchette, A. Popescu, D. Traytel.
  
  Foundational Extensible Corecursion: A Proof Assistant Perspective, in: ICFP 2015, Vancouver, Canada, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, September 1-3, August 2015. [ DOI : 10.1145/2784731.2784732 ]
  
  https://hal.inria.fr/hal-01212589
• 22J. C. Blanchette, A. Popescu, D. Traytel.
  
  Witnessing (Co)datatypes, in: ESOP 2015, London, United Kingdom, Programming Languages and Systems - 24th European Symposium on Programming, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, April 11-18, Proceedings, April 2015. [ DOI : 10.1007/978-3-662-46669-8_15 ]
  
  https://hal.inria.fr/hal-01212587
• 23M. Bromberger, T. Sturm, C. Weidenbach.
  
  Linear Integer Arithmetic Revisited, in: 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, Springer, August 2015, vol. 9195, pp. 623-637.
  
  https://hal.inria.fr/hal-01239394
• 24P. Chocron, P. Fontaine, C. Ringeissen.
  
  A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited, in: 25th International Conference on Automated Deduction, CADE-25, Berlin, Germany, A. P. Felty, A. Middeldorp (editors), Lecture Notes in Computer Science, Springer, August 2015, vol. 9195, pp. 419-433. [ DOI : 10.1007/978-3-319-21401-6_29 ]
  
  https://hal.inria.fr/hal-01157898
• 25P. Chocron, P. Fontaine, C. Ringeissen.
  
  A Rewriting Approach to the Combination of Data Structures with Bridging Theories, in: Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, C. Lutz, S. Ranise (editors), Lecture Notes in Computer Science, Springer, September 2015, vol. 9322, pp. 275–290. [ DOI : 10.1007/978-3-319-24246-0_17 ]
  
  https://hal.inria.fr/hal-01206187
• 26M. Guthmuller, M. Quinson, G. Corona.
  
  System-level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications, in: Formal Approaches to Parallel and Distributed Systems (4PAD) - Special Session of Parallel, Distributed and network-based Processing (PDP), Turku, Finland, March 2015.
  
  https://hal.archives-ouvertes.fr/hal-01097204
• 27M. Jaroschek, P. F. Dobal, P. Fontaine.
  
  Adapting Real Quantifier Elimination Methods for Conflict Set Computation, in: Frontiers of Combining Systems (FroCoS), Wroclaw, Poland, C. Lutz, S. Ranise (editors), LNCS, Springer, 2015, vol. 9322, pp. 151-166. [ DOI : 10.1007/978-3-319-24246-0_10 ]
  
  https://hal.inria.fr/hal-01240343
• 28D. Méry, S. Rushikesh, A. Tarasyuk.
  
  Integrating Domain-Based Features into Event-B: a Nose Gear Velocity Case Study, in: Model and Data Engineering - 5th International Conference, MEDI 2015, Rhodes, Greece, L. Bellatreche, Y. Manolopoulos (editors), springer, September 2015, vol. lncs 9344, pp. 89-102.
  
  https://hal.inria.fr/hal-01245991
• 29D. Méry, N. K. Singh.
  
  Analyzing Requirements Using Environment Modelling, in: Digital Human Modeling - Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health - 6th International Conference, DHM 2015, Los Angeles, United States, V. G. Duffy (editor), Lecture Notes in Computer Science - Held as Part of HCI International 2015, Springer, August 2015, vol. 9185.
  
  https://hal.inria.fr/hal-01245994
• 30M. Quinson, G. Oster.
  
  A Teaching System To Learn Programming: the Programmer's Learning Machine, in: ACM Conference on Innovation and Technology in Computer Science Education 2015, Vilnius, Lithuania, ACM, July 2015. [ DOI : 10.1145/2729094.2742626 ]
  
  https://hal.inria.fr/hal-01238377
• 31A. Reynolds, J. C. Blanchette.
  
  A Decision Procedure for (Co)datatypes in SMT Solvers, in: CADE-25, Berlin, Germany, Automated Deduction - 25th International Conference on Automated Deduction, August 1-7, 2015, Proceedings, August 2015. [ DOI : 10.1007/978-3-319-21401-6_13 ]
  
  https://hal.inria.fr/hal-01212585
• 32R. Schmidt, U. Waldmann.
  
  Modal Tableau Systems with Blocking and Congruence Closure, in: 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Wroclaw, Poland, H. de Nivelle (editor), Lecture Notes in Computer Science, Springer, September 2015, vol. 9323, pp. 38-53. [ DOI : 10.1007/978-3-319-24312-2_4 ]
  
  https://hal.inria.fr/hal-01251380
• 33T. Sturm.
  
  Subtropical Real Root Finding, in: Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, Bath, United Kingdom, ACM, July 2015.
  
  https://hal.inria.fr/hal-01239489

Conferences without Proceedings

• 34H. Barbosa, P. Fontaine.
  
  Congruence Closure with Free Variables (Work in Progress), in: Quantify 2015 : 2nd International Workshop on Quantification, Berlin, Germany, 2015.
  
  https://hal.inria.fr/hal-01246036
• 35M. Duflot, M. Quinson, F. Masseglia, D. Roy, J. Vaubourg, T. Viéville.
  
  When sharing computer science with everyone also helps avoiding digital prejudices, in: Scratch2015AMS, Amsterdam, Netherlands, August 2015.
  
  https://hal.inria.fr/hal-01154767
• 36A. Reynolds, J. C. Blanchette, C. Tinelli.
  
  Model Finding for Recursive Functions in SMT, in: SMT Workshop 2015, San Francisco, United States, July 2015.
  
  https://hal.inria.fr/hal-01242509

Scientific Books (or Scientific Book chapters)

• 37C. Areces, P. Fontaine, S. Merz.
  
  Modal Satisfiability via SMT Solving, in: Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, Lecture Notes in Computer Science, Springer, 2015, vol. 8950, pp. 30-45. [ DOI : 10.1007/978-3-319-15545-6_5 ]
  
  https://hal.inria.fr/hal-01127966
• 38C. Dubois, P. Masci, D. Méry.
  
  Second International Workshop on Formal Integrated Development Environment, EPTCS, June 2015, n^o 187. [ DOI : 10.4204/EPTCS.187 ]
  
  https://hal.inria.fr/hal-01246691
• 39P. Fontaine, T. Sturm, U. Waldmann.
  
  D. Wang (editor), Foreword to the Special Focus on Constraints and Combinations, Mathematics in Computer Science, Springer, October 2015, vol. 9, n^o 3. [ DOI : 10.1007/s11786-015-0239-8 ]
  
  https://hal.inria.fr/hal-01239438
• 40C. Weidenbach.
  
  Automated Reasoning Building Blocks, in: Correct System Design – Symposium in Honor of Ernst-Rüdiger Olderog, R. Meyer, A. Platzer, H. Wehrheim (editors), Springer, September 2015, vol. 9360, pp. 172-188. [ DOI : 10.1007/978-3-319-23506-6_12 ]
  
  https://hal.inria.fr/hal-01239428

Internal Reports

• 41H. Barbosa, P. Fontaine.
  
  Congruence Closure with Free Variables (Work in Progress), Inria Nancy - Grand Est (Villers-lès-Nancy, France), August 2015.
  
  https://hal.inria.fr/hal-01235912

Scientific Popularization

• 42M. B. Andriamiarina, D. Méry, N. K. Singh.
  
  Incremental Proof-Based Development for Resilient Distributed Systems, in: Trustworthy Cyber-Physical Systems Engineering, Tylor and Francis Group, December 2015.
  
  https://hal.archives-ouvertes.fr/hal-01246669
• 43D. Méry, M. Poppleton.
  
  Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems, in: Software and Systems Modeling (SoSyM), December 2015.
  
  https://hal.inria.fr/hal-01245819

Other Publications

• 44M. Kosta, T. Sturm, A. Dolzmann.
  
  Better Answers to Real Questions, 2015, working paper or preprint.
  
  https://hal.inria.fr/hal-01248053
• 45M. Kosta, T. Sturm.
  
  A Generalized Framework for Virtual Substitution, January 2015, 17 p, preprint.
  
  https://hal.inria.fr/hal-01239431
• 46S. Merz, H. Vanzetto.
  
  Encoding TLA+ set theory into many-sorted first-order logic, December 2015, working paper or preprint.
  
  https://hal.inria.fr/hal-01244627
• 47M. Voigt, C. Weidenbach.
  
  Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete, January 2015, preprint.
  
  https://hal.inria.fr/hal-01239399

References in notes

• 48Gurobi Optimizer Reference Manual, Gurobi Optimization, Inc., 2014.
• 49J.-R. Abrial.
  
  Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010.
• 50L. Bachmair, H. Ganzinger.
  
  Rewrite-Based Equational Theorem Proving with Selection and Simplification, in: Journal of Logic and Computation, 1994, vol. 4, n^o 3, pp. 217–247.
• 51R. Back, J. von Wright.
  
  Refinement calculus—A systematic introduction, Springer Verlag, 1998.
• 52C. Barrett, R. Sebastiani, S. A. Seshia, C. Tinelli.
  
  Satisfiability Modulo Theories, in: Handbook of Satisfiability, A. Biere, Marijn J. H. Heule, H. van Maaren, T. Walsh (editors), Frontiers in Artificial Intelligence and Applications, IOS Press, February 2009, vol. 185, chap. 26, pp. 825-885.
• 53D. Déharbe, P. Fontaine, Y. Guyot, L. Voisin.
  
  SMT solvers for Rodin, in: ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, Pisa, Italy, J. Derrick, J. A. Fitzgerald, S. Gnesi, S. Khurshid, M. Leuschel, S. Reeves, E. Riccobene (editors), Lecture Notes in Computer Science, Springer, 2012, vol. 7316, pp. 194-207.
• 54M. El Kahoui, A. Weber.
  
  Deciding Hopf Bifurcations by Quantifier Elimination in a Software-Component Architecture, in: Journal of Symbolic Computation, 2000, vol. 30, n^o 2, pp. 161-179.
• 55H. Errami, M. Eiswirth, D. Grigoriev, W. M. Seiler, T. Sturm, A. Weber.
  
  Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates, in: Computer Algebra in Scientific Computing, Berlin, V. P. Gerdt, W. Koepf, E. W. Mayr, E. V. Vorozhtsov (editors), Lecture Notes in Computer Science, Springer, 2013, vol. 8136, pp. 88–99.
• 56H. Errami, W. M. Seiler, T. Sturm, A. Weber.
  
  On Muldowney's Criteria for Polynomial Vector Fields with Constraints, in: Proceedings of the CASC 2011, LNCS, Springer, 2011, vol. 6885, pp. 135–143.
• 57K. Gatermann, M. Eiswirth, A. Sensse.
  
  Toric ideals and graph theory to analyze Hopf bifurcations in mass action systems, in: Journal of Symbolic Computation, 2005, vol. 40, pp. 1361–1382.
• 58K. Gatermann, S. Hosten.
  
  Computational Algebra for Bifurcation Theory, in: Journal of Symbolic Computation, 2005, vol. 40, n^o 4–5, pp. 1180-1207.
• 59E. Hairer, S. Norsett, G. Wanner.
  
  Solving Ordinary Differential Equations I. Nonstiff Problems, Series in Computational Mathematics, Springer, 1993, vol. 8.
• 60J. K. Hale, H. Kocak.
  
  Dynamics and Bifurcations, Texts in Applied Mathematics, Springer, 1991, vol. 3.
• 61A. C. Hearn, R. Schöpf.
  
  Reduce User's Manual, Free Version, October 2014.
• 62D. Jovanović, L. de Moura.
  
  Cutting to the Chase, in: Journal of Automated Reasoning, 2013, vol. 51, n^o 1, pp. 79-108.
• 63M. Lamotte-Schubert, C. Weidenbach.
  
  BDI: a new decidable clause class, in: Journal of Logic and Computation, 2014, vol. 24, n^o 6, 28 p.
  
  https://hal.inria.fr/hal-01098084
• 64L. Lamport.
  
  Specifying Systems, Addison-Wesley, Boston, Mass., 2002.
• 65M. Lemerre, E. Ohayon.
  
  A Model of Parallel Deterministic Real-Time Computation, in: Proc. 33rd IEEE Real-Time Systems Symposium (RTSS 2012), San Juan, PR, U.S.A., IEEE Comp. Soc., 2012, pp. 273-282.
• 66C. Morgan.
  
  Programming from Specifications, Prentice Hall, 1998, 2nd edition.
• 67H. Peyrl, P. A. Parrilo.
  
  Computing sum of squares decompositions with rational coefficients, in: Theor. Comput. Sci., 2008, vol. 409, n^o 2, pp. 269–281.
• 68A. Reynolds, C. Tinelli, L. de Moura.
  
  Finding conflicting instances of quantified formulas in SMT, in: Formal Methods in Computer-Aided Design, FMCAD 2014, IEEE, 2014, pp. 195-202.
• 69A. Rowstron, P. Druschel.
  
  Pastry: Scalable, Decentralized Object Location, and Routing for Large-Scale Peer-to-Peer Systems, in: IFIP/ACM International Conference on Distributed Systems Platforms (Middleware 2001), Heidelberg, Germany, R. Guerraoui (editor), Lecture Notes in Computer Science, Springer, 2001, vol. 2218, pp. 329-350.
• 70V. Sofronie-Stokkermans.
  
  Hierarchical and modular reasoning in complex theories: The case of local theory extensions, in: Frontiers of Combining Systems. 6th International Symposium FroCos 2007, Proceedings, Liverpool, UK, B. Konev, F. Wolter (editors), Lecture Notes in Computer Science, Springer, 2007, vol. 4720, pp. 47-71, Invited paper.
• 71T. Sturm, A. Weber, E. O. Abdel-Rahman, M. El Kahoui.
  
  Investigating Algebraic and Logical Algorithms to Solve Hopf Bifurcation Problems in Algebraic Biology, in: Mathematics in Computer Science, March 2009, vol. 2, n^o 3, pp. 493–515.
• 72T. Sturm, A. Weber.
  
  Investigating Generic Methods to Solve Hopf Bifurcation Problems in Algebraic Biology, in: Proceedings of Algebraic Biology 2008, RISC, Castle of Hagenberg, Austria, July 31–August 2,, Berlin, Heidelberg, K. Horimoto (editor), Lecture Notes in Computer Science (LNCS), Springer-Verlag, 2008, vol. 5147, pp. 200–215.
• 73B. Sturmfels.
  
  Solving Systems of Polynomial Equations, AMS, Providence, RI, 2002.
• 74D. Wang, B. Xia.
  
  Stability Analysis of Biological Systems with Real Solution Classification, in: Proceedings of the ISSAC 2005, ACM Press, 2005, pp. 354-361.