Proofs and algorithms seminar: Adel Bouhoula on Thursday 10 July 2025 at 15h00, "Three Decades Advancing Automated Induction: From Test Sets to Constrained Tree Grammars and Primal Grammar Schematization"

===== Seminar of the proofs and algorithms pole =====

Hello everybody,

For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Adel Bouhoula (Arabian Gulf University and Invited Professor Polytechnique), invited by the Alco team.

***** Thursday 10 July 2025 at 15h00, room Henri Poincaré *****

Adel Bouhoula -- Three Decades Advancing Automated Induction: From Test Sets to Constrained Tree Grammars and Primal Grammar Schematization

"Designing reliable critical systems requires rigorous verification, where errors can yield severe consequences in safety-critical sectors. This highlights the need for automated reasoning techniques, such as inductive theorem proving, that can handle infinite state spaces and complex data structures with mathematical soundness. This talk presents an overview of over three decades of research on advancing inductive reasoning in computer science. It starts with the test set induction technique, which automatically proves (and disproves) inductive properties. Unlike classical proof by induction techniques, this method needs no completion and explicit induction. However, it retains their positive features, namely, the completeness of the former and the robustness of the latter. Test set induction became the basis for a series of generalizations: first to associative-commutative theories, then to non-free constructors through the introduction of cover sorts, and later to membership equational logic, an extension of order-sorted equational logic and partial algebras that supports both equations and sort membership assertions, expressed as Horn clauses. A key limitation of the latest methods is that constructor axioms must be linear and unconstrained. We address this restriction by using tree grammars with constraints which can be used in the inductive proofs first as an induction scheme for the generation of subgoals at induction steps, second for checking validity and redundancy criteria by reduction to an emptiness problem, and third for defining and solving membership constraints. This technique enables induction on complex data structures like sets, trees, power lists, and sorted lists. However, the inductive proof process still faces two significant challenges; it is undecidable and can diverge even on small examples, leading to failures in the proving experience. Previous methods have proposed ad-hoc heuristics to speculate on additional lemmas that hopefully stop the divergence. Although these methods have succeeded in proving some interesting theorems, they have significant limitations; in particular, they often fail to discover appropriate lemmas, and the lemmas they provide may not be valid. This talk also presents our recent method that performs inductive proofs in conditional theories by automatically detecting divergence in proof traces and deriving a primal grammar as well as new lemmas that schematize the divergent sequences and, thus, allow breaking the divergence and ending the proof. Our method can be integrated with existing automated and interactive inductive proof systems to enhance their performances. Moreover, it has the potential to substantially reduce the time needed for the verification of critical systems. Finally, this talk will illustrate how automated inductive reasoning enables both the detection of attacks and the inductive proof of their absence for security protocols operating in insecure communication environments."


The following seminar will be on Wednesday 09 July 2025 at 10h30 by Patrick Massot: Formalisation de topologie différentielle avec Lean.

The list of upcoming seminars can be found at:
https://www.lix.polytechnique.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at:
https://www.lix.polytechnique.fr/proofs-algorithms/seminar/calendar.ics

To unsubscribe from this mailing list visit:
https://sympa.lix.polytechnique.fr/lists/signoff/proofs-algorithms-seminar