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