• DRAT-trim

  • Referenced in 37 articles [sw13313]
  • DRAT-trim: efficient checking and trimming using expressive clausal proofs. The DRAT-trim tool ... satisfiability proof checker based on the new DRAT proof format. Unlike its predecessor, DRUP-trim ... preprocessing techniques can be validated using DRAT-trim. Checking time of a proof is comparable ... hurdle of resolution-based proof checkers. The DRAT-trim tool can emit trimmed formulas, optimized...
  • GRAT

  • Referenced in 5 articles [sw21969]
  • highly optimized gratgen tool converts a DRAT certificate to a GRAT certificate, which is then ... faster than the unverified standard tool drat-trim, and significantly faster than the formally verified...
  • drat

  • Referenced in 1 article [sw16285]
  • package drat. Creation and use of R Repositories via helper functions to insert packages into ... same machine or a local network. Drat is a recursive acronym: Drat R Archive Template...
  • Coq

  • Referenced in 1890 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 713 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Chaff

  • Referenced in 586 articles [sw06916]
  • Chaff:engineering an efficient SAT solver. Boolean Satisfiability...
  • LCF

  • Referenced in 158 articles [sw08360]
  • Edinburgh LCF. A mechanized logic of computation. From...
  • versat

  • Referenced in 10 articles [sw08417]
  • versat: A verified modern SAT solver. This paper...
  • CakeML

  • Referenced in 53 articles [sw08799]
  • Cakeml, a verified implementation of ML. We have...
  • Autoref

  • Referenced in 15 articles [sw12809]
  • Automatic data refinement. We present the Autoref tool...
  • GitHub

  • Referenced in 2766 articles [sw23170]
  • GitHub (originally known as Logical Awesome LLC)[3...
  • Gabow SCC

  • Referenced in 8 articles [sw28915]
  • Verified Efficient Implementation of Gabow’s Strongly Connected...