GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → lukaszcz → Coqhammer

lukaszcz / Coqhammer

Licence: lgpl-2.1
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

Programming Languages

ocaml
1615 projects

Labels

automationcoqverification

Projects that are alternatives of or similar to Coqhammer

Perennial
Verifying concurrent crash-safe systems
Stars: ✭ 57 (-63.69%)
Mutual labels:  coq, verification
Cosette
Cosette is an automated SQL solver.
Stars: ✭ 533 (+239.49%)
Mutual labels:  coq, verification
vericert
A formally verified high-level synthesis tool based on CompCert and written in Coq.
Stars: ✭ 63 (-59.87%)
Mutual labels:  coq, verification
Ergo
The Language for Smart Legal Contracts
Stars: ✭ 108 (-31.21%)
Mutual labels:  coq, verification
Express Mongodb Rest Api Boilerplate
A boilerplate for Node.js apps / Rest API / Authentication from scratch - express, mongodb (mongoose).
Stars: ✭ 153 (-2.55%)
Mutual labels:  verification
Logic
CMake, SystemVerilog and SystemC utilities for creating, building and testing RTL projects for FPGAs and ASICs.
Stars: ✭ 149 (-5.1%)
Mutual labels:  verification
Easyengine
Command-line control panel for Nginx Server to manage WordPress sites running on Nginx, PHP, MySQL, and Let's Encrypt
Stars: ✭ 1,881 (+1098.09%)
Mutual labels:  automation
Dbgchild
Debug Child Process Tool (auto attach)
Stars: ✭ 145 (-7.64%)
Mutual labels:  automation
Flashsploit
Exploitation Framework for ATtiny85 Based HID Attacks
Stars: ✭ 155 (-1.27%)
Mutual labels:  automation
Securecrt Tools
SecureCRT scripts, written in Python, for doing various tasks when connected to Cisco equipment.
Stars: ✭ 154 (-1.91%)
Mutual labels:  automation
Immudb
immudb - world’s fastest immutable database, built on a zero trust model
Stars: ✭ 3,743 (+2284.08%)
Mutual labels:  verification
Homebridge Wol
A Wake on Lan plugin for Homebridge
Stars: ✭ 150 (-4.46%)
Mutual labels:  automation
Vscode Tlaplus
TLA+ language support for Visual Studio Code
Stars: ✭ 152 (-3.18%)
Mutual labels:  verification
Terrahub
Terraform Automation and Orchestration Tool (Open Source)
Stars: ✭ 148 (-5.73%)
Mutual labels:  automation
Scheduler Card
HA Lovelace card for control of scheduler entities
Stars: ✭ 154 (-1.91%)
Mutual labels:  automation
Keycloak Config Cli
Import YAML/JSON-formatted configuration files into Keycloak - Configuration as Code for Keycloak.
Stars: ✭ 147 (-6.37%)
Mutual labels:  automation
Maintainer
👨‍💻 🐳 Generate personal daily reports or summary, AUTHORS, CONTRIBUTING, CHANGELOG and so on for GitHub user or repository.
Stars: ✭ 152 (-3.18%)
Mutual labels:  automation
Qxf2 Page Object Model
Write Selenium and Appium tests in Python using the Page Object pattern. This Pythonic GUI and API test automation framework will help you get started with QA automation quickly. It comes with many useful integrations like - email, BrowserStack, Slack, TestRail, etc. This repository is developed and maintained by Qxf2 Services (https://qxf2.com).
Stars: ✭ 155 (-1.27%)
Mutual labels:  automation
Hyperkernel
Stars: ✭ 152 (-3.18%)
Mutual labels:  verification
Smarthome Homeassistant Config
🏠 My Home Assistant configuration. This repo will be archived 🗄️ in the future
Stars: ✭ 152 (-3.18%)
Mutual labels:  automation
View All Similar Projects ➔

CoqHammer (dev) for Coq 8.13

Travis

CoqHammer video tutorial: part 1 (sauto), part 2 (hammer).

Since version 1.3, the CoqHammer system consists of two major separate components.

  1. The sauto general proof search tactic for the Calculus of Inductive Construction.

  2. The hammer automated reasoning tool which combines learning from previous proofs with the translation of problems to the logics of external automated systems and the reconstruction of successfully found proofs with the sauto procedure.

See the CoqHammer webpage for documentation and installation instructions.

Requirements

Copyright and license

Copyright (c) 2017-2021, Lukasz Czajka, TU Dortmund University.
Copyright (c) 2017-2018, Cezary Kaliszyk, University of Innsbruck.

Distributed under the terms of LGPL 2.1, see the file LICENSE.

See CREDITS for a full list of contributors.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].