• Coq

  • Referenced in 1898 articles [sw00161]
  • proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification...
  • CeTA

  • Referenced in 47 articles [sw06584]
  • Certification of termination proofs using CeTA. There are many automatic tools to prove termination...
  • KRAKATOA

  • Referenced in 89 articles [sw03159]
  • applets certification. It involves three distinct components: the WHY tool, which computes proof obligations...
  • SMTCoq

  • Referenced in 7 articles [sw32310]
  • checker for generic first-order proof certificates fully implemented and proved correct in Coq, SMTCoq ... safe way. The current version supports proof certificates produced by the SAT solver ZChaff...
  • Zenon

  • Referenced in 23 articles [sw06753]
  • environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml ... code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which...
  • CoLoR

  • Referenced in 38 articles [sw09806]
  • application to the automated verifications of termination certificates. Termination is an important property of programs ... notably required for programs formulated in proof assistants. It is a very active subject ... proof assistant Coq. We also present its application to the automated verification of termination certificates...
  • dReal

  • Referenced in 34 articles [sw07157]
  • certificates of correctness for both δ -sat (a solution) and unsat answers (a proof...
  • cake_lpr

  • Referenced in 2 articles [sw41080]
  • solvers can emit independently checkable proof certificates to validate their results. The state ... proof system that allows for compact proof certificates is propagation redundancy (PR). However, the only...
  • DSDP5

  • Referenced in 30 articles [sw04411]
  • semidefinite programming. Its features include a convergence proof with polynomially bounded worst-case complexity, primal ... dual feasible solutions when they exist, certificates of infeasibility when solutions do not exist, initial...
  • IsaFoR

  • Referenced in 6 articles [sw10106]
  • link to the external prover includes full proof reconstruction, where all necessary properties are derived ... without oracles. Apart from the certification of the imported proof, the main challenge...
  • AutoBayes/CC

  • Referenced in 4 articles [sw01806]
  • with automatic code certification -- system description. Code certification is a lightweight approach to formally demonstrate ... require code producers to provide formal proofs that their code ... satisfies these quality properties. The proofs serve as certificates which can be checked independently ... certification authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying...
  • PRECiSA

  • Referenced in 2 articles [sw38041]
  • prototype tool PRECiSA that generates formal proof certificates stating the correctness of the computed round...
  • Synthia

  • Referenced in 8 articles [sw12933]
  • user. Such certificates are easy-to-validate deductive proofs that only reflect the specification-critical...
  • MadMax

  • Referenced in 2 articles [sw28631]
  • ground completeness checks and supports certification of its proofs by an Isabelle-based certifier...
  • ibexMop

  • Referenced in 2 articles [sw34657]
  • performance make them useful when proofs of infeasibility and/or certification of solutions are a must...
  • NLCertify

  • Referenced in 4 articles [sw08786]
  • certificates for f over K, which can be ultimately proved correct inside the Coq proof ... develop adaptive techniques to produce certificates with a reduced complexity. The software first builds...
  • Pratt_Certificate

  • Referenced in 1 article [sw38039]
  • Certificate: Pratt’s Primality Certificates. In 1975, Pratt introduced a proof system for certifying primes ... number p is prime iff a primality certificate for p exists. By showing a logarithmic ... upper bound on the length of the certificates in size of the prime number ... proof system as well as an upper bound for the size of the certificate...
  • CoqJVM

  • Referenced in 4 articles [sw02002]
  • proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification...