• 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...
  • Template-Coq

  • Referenced in 4 articles [sw27569]
  • Towards certified meta-programming with typed Template-Coq. Template-Coq (url{https://template-coq.github.io/template-coq}) ... 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, rule-based 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 floating-point or fixed-point ... CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended...
  • GCminor

  • Referenced in 4 articles [sw22622]
  • machine-certified framework for correct compilation and execution of programs in garbage-collected languages...
  • RealCertify

  • Referenced in 7 articles [sw28191]
  • RealCertify: a Maple package for certifying non-negativity. Let Q (resp. R) be the field ... numerous problems coming from engineering sciences, program verification and cyber-physical 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 verified-programming 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 poly-time complexity of Java programs. ComplexityParser is a static complexity...