Coming to terms with quantified reasoning L Kovács, S Robillard, A Voronkov Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming …, 2017 | 43 | 2017 |

A comprehensive framework for saturation theorem proving U Waldmann, S Tourret, S Robillard, J Blanchette International Joint Conference on Automated Reasoning, 316-334, 2020 | 20 | 2020 |

Superposition with Datatypes and Codatatypes JC Blanchette, N Peltier, S Robillard Technical report, 2018 | 15 | 2018 |

Vampire A Voronkov, L Kovács, G Reger, M Suda, E Kotelnikov, S Robillard, ... | 14 | 2018 |

Formal derivation and extraction of a parallel program for the all nearest smaller values problem F Loulergue, S Robillard, J Tesson, J Legaux, Z Hu Proceedings of the 29th Annual ACM Symposium on Applied Computing, 1577-1584, 2014 | 9 | 2014 |

Loop Analysis by Quantification over Iterations. B Gleiss, L Kovács, S Robillard LPAR, 381-399, 2018 | 8 | 2018 |

Reasoning about loops using vampire in key W Ahrendt, L Kovács, S Robillard Logic for Programming, Artificial Intelligence, and Reasoning, 434-443, 2015 | 8 | 2015 |

Powerlists in Coq: programming and reasoning F Loulergue, V Niculescu, S Robillard 2013 First International Symposium on Computing and Networking, 57-65, 2013 | 7 | 2013 |

A comprehensive framework for saturation theorem proving (technical report) U Waldmann, S Tourret, S Robillard, J Blanchette Technical report, 2020 | 5 | 2020 |

Toward safe and efficient reconfiguration with Concerto M Chardet, H Coullon, S Robillard Science of Computer Programming 203, 102582, 2021 | 4 | 2021 |

Verified approximation algorithms R Eßmann, T Nipkow, S Robillard International Joint Conference on Automated Reasoning, 291-306, 2020 | 3 | 2020 |

Theory-Specific Reasoning about Loops with Arrays using Vampire. YT Chen, L Kovács, S Robillard Vampire@ IJCAR, 16-32, 2016 | 3 | 2016 |

Reasoning About Loops Using Vampire. L Kovács, S Robillard Vampire Workshop, 52-62, 2015 | 3 | 2015 |

Enhancing Separation of Concerns, Parallelism, and Formalism in Distributed Software Deployment with Madeus M Chardet, H Coullon, C Pérez, D Pertin, C Servantie, S Robillard | 2 | 2020 |

An inference rule for the acyclicity property of term algebras S Robillard Vampire, 2017 | 2 | 2017 |

Deductive Program Analysis with First-Order Theorem Provers S Robillard Department of Computer Science and Engineering, Chalmers University of …, 2019 | | 2019 |

Analysis of Iterative or Recursive Programs Using a First-Order Theorem Prover S Robillard PQDT-Global, 2016 | | 2016 |

Catamorphism generation and fusion using Coq S Robillard 2014 16th International Symposium on Symbolic and Numeric Algorithms for …, 2014 | | 2014 |

CALCULATING PARALLEL PROGRAMS IN COQ WITH BSP AND LIST HOMOMORPHISMS F Loulergue, WBZHJ Tesson, J Légaux, S Robillard | | 2014 |

PARALLEL PROGRAM DEVELOPMENT WITH POWERLISTS FLVNJ Tesson, S Robillard | | 2014 |