EN FR
EN FR


previous Previous | up Home


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, no 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, no 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, no 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

Articles in International Peer-Reviewed Journals

  • 11Y. Ait Ameur, D. Méry.

    Making explicit domain knowledge in formal system development, in: Science of Computer Programming, March 2016, vol. 121, no 100–127. [ DOI : 10.1016/j.scico.2015.12.004 ]

    https://hal.inria.fr/hal-01245832
  • 12J. 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
  • 13J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, J. Urban.

    A Learning-Based Fact Selector for Isabelle/HOL, in: Journal of Automated Reasoning, 2016, vol. 57, pp. 219 - 244. [ DOI : 10.1007/s10817-016-9362-8 ]

    https://hal.inria.fr/hal-01386986
  • 14J. C. Blanchette, C. Kaliszyk, L. C. Paulson, J. Urban.

    Hammering towards QED, in: Journal of Formalized Reasoning, 2016, vol. 9, no 1, pp. 101-148.

    https://hal.inria.fr/hal-01386988
  • 15M. Košta, T. Sturm, A. Dolzmann.

    Better answers to real questions, in: Journal of Symbolic Computation, 2016, vol. 74, pp. 255 - 275. [ DOI : 10.1016/j.jsc.2015.07.002 ]

    https://hal.inria.fr/hal-01388720
  • 16S. Merz, J. Pang.

    Editorial, in: Formal Aspects of Computing, 2016, vol. 28, no 3, pp. 343-344. [ DOI : 10.1007/s00165-016-0390-2 ]

    https://hal.inria.fr/hal-01356470
  • 17S. Merz, J. Pang.

    Editorial, in: Formal Aspects of Computing, 2016, vol. 28, no 5, pp. 723-724. [ DOI : 10.1007/s00165-016-0390-2 ]

    https://hal.inria.fr/hal-01356471
  • 18D. Méry.

    Playing with State-Based Models for Designing Better Algorithms, in: Future Generation Computer Systems, May 2016, 25 p.

    https://hal.inria.fr/hal-01316026

Invited Conferences

    International Conferences with Proceedings

    • 20E. H. Abrahám, J. Abbott, B. Becker, A. M. Bigatti, M. M. Brain, B. Buchberger, A. Cimatti, J. H. Davenport, M. M. England, P. Fontaine, S. M. Forrest, A. Griggio, D. Kroening, W. M. Seiler, T. Sturm.

      SC 2 : Satisfiability Checking meets Symbolic Computation (Project Paper), in: Intelligent Computer Mathematics, Bialystok, Poland, July 2016.

      https://hal.inria.fr/hal-01377655
    • 21S. Azaiez, D. Doligez, M. Lemerre, T. Libal, S. Merz.

      Proving Determinacy of the PharOS Real-Time Operating System, in: Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, M. J. Butler, K.-D. Schewe, A. Mashkoor, M. Biró (editors), LNCS - Lecture Notes in Computer Science, Springer, May 2016, vol. 9675, pp. 70-85. [ DOI : 10.1007/978-3-319-33600-8_4 ]

      https://hal.inria.fr/hal-01322335
    • 22N. Azmy, S. Merz, C. Weidenbach.

      A Rigorous Correctness Proof for Pastry, in: Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, M. J. Butler, K.-D. Schewe, A. Mashkoor, M. Biró (editors), Springer, 2016, vol. 9675, pp. 86-101. [ DOI : 10.1007/978-3-319-33600-8_5 ]

      https://hal.inria.fr/hal-01322342
    • 23J. C. Blanchette, A. Bouzy, A. Lochbihler, A. Popescu, D. Traytel.

      Friends with Benefits: Implementing Foundational Corecursion in Isabelle/HOL (Extended Abstract), in: Isabelle Workshop 2016, Nancy, France, August 2016.

      https://hal.inria.fr/hal-01401812
    • 24J. C. Blanchette, M. Fleury, C. Weidenbach.

      A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Extended Abstract), in: Isabellle Workshop 2016, Nancy, France, August 2016.

      https://hal.inria.fr/hal-01401807
    • 26M. Bromberger, C. Weidenbach.

      Computing a Complete Basis for Equalities Implied by a System of LRA Constraints, in: 14th International Workshop on Satisfiability Modulo Theories, Coimbra, Portugal, T. King, R. Piskac (editors), CEUR Workshop Proceedings, 2016, vol. 1617, pp. 15-30.

      https://hal.inria.fr/hal-01403214
    • 27M. Bromberger, C. Weidenbach.

      Fast Cube Tests for LIA Constraint Solving, in: Automated Reasoning - 8th International Joint Conference (IJCAR 2016), Coimbra, Portugal, N. Olivetti, A. Tiwari (editors), Lecture Notes in Computer Science, Springer, 2016, vol. 9706, pp. 116-132. [ DOI : 10.1007/978-3-319-40229-1_9 ]

      https://hal.inria.fr/hal-01403200
    • 28S. Cruanes, J. C. Blanchette.

      Extending Nunchaku to Dependent Type Theory, in: Hammers for Type Theories (HaTT 2016), Coimbra, Portugal, Proceedings First International Workshop on Hammers for Type Theories, July 2016, vol. 210, pp. 3 - 12. [ DOI : 10.4204/EPTCS.210.3 ]

      https://hal.inria.fr/hal-01401696
    • 29C. Fetzer, C. Weidenbach, P. Wischnewski.

      Compliance, Functional Safety and Fault Detection by Formal Methods, in: Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2016), Corfu, Greece, T. Margaria, B. Steffen (editors), Lecture Notes in Computer Science, Springer, 2016, vol. 9953, pp. 626 - 632. [ DOI : 10.1007/978-3-319-47169-3_48 ]

      https://hal.inria.fr/hal-01403190
    • 30J. Haël Brenas, R. Echahed, M. Strecker.

      Ensuring Correctness of Model Transformations While Remaining Decidable, in: Theoretical Aspects of Computing - ICTAC, Taipei, Taiwan, Theoretical Aspects of Computing – ICTAC 2016 13th International Colloquium, Taipei, Taiwan, ROC, October 24–31, 2016, Proceedings, October 2016, pp. 315 - 332. [ DOI : 10.1007/978-3-319-46750-4_18 ]

      https://hal.archives-ouvertes.fr/hal-01403585
    • 31S. Merz, H. Vanzetto.

      Encoding TLA+ into Many-Sorted First-Order Logic, in: Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, M. J. Butler, K.-D. Schewe, A. Mashkoor, M. Biró (editors), Springer, 2016, vol. 9675, pp. 54-69. [ DOI : 10.1007/978-3-319-33600-8_3 ]

      https://hal.inria.fr/hal-01322328
    • 32D. Méry, R. Monahan, C. Zheng.

      On two Friends for getting Correct ProgramsAutomatically Translating Event B Specifications to Recursive Algorithms in Rodin, in: ISOLA 2016, CORFU, Greece, B. Steffen, T. Margaria (editors), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, Springer, October 2016, vol. I, no 9952, 18 p. [ DOI : 10.1007/978-3-319-47166-2_57 ]

      https://hal.inria.fr/hal-01369425
    • 33A. Reynolds, J. C. Blanchette, S. Cruanes, C. Tinelli.

      Model Finding for Recursive Functions in SMT, in: 8th International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, June 2016. [ DOI : 10.1007/978-3-319-40229-1_10 ]

      https://hal.inria.fr/hal-01336082
    • 34T. Sturm, M. Voigt, C. Weidenbach.

      Deciding First-Order Satisfiability when Universal and Existential Variables are Separated, in: LICS 2016, New York, United States, July 2016, pp. 86 - 95. [ DOI : 10.1145/2933575.2934532 ]

      https://hal.inria.fr/hal-01389744
    • 35A. Teucke, C. Weidenbach.

      Ordered Resolution with Straight Dismatching Constraints, in: 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), Coimbra, Portugal, P. Fontaine, S. Schulz, J. Urban (editors), CEUR Workshop Proceedings, 2016, vol. 1635, pp. 95-109.

      https://hal.inria.fr/hal-01403206

    Scientific Books (or Scientific Book chapters)

    • 36M. B. Andriamiarina, D. Méry, N. K. Singh.

      Incremental Proof-Based Development for Resilient Distributed Systems, in: Trustworthy Cyber-Physical Systems Engineering, Trustworthy Cyber-Physical Systems Engineering, Taylor and Francis Group, September 2016.

      https://hal.archives-ouvertes.fr/hal-01246669

    Books or Proceedings Editing

    • 37J. C. Blanchette, S. Merz (editors)

      Interactive Theorem Proving: 7th International Conference, ITP 2016, Lecture Notes in Computer Science, Springer, Nancy, France, 2016, vol. 9807. [ DOI : 10.1007/978-3-319-43144-4 ]

      https://hal.inria.fr/hal-01356464
    References in notes
    • 38J.-R. Abrial.

      Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010.
    • 39L. Bachmair, H. Ganzinger.

      Rewrite-Based Equational Theorem Proving with Selection and Simplification, in: Journal of Logic and Computation, 1994, vol. 4, no 3, pp. 217–247.
    • 40R. Back, J. von Wright.

      Refinement calculus—A systematic introduction, Springer Verlag, 1998.
    • 41C. 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.
    • 42P. 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
    • 43P. 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
    • 44N. Foster, A. Guha, M. Reitblatt, A. Story, M. J. Freedman, N. Praveen Katta, C. Monsanto, J. Reich, J. Rexford, C. Schlesinger, D. Walker, R. Harrison.

      Languages for software-defined networks, in: IEEE Communications Magazine, 2013, vol. 51, no 2, pp. 128-134.
    • 45L. Lamport.

      Specifying Systems, Addison-Wesley, Boston, Mass., 2002.
    • 46M. 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.
    • 47T. Lu.

      Formal Verification of the Pastry Protocol, Universität des Saarlandes and Université de Lorraine, 2013.
    • 48C. Morgan.

      Programming from Specifications, Prentice Hall, 1998, 2nd edition.
    • 49D. 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, Rhodos, Greece, L. Bellatreche, Y. Manolopoulos (editors), LNCS, Springer, 2015, vol. 9344, pp. 89-102.

      https://hal.inria.fr/hal-01245991
    • 50D. Ongaro, J. K. Ousterhout.

      In Search of an Understandable Consensus Algorithm, in: USENIX Annual Technical Conference 2014, Philadelphia, PA, G. Gibson, N. Zeldovich (editors), Usenix Association, 2014, pp. 305-319.
    • 51A. 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.
    • 52V. 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.
    • 53S. A. Weil, S. A. Brandt, E. L. Miller, D. D. E. Long, C. Maltzahn.

      Ceph: A Scalable, High-Performance Distributed File System, in: 7th Symp. Operating Systems Design and Implementation (OSDI '06), Seattle, WA, Usenix Association, 2006, pp. 307-320.


    previous Previous | up Home