References

  1. Serge Autexier (2015): Similarity-Based Diff, Three-Way Diff and Merge. International Journal of Software & Informatics 9(2). Available at http://www.ijsi.org/ch/reader/view_abstract.aspx?file_no=i217.
  2. John Barnes (2012): SPARK: The Proven Approach to High Integrity Software. Altran Praxis, http://www.altran.co.uk, UK.
  3. François Bobot, Sylvain Conchon, Evelyne Contejean & Stéphane Lescuyer (2008): Implementing Polymorphism in SMT solvers. In: SMT '08/BPR '08: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning. ACM, New York, NY, USA, pp. 1–5, doi:10.1145/1512464.1512466. Available at http://www.lri.fr/~conchon/publis/conchon-smt08.pdf.
  4. ClearSy System Engineering: Atelier B User Manual, version 4.0. Available at http://tools.clearsy.com/wp-content/uploads/sites/8/resources/User_uk.pdf.
  5. Sylvain Conchon, Evelyne Contejean & Mohamed Iguernelala (2012): Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation. Logical Methods in Computer Science 8(3), doi:10.2168/LMCS-8(3:16)2012. Available at http://www.lri.fr/~conchon/publis/conchon-lmcs2012.pdf.
  6. Sylvain Conchon, Evelyne Contejean, Johannes Kanig & Stéphane Lescuyer (2008): CC(X): Semantic Combination of Congruence Closure with Solvable Theories. Electronic Notes in Theoretical Computer Science 198(2), pp. 51–69, doi:10.1016/j.entcs.2008.04.080. Available at http://www.lri.fr/~conchon/publis/conchon-entcs08.pdf.
  7. Sylvain Conchon & Mohamed Iguernelala (2016): Increasing Proofs Automation Rate of Atelier-B Thanks to Alt-Ergo. In: Thierry Lecomte, Ralf Pinger & Alexander Romanovsky: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification - First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, Lecture Notes in Computer Science 9707. Springer, pp. 243–253, doi:10.1007/978-3-319-33951-1.
  8. Claire Dross, Sylvain Conchon, Johannes Kanig & Andrei Paskevich (2016): Adding Decision Procedures to SMT Solvers using Axioms with Triggers. Journal of Automated Reasoning 56(4), pp. 387–457, doi:10.1007/s10817-015-9352-2.
  9. Jean-Christophe Filliâtre & Andrei Paskevich (2013): Why3 - Where Programs Meet Provers. In: ESOP, pp. 125–128, doi:10.1007/978-3-642-37036-6_8.
  10. Mohamed Iguernelala (2013): Strengthening the heart of an SMT-solver : Design and implementation of efficient decision procedures. (Renforcement du noyau d'un démonstrateur SMT : Conception et implantation de procédures de décisions efficaces). University of Paris-Sud, Orsay, France. Available at https://tel.archives-ouvertes.fr/tel-00842555.
  11. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles & Boris Yakobowski (2015): Frama-C: A software analysis perspective. Formal Aspects of Computing 27(3), pp. 573–609, doi:10.1007/s00165-014-0326-7.
  12. MichałMoskal, Jakub Łopuszański & Joseph R. Kiniry (2008): E-matching for Fun and Profit. Electron. Notes Theor. Comput. Sci. 198, pp. 19–35, doi:10.1016/j.entcs.2008.04.078. Available at http://dl.acm.org/citation.cfm?id=1371256.1371287.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org