
CeTA
 Referenced in 47 articles
[sw06584]
 generate a highly efficient and certified Haskell program, CeTA, which can be used to certify...

Mathemagix
 Referenced in 43 articles
[sw00553]
 Mathemagix: Towards large scale programming for symbolic and certified numeric computations. Coordinated by Joris ... design of a scientific programming language for symbolic and certified numeric algorithms. This language...

alphaCertified
 Referenced in 50 articles
[sw07351]
 convergence of Newton’s method to certify that Newton iterations will converge quadratically to solutions ... system. The program alphaCertified implements algorithms based on αtheory to certify solutions of polynomial...

FoCaLiZe
 Referenced in 10 articles
[sw12384]
 providing a programming environment to develop certified programs. The environment is based on a functional...

CiaoPP
 Referenced in 45 articles
[sw12089]
 program inferred by the analyzers is used in the system to certify that an untrusted...

Fiat
 Referenced in 14 articles
[sw21357]
 libraries of specification languages for describing common programming tasks like querying a relational database. These ... produces a formal proof trail certifying that the synthesized program meets the original specification. Code...

TemplateCoq
 Referenced in 4 articles
[sw27569]
 Towards certified metaprogramming with typed TemplateCoq. TemplateCoq (url{https://templatecoq.github.io/templatecoq}) ... Recently, it was used in the CertiCoq certified compiler project [4], as its front...

jsCoq
 Referenced in 1 article
[sw40703]
 books such as Software Foundations or Certified Programming with Dependent Types. The new target platform...

ROSCoq
 Referenced in 2 articles
[sw13285]
 present ROSCoq, a framework for developing certified Coq programs for robots. ROSCoq subsystems communicate using...

A3PAT
 Referenced in 8 articles
[sw21587]
 approach for certified automated termination proofs. Software engineering, automated reasoning, rulebased programming or specifications ... Project A3PAT to discover and moreover certify, with full automation, termination proofs for term rewriting...

Gappa
 Referenced in 19 articles
[sw04885]
 verifying and formally proving properties on numerical programs dealing with floatingpoint or fixedpoint ... CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended...

GCminor
 Referenced in 4 articles
[sw22622]
 machinecertified framework for correct compilation and execution of programs in garbagecollected languages...

RealCertify
 Referenced in 7 articles
[sw28191]
 RealCertify: a Maple package for certifying nonnegativity. Let Q (resp. R) be the field ... numerous problems coming from engineering sciences, program verification and cyberphysical systems. It is based...

IMP+Exc
 Referenced in 1 article
[sw28535]
 allows us to prove equivalences between programs written in IMP+Exc. The combined logic ... this encoding is used to certify some program equivalence proofs...

CertiCrypt
 Referenced in 6 articles
[sw09443]
 Programming language techniques for cryptographic proofs. CertiCrypt is a general framework to certify the security ... proved, are expressed using probabilistic programs. It provides a set of programming language tools (observational...

versat
 Referenced in 10 articles
[sw08417]
 proofs are written in Guru, a verifiedprogramming language. We compare versat to a state ... solver that produces certified “unsat” answers. We also show through an empirical evaluation that versat...

omniORB
 Referenced in 8 articles
[sw23761]
 means that omniORB has been tested and certified CORBA compliant, to version ... find out more about the branding program at the Open Group...

Jakarta
 Referenced in 18 articles
[sw01269]
 specifications; the JaKarTa Transformation Kit (JTK), a program to manipulate and transform JSL specifications ... Goal of the work is to derive certified Byte Code Verifiers by abstraction from...

Omega++
 Referenced in 1 article
[sw32372]
 Certified reasoning with infinity. We demonstrate how infinities improve the expressivity, power, readability, conciseness ... compositionality of a program logic. We prove that adding infinities to Presburger arithmetic enables these ... certified decision procedure for Presburger arithmetic with infinity and benchmark its performance. Both the program...

ComplexityParser
 Referenced in 1 article
[sw42399]
 automatic tool for certifying polytime complexity of Java programs. ComplexityParser is a static complexity...