Why3: Shepherd your herd of provers F Bobot, JC Filliâtre, C Marché, A Paskevich Boogie 2011: First International Workshop on Intermediate Verification …, 2011 | 385 | 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, 709-727, 2015 | 73 | 2015 |

Implementing polymorphism in SMT solvers F Bobot, S Conchon, É Contejean, S Lescuyer Proceedings of the Joint Workshops of the 6th International Workshop on …, 2008 | 70 | 2008 |

The dogged pursuit of bug-free C programs: the Frama-C software analysis platform P Baudin, F Bobot, D Bühler, L Correnson, F Kirchner, N Kosmatov, ... Communications of the ACM 64 (8), 56-68, 2021 | 62 | 2021 |

The Alt-Ergo automated theorem prover, 2008 F Bobot, S Conchon, E Contejean, M Iguernelala, S Lescuyer, A Mebsout | 61 | 2013 |

Expressing polymorphic types in a many-sorted language F Bobot, A Paskevich International Symposium on Frontiers of Combining Systems, 87-102, 2011 | 56 | 2011 |

An automated deductive verification framework for circuit-building quantum programs C Chareton, S Bardin, F Bobot, V Perrelle, B Valiron Programming Languages and Systems: 30th European Symposium on Programming …, 2021 | 48 | 2021 |

Certified complexity (cerco) RM Amadio, N Ayache, F Bobot, JP Boender, B Campbell, I Garnier, ... Foundational and Practical Aspects of Resource Analysis: Third International …, 2014 | 46 | 2014 |

A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic F Bobot, S Conchon, E Contejean, M Iguernelala, A Mahboubi, A Mebsout, ... Automated Reasoning: 6th International Joint Conference, IJCAR 2012 …, 2012 | 32 | 2012 |

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 2, 2011 | 27 | 2011 |

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 | 26 | 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 | 26 | 2008 |

Real behavior of floating point numbers B Marre, F Bobot, Z Chihani The SMT Workshop, 2017 | 23 | 2017 |

Formal analysis of the compact position reporting algorithm A Dutle, M Moscato, L Titolo, C Munoz, G Anderson, F Bobot Formal Aspects of Computing 33, 65-86, 2021 | 19 | 2021 |

Deductive proof of ethereum smart contracts using why3 Z Nehai, F Bobot arXiv preprint arXiv:1904.11281, 2019 | 19 | 2019 |

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 | 19 | 2012 |

WP plug-in manual P Baudin, F Bobot, L Correnson, Z Dargaye, A Blanchard Frama-c. com, 2020 | 17 | 2020 |

A formally verified floating-point implementation of the compact position reporting algorithm L Titolo, MM Moscato, CA Munoz, A Dutle, F Bobot Formal Methods: 22nd International Symposium, FM 2018, Held as Part of the …, 2018 | 14 | 2018 |

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 | 12 | 2017 |

Deductive proof of industrial smart contracts using Why3 Z Nehaï, F Bobot Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7 …, 2020 | 10 | 2020 |