Category: Decision Procedures and Certified Algorithms

Correctness proofs based on external tools

• Bertrand: Correctness of Knuth's algorithm for prime numbers
  Laurent Théry

Correctness proofs of algorithms

• AILS: Proof of AILS algorithm
  Olivier Desmettre
• Additions: Addition Chains
  Pierre Castéran
• FOUnify: Correctness and extraction of the unification algorithm
  Jocelyne Rouyer
• Huffman: A correctness proof of Huffman algorithm
  Laurent Théry
• PersistentUnionFind: Persistent Union Find
  Jean-Christophe Filliâtre
• QuicksortComplexity: Proofs of Quicksort's worst- and average-case complexity
  Eelis
• RSA: Correctness of RSA algorithm
  Jose C. Almeida, Laurent Théry
• Random: Interpretation of random programs
  Christine Paulin
• TortoiseHareAlgorithm: Tortoise and the hare algorithm
  Jean-Christophe Filliâtre
• TreeDiameter: Diameter of a binary tree
  Jean-Christophe Filliâtre

Decision procedures

• ATBR: A tactic for deciding Kleene algebras
  Damien Pous, Thomas Braibant
• BDDs: BDD algorithms and proofs in Coq, by reflection
  Kumar Neeraj Verma
• CanonBDDs: Canonicity of Binary Decision Dags
  Emmanuel Ledinot
• Ergo: Ergo: a Coq plugin for reification of term with arbitrary signature
  Stéphane Lescuyer
• Graphs: Satisfiability of inequality constraints and detection of cycles with negative weight in graphs
  Jean Goubault
• IPC: Intuitionistic Propositional Checker
  Klaus Weich
• Presburger: Presburger's algorithm
  Laurent Théry
• SMC: BDD based symbolic model checker for the modal mu-calculus
  Kumar Neeraj Verma
• Stalmarck: Proof of Stalmarck's algorithm
  Laurent Théry, Pierre Letouzey