39 citations · 82 across the 9 of their papers we have counts for
10 papers
First-Order Quantification over Automata
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Deciding formulas mixing arithmetic and uninterpreted predicates is of practical interest, notably for applications in verification. Some decision procedures consist in building by…
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted predicates are often undecidable, as is, for instance, Presburger arithmetic extended with a single un…
Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications
Daniele Nantes-Sobrinho, Pascal Fontaine
This volume contains the post-proceedings of the Seventeenth Logical and Semantic Frameworks with Applications (LSFA 2022), organised by the Universidade Federal de Minas Gerais, B…
Alethe: Towards a Generic SMT Proof Format (extended abstract)
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa +1
The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are use…
Fair and Adventurous Enumeration of Quantifier Instantiations
Mikoláš Janota, Haniel Barbosa, Pascal Fontaine +1
SMT solvers generally tackle quantifiers by instantiating their variables with tuples of terms from the ground part of the formula. Recent enumerative approaches for quantifier ins…
Politeness for the Theory of Algebraic Datatypes
Ying Sheng, Yoni Zohar, Christophe Ringeissen +3
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable versi…