gmalecha/coq-smt-check gmalecha/coq-smt-check

  • Stars
    star
    10
  • Rank 1,807,489 (Top 36 %)
  • Language
    OCaml
  • License
    MIT License
  • Created almost 9 years ago
  • Updated over 4 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
gmalecha/coq-smt-check
github

gmalecha

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Invoke SMT solvers from Coq to check obligations

More Repositories

1

mirror-core

A framework for extensible, reflective decision procedures.
Coq
19
star
2

coq-printf

Implementation of sprintf for Coq
Coq
18
star
3

coq-interaction-trees

Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior.
Coq
17
star
4

coq-ltac-iter

Access hint databases from tactics.
Coq
12
star
5

skip-list

Pure skip lists in Haskell
Haskell
9
star
6

mirror-shard

Reflective verification procedures for separation logic programs in Coq
Coq
8
star
7

coq-extensible-records

Implementation of extensible records in Coq
Coq
6
star
8

coq-plugin-template

Template for Coq plugins
Makefile
5
star
9

bedrock-mirror-shard

Port of Bedrock to use MirrorShard library for computational reflection
Coq
5
star
10

coq-temporal

An implementation of temporal logic in Coq using Charge!
Coq
4
star
11

coq-plugin-utils

Useful utility functions for writing Coq plugins
OCaml
4
star
12

coq-markov

Exploring probabilistic programming in Coq
Coq
4
star
13

coq-k

Some formalization of the K framework in Coq
Coq
2
star
14

coq-simulink

Simulink-like formalism in Coq
Coq
2
star
15

semantic-query

Semantic query optimization
TeX
2
star
16

coq-apply-any

An extension to eauto that allows you to apply an arbitrary lemma from a hint database
OCaml
1
star
17

coq-refinement

Relational refinements in Coq based on the work of Maxime Denes.
Coq
1
star
18

coq-seal

Implementation of sealing in Coq with macros for generation
Coq
1
star
19

coq-mod-reduce

Modular reduction specifications for cbv
OCaml
1
star
20

ppx_rewriter

An OCaml optimizer using ppx extensions
OCaml
1
star
21

categorical-unification

Exploration of unification on categorical terms.
Coq
1
star