11 search results for "tag:"category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures""

Showing 1 - 11
  1. coq-aac-tactics

    No documentation

    Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:reflexive tactic keyword:rewriting keyword:rewriting modulo associativity and commutativity keyword:rewriting modulo ac keyword:decision procedure logpath:AAC_tactics date:2024-06-27
    Thomas Braibant Damien Pous Fabian Kunze
    8.20.0
    LGPL-3.0-or-later
    Used by 2 other packages
    06 Sep 2024
  2. coq-atbr

    No documentation

    Coq library and tactic for deciding Kleene algebras
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:Kleene algebra keyword:finite automata keyword:semiring keyword:matrices keyword:decision procedure keyword:reflexive tactic logpath:ATBR date:2024-06-30
    Thomas Braibant Damien Pous
    8.20.0
    LGPL-3.0-or-later
    Used by 0 other packages
    06 Sep 2024
  3. coq-gappa

    No documentation

    A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
    keyword:floating-point arithmetic keyword:interval arithmetic keyword:decision procedure category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Gappa date:2024-02-08
    Guillaume Melquiond <guillaume.melquiond@inria.fr>
    1.5.5
    LGPL-3.0-or-later
    Used by 0 other packages
    08 Feb 2024
  4. coq-interval

    No documentation

    A Coq tactic for proving bounds on real-valued expressions automatically
    keyword:interval arithmetic keyword:decision procedure keyword:floating-point arithmetic keyword:reflexive tactic keyword:Taylor models category:Mathematics/Real Calculus and Topology category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Interval date:2024-10-21
    Guillaume Melquiond <guillaume.melquiond@inria.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr> Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>
    4.11.1
    CeCILL-C
    Used by 7 other packages
    22 Oct 2024
  5. coq-itauto

    No documentation

    Reflexive SAT solver with Nelson-Oppen support, parameterised by a leaf tactic inside Coq
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:integers keyword:SAT keyword:SMT keyword:Nelson-Oppen keyword:automation logpath:Cdcl date:2024-06-17
    Frédéric Besson
    8.20.0
    MIT
    Used by 1 other packages
    06 Sep 2024
  6. coq-smtcoq

    No documentation

    A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword: SMT keyword: SAT keyword: automation logpath:SMTCoq
    Michaël Armand Valentin Blot Amina Bousalem Boris Djalal Louise Dubois de Prisque et al.
    2.3+8.20
    CECILL-C
    Used by 1 other packages
    19 Sep 2024
  7. coq-sniper

    No documentation

    A Coq plugin for general proof automation
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword: SMT keyword: automation logpath:Sniper
    Valentin Blot <Valentin.Blot@inria.fr> Louise Dubois de Prisque <Louise.Dubois-de-Prisque@inria.fr> Chantal Keller <ckeller@lmf.cnrs.fr Pierre Vial <Pierre.Vial@inria.fr>
    1.1+8.16
    CECILL-C
    Used by 0 other packages
    16 Jun 2023
  8. coq-stalmarck

    No documentation

    Verified implementation of Stålmarck's algorithm for proving tautologies in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:boolean formula keyword:tautology checker logpath:Stalmarck.Algorithm date:2024-06-30
    Pierre Letouzey Laurent Théry
    8.20.0
    LGPL-2.1-or-later
    Used by 1 other packages
    06 Sep 2024
  9. coq-trakt

    No documentation

    A generic goal preprocessing tool for proof automation tactics in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi date:2022-05-16 logpath:Trakt
    Enzo Crance
    1.2c
    LGPL-3.0-or-later
    Used by 0 other packages
    19 Jun 2024
  10. coq-vcfloat

    No documentation

    VCFloat: Floating Point Round-off Error Analysis
    date:2024-03-20 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat
    Andrew W. Appel Ariel E. Kellison Tahina Ramananandro Paul Mountcastle Benoit Meister et al.
    2.2
    LGPL-3.0-or-later
    Used by 1 other packages
    21 Mar 2024
  11. coq-vst-lib

    No documentation

    VSTlib: VST-verified C library for VST-verified clients
    date:2024-03-20 keyword:VST keyword:library keyword:malloc keyword:threads keyword:floating-point arithmetic category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VSTlib
    Andrew W. Appel William Mansky
    2.14
    BSD-2-Clause
    Used by 0 other packages
    21 Mar 2024