Why3: Shepherd your herd of provers F Bobot, JC Filliâtre, C Marché, A Paskevich Boogie 2011: First International Workshop on Intermediate Verification …, 2011 | 375 | 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 | 70 | 2008 |
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 | 67 | 2015 |
The Alt-Ergo automated theorem prover, 2008 F Bobot, S Conchon, E Contejean, M Iguernelala, S Lescuyer, A Mebsout | 58 | 2013 |
Expressing polymorphic types in a many-sorted language F Bobot, A Paskevich Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011 …, 2011 | 56 | 2011 |
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 | 41 | 2014 |
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 | 36 | 2021 |
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 | 31 | 2021 |
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 | 31 | 2012 |
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 |
Preserving user proofs across specification changes F Bobot, JC Filliâtre, C Marché, G Melquiond, A Paskevich Verified Software: Theories, Tools, Experiments: 5th International …, 2014 | 25 | 2014 |
Deductive proof of industrial smart contracts using Why3 Z Nehai, F Bobot Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7 …, 2020 | 24 | 2020 |
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 | 23 | 2011 |
Real behavior of floating point numbers B Marre, F Bobot, Z Chihani The SMT Workshop, 2017 | 22 | 2017 |
Separation predicates: A taste of separation logic in first-order logic F Bobot, JC Filliâtre Formal Methods and Software Engineering: 14th International Conference on …, 2012 | 17 | 2012 |
WP plug-in manual P Baudin, F Bobot, L Correnson, Z Dargaye, A Blanchard Frama-c. com, 2020 | 15 | 2020 |
Sharpening constraint programming approaches for bit-vector theory Z Chihani, B Marre, F Bobot, S Bardin Integration of AI and OR Techniques in Constraint Programming: 14th …, 2017 | 12 | 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 | 9 | 2021 |
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 | 9 | 2018 |
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 | |