Boigelot, B., Fontaine, P., & Vergain, B. (2024). Non-emptiness Test for Automata over Words Indexed by the Reals and Rationals. In S. Z. Fazekas (Ed.), Implementation and Application of Automata - 28th International Conference, CIAA 2024, Proceedings. Springer Science and Business Media Deutschland GmbH. doi:10.1007/978-3-031-71112-1_7 |
Boigelot, B., Fontaine, P., & Vergain, B. (2023). Universal First-Order Quantification over Automata. In Implementation and Application of Automata (pp. 12). Springer Nature Switzerland. doi:10.1007/978-3-031-40247-0_6 |
Vergain, B., Fontaine, P., & Boigelot, B. (01 September 2023). Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. Lecture Notes in Computer Science, 14132, 542-559. doi:10.1007/978-3-031-38499-8 |
Boigelot, B., Fontaine, P., & Vergain, B. (19 August 2023). Decidability of difference logics with unary predicates. CEUR Workshop Proceedings, 3458, 25-36. |
Steen, A., Sutcliffe, G., Fontaine, P., & McKeown, J. (2023). Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic. EPiC Series in Computing, 94, 369 - 385. doi:10.29007/1rhx |
Vergain, B., Boigelot, B., & Fontaine, P. (14 November 2022). Deciding Satisfiability for Fragments with Unary Predicates and Difference Arithmetic. CEUR Workshop Proceedings, 3273. |
Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., & Barrett, C. (August 2022). Polite Combination of Algebraic Datatypes. Journal of Automated Reasoning, 66 (3), 331 - 355. doi:10.1007/s10817-022-09625-3 |
Fontaine, P., & Schurr, H.-J. (2021). Quantifier Simplification by Unification in SMT. In Frontiers of Combining Systems (FroCoS) (pp. 232-249). Springer. doi:10.1007/978-3-030-86205-3_13 |
Janota, M., Barbosa, H., Fontaine, P., & Reynolds, A. (2021). Fair and Adventurous Enumeration of Quantifier Instantiations. In Formal Methods in Computer Aided Design (FMCAD) (pp. 256-260). IEEE. doi:10.34727/2021/isbn.978-3-85448-046-4_35 |
Schurr, H.-J., Fleury, M., Barbosa, H., & Fontaine, P. (2021). Alethe: Towards a Generic SMT Proof Format (extended abstract). In Workshop on Proof eXchange for Theorem Proving (PxTP) (pp. 49-54). doi:10.4204/EPTCS.336.6 |
Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., & Barrett, C. W. (2021). Politeness for the Theory of Algebraic Datatypes (Extended Abstract). In International Joint Conference on Artificial Intelligence (IJCAI) (pp. 4829-4833). ijcai.org. doi:10.24963/ijcai.2021/660 |
Barbosa, H., Blanchette, J. C., Fleury, M., & Fontaine, P. (2020). Scalable Fine-Grained Proofs for Formula Processing. Journal of Automated Reasoning, 64 (3), 485-510. doi:10.1007/s10817-018-09502-y |
Chocron, P., Fontaine, P., & Ringeissen, C. (2020). Politeness and Combination Methods for Theories with Bridging Functions. Journal of Automated Reasoning, 64 (1), 97-134. doi:10.1007/s10817-019-09512-4 |
Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., & Barrett, C. W. (2020). Politeness for the Theory of Algebraic Datatypes. In N. Peltier & V. Sofronie-Stokkermans (Eds.), Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I (pp. 238-255). Springer. doi:10.1007/978-3-030-51074-9_14 |
Tourret, S., Fontaine, P., El Ouraoui, D., & Barbosa, H. (2020). Lifting Congruence Closure with Free Variables to Encoding. In Satisfiability Modulo Theories (pp. 3-14). CEUR-WS.org. |
Bonacina, M. P., Fontaine, P., Ringeissen, C., & Tinelli, C. (2019). Theory Combination: Beyond Equality Sharing. In C. Lutz, U. Sattler, C. Tinelli, A.-Y. Turhan, ... F. Wolter, Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday (pp. 57-89). Springer. doi:10.1007/978-3-030-22102-7_3 |
Fontaine, P. (2019). Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. Lecture Notes in Computer Science, 11716. doi:10.1007/978-3-030-29436-6 |