
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 firstorder 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 objectoriented 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 worstcase 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 proofcarrying...

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 easytovalidate deductive proofs that only reflect the specificationcritical...

MadMax
 Referenced in 2 articles
[sw28631]
 ground completeness checks and supports certification of its proofs by an Isabellebased 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...