François Bobot

Most-cited papers

Why3: Shepherd Your Herd of Provers
François Bobot, J. Filliâtre, C. Marché, A. Paskevich
2011317 citations
Semantic Scholar
An Automated Deductive Verification Framework for Circuit-building Quantum Programs
Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle +1 more
2020European Symposium on Programming88 citations Open access
Semantic Scholar
Let’s verify this with Why3
François Bobot, J. Filliâtre, C. Marché, A. Paskevich
2014International Journal on Software Tools for Technology Transfer (STTT)80 citations Open access
Semantic Scholar
The dogged pursuit of bug-free C programs
P. Baudin, François Bobot, David Bühler, Loïc Correnson +7 more
2021Communications of the ACM61 citations Open access
Semantic Scholar
Implementing polymorphism in SMT solvers
François Bobot, Sylvain Conchon, Évelyne Contejean, Stéphane Lescuyer
2008SMT '08/BPR '0860 citations Open access
Semantic Scholar
Expressing Polymorphic Types in a Many-Sorted Language
François Bobot, A. Paskevich
2011International Symposium on Frontiers of Combining Systems46 citations
Semantic Scholar
Certified Complexity (CerCo)
R. Amadio, N. Ayache, François Bobot, J. Boender +11 more
2013International Workshop on Foundational and Practical Aspects of Resource Analysis32 citations Open access
Semantic Scholar
Deductive Proof of Industrial Smart Contracts Using Why3
Zeinab Nehaï, François Bobot
2019FM Workshops24 citations
Semantic Scholar
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala +3 more
2012International Joint Conference on Automated Reasoning21 citations Open access
Semantic Scholar
Formal analysis of the compact position reporting algorithm
Aaron Dutle, Mariano M. Moscato, Laura Titolo, C. Muñoz +2 more
2020Formal Aspects of Computing18 citations Open access
Semantic Scholar
Preserving User Proofs across Specification Changes
François Bobot, J. Filliâtre, C. Marché, G. Melquiond +1 more
2013Verified Software: Theories, Tools, Experiments17 citations Open access
Semantic Scholar
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
Laura Titolo, Mariano M. Moscato, C. Muñoz, Aaron Dutle +1 more
2018World Congress on Formal Methods15 citations Open access
Semantic Scholar
Separation Predicates: A Taste of Separation Logic in First-Order Logic
François Bobot, J. Filliâtre
2012IEEE International Conference on Formal Engineering Methods15 citations Open access
Semantic Scholar
Sharpening Constraint Programming Approaches for Bit-Vector Theory
Zakaria Chihani, B. Marre, François Bobot, Sébastien Bardin
2017Integration of AI and OR Techniques in Constraint Programming11 citations Open access
Semantic Scholar
A TLA+ Formal Proof of a Cross-Chain Swap
Zeinab Nehaï, François Bobot, S. Tucci-Piergiovanni, C. Delporte-Gallet +1 more
2022International Conference of Distributed Computing and Networking10 citations Open access
Semantic Scholar
Toward certified quantum programming
Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle +1 more
2018arXiv.org9 citations
Semantic Scholar
Preserving User Proofs Across Speci cation Changes ?
François Bobot, J. Filliâtre, C. Marché, G. Melquiond +1 more
20139 citations
Semantic Scholar
Verifying Models with Dolmen
Guillaume Bury, François Bobot
2023International Workshop on Satisfiability Modulo Theories7 citations
Semantic Scholar
Centralizing equality reasoning in MCSAT
François Bobot, Stéphane Graham-Lengrand, B. Marre, Guillaume Bury
20186 citations
Semantic Scholar
Real Behavior of Floating Point
François Bobot, Zakaria Chihani, B. Marre
2017International Workshop on Satisfiability Modulo Theories6 citations
Semantic Scholar
CDCL-inspired Word-level Learning for Bit-vector Constraint Solving
Zakaria Chihani, François Bobot, Sébastien Bardin
2017arXiv.org5 citations
Semantic Scholar
The Why3 platform 0.81
François Bobot, J. Filliâtre, C. Marché, G. Melquiond +1 more
20135 citations
Semantic Scholar
Exploiting Pointer Analysis in Memory Models for Deductive Verification
Quentin Bouillaguet, François Bobot, M. Sighireanu, Boris Yakobowski
2018International Conference on Verification, Model Checking and Abstract Interpretation2 citations
Semantic Scholar
A Value-based Memory Model for Deductive Verification
Quentin Bouillaguet, François Bobot, M. Sighireanu, Boris Yakobowski
20170 citations
Semantic Scholar
CP meets SMT
François Bobot, Sébastien Bardin, B. Marre
20140 citations
Semantic Scholar
Scientific Foundations - Proof of Imperative andObject-Oriented programs
Romain Bardou, François Bobot, S. Boldo, J. Filliâtre +6 more
20110 citations
Semantic Scholar
Software - The Why platform
J. Filliâtre, Romain Bardou, François Bobot, C. Marché +2 more
20100 citations
Semantic Scholar
Other Grants and Activities - European initiatives
C. Marché, Romain Bardou, François Bobot, Asma Tafat
20100 citations
Semantic Scholar