Why3: Shepherd your herd of provers F Bobot, JC Filliâtre, C Marché, A Paskevich | 316 | 2011 |
Implementing polymorphism in SMT solvers F Bobot, S Conchon, E Contejean, S Lescuyer Proceedings of the Joint Workshops of the 6th International Workshop on …, 2008 | 67 | 2008 |
The Alt-Ergo automated theorem prover, 2008 F Bobot, S Conchon, E Contejean, M Iguernelala, S Lescuyer, A Mebsout | 54 | 2013 |
Expressing polymorphic types in a many-sorted language F Bobot, A Paskevich International Symposium on Frontiers of Combining Systems, 87-102, 2011 | 49 | 2011 |
Let’s verify this with Why3 F Bobot, JC Filliâtre, C Marché, A Paskevich International Journal on Software Tools for Technology Transfer 17 (6), 709-727, 2015 | 45 | 2015 |
A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic F Bobot, S Conchon, E Contejean, M Iguernelala, A Mahboubi, A Mebsout, ... International Joint Conference on Automated Reasoning, 67-81, 2012 | 29 | 2012 |
Certified complexity (cerco) RM Amadio, N Ayache, F Bobot, JP Boender, B Campbell, I Garnier, ... International Workshop on Foundational and Practical Aspects of Resource …, 2013 | 28 | 2013 |
Preserving user proofs across specification changes F Bobot, JC Filliâtre, C Marché, G Melquiond, A Paskevich Working Conference on Verified Software: Theories, Tools, and Experiments …, 2013 | 20 | 2013 |
The Alt-Ergo automated theorem prover F Bobot, S Conchon, E Contejean, M Iguernelala, S Lescuyer, A Mebsout URL: http://alt-ergo. lri. fr, 2008 | 20 | 2008 |
The why3 platform F Bobot, JC Filliâtre, C Marché, G Melquiond, A Paskevich LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, 2011 | 18 | 2011 |
Separation predicates: a taste of separation logic in first-order logic F Bobot, JC Filliâtre International Conference on Formal Engineering Methods, 167-181, 2012 | 16 | 2012 |
Real behavior of floating point numbers B Marre, F Bobot, Z Chihani | 15 | 2017 |
Deductive proof of ethereum smart contracts using why3 Z Nehai, F Bobot arXiv preprint arXiv:1904.11281, 2019 | 11 | 2019 |
WP plug-in manual P Baudin, F Bobot, L Correnson, Z Dargaye CEA LIST, Software Safety Laboratory, 2016 | 10 | 2016 |
Sharpening constraint programming approaches for bit-vector theory Z Chihani, B Marre, F Bobot, S Bardin International Conference on AI and OR Techniques in Constraint Programming …, 2017 | 9 | 2017 |
The Why3 platform, version 0.72. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.May 2012 F Bobot, JC Filliâtre, C Marché, G Melquiond, A Paskevich | 9 | |
A formally verified floating-point implementation of the compact position reporting algorithm L Titolo, MM Moscato, CA Munoz, A Dutle, F Bobot International Symposium on Formal Methods, 364-381, 2018 | 7 | 2018 |
Frama-c P Baudin, F Bobot, R Bonichon, L Correnson, P Cuoq, Z Dargaye, ... Frama-C 16-Sulfur ed: Informations légales et droit de diffusion, 2007 | 6 | 2007 |
The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.February 2011 F Bobot, JC Filliâtre, C Marché, G Melquiond, A Paskevich | 6 | |
Centralizing equality reasoning in MCSAT F Bobot, S Graham-Lengrand, B Marre, G Bury | 5 | 2018 |