• VeriStar

  • Referenced in 3 articles [sw09393]
  • proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully machine-checked ... tightly integrated collection of machine-verified program logics and compilers giving foundational correctness guarantees.par VeriStar ... implemented in Gallina, the pure functional programming language embedded in the Coq theorem prover ... theorem prover says a C minor program is safe, the program will be compiled...
  • Libra

  • Referenced in 7 articles [sw41699]
  • time is O(C) irrespective of the circuit type; (ii) the proof size and verification ... space uniform circuits (such as RAM programs). In addition Libra features an one-time trusted...
  • Geppetto

  • Referenced in 10 articles [sw31791]
  • cryptographic primitives, Geppetto’s instantiation of bounded proof bootstrapping improves on prior bootstrapped systems ... costs more in line with the program’s actual (rather than worst-case) execution time ... code generated from a variety of source C programs and cryptographic libraries...
  • RedHom

  • Referenced in 12 articles [sw08776]
  • homology. The library is based on C++ templates. This allows us to have one efficient ... programs as well as programmers who need to use homology algorithms in their own programs ... constitutes a part of CAPD (Computer Assisted Proofs in Dynamics) project. We decided to make...
  • CyNTHIA

  • Referenced in 1 article [sw19663]
  • Proofs-as-programs as a framework for the design of an analogy-based ML editor ... C Y NTHIA is a transformation-based editor for a functional subset of ML that ... framework for formal program development. Users construct programs from existing code by applying editing commands ... system, which is an implementation of proofs-as-programs. We concentrate on identifying analyses that...
  • MJ

  • Referenced in 12 articles [sw24342]
  • object-oriented languages such as Java or C#, a common practice is to define lightweight ... which are sufficiently small to facilitate formal proofs of key properties. However many ... operational semantics of MJ, and give a proof of type safety. In order to demonstrate ... scope of computational effects within a Java program. We define an extension of MJ with...
  • ROOT

  • Referenced in 5 articles [sw20052]
  • step, making use of the interactive C++ interpreter CINT, while running over small data samples ... creating a stand-alone batch program. Finally, if processing farms are available, the user ... data mining in HEP — by using PROOF, which will take care of optimally distributing...
  • Vellvm

  • Referenced in 6 articles [sw13286]
  • them to facilitate different reasoning styles and proof techniques.par To validate Vellvm’s design ... formal semantics that can execute programs from LLVM test suite and thus be compared against ... verify a previously proposed transformation that hardens C programs against spatial memory safety violations. Vellvm...
  • Erlang-B

  • Referenced in 1 article [sw20978]
  • proof of the convergence of the two iterations. Numerical results and a C++ program...
  • Cascade

  • Referenced in 3 articles [sw34344]
  • checked together with restrictions on program behaviors. The tool generates verification conditions for the specified ... solver which either produces a proof or gives a concrete trace showing how an assertion ... Version 2.0 supports the majority of standard C features except for floating point...
  • Octave Interval

  • Referenced in 2 articles [sw13236]
  • applied to computer-assisted proofs, constraint programming, and verified computing. The implementation is based ... standard for interval arithmetic. Related software: INTLAB, C-XSC, filib...
  • CompCertS

  • Referenced in 3 articles [sw22722]
  • this paper, we present a formally verified C compiler, CompCertS, which is essentially the CompCert ... guarantee: it gives a semantics to more programs and ensures that the memory consumption ... memory is available.{par}The whole proof of CompCertS is a significant proof-effort...
  • apims

  • Referenced in 1 article [sw27565]
  • project. Since this is a proof of concept implementation, the users should be prepared ... bugs. apims is a c++ library, but contains sample programs to typecheck and evaluate code...
  • oneTBB

  • Referenced in 1 article [sw42848]
  • Threading Building Blocks. oneTBB is a flexible C++ library that simplifies the work of adding ... parallel programs that take full advantage of the multi-core performance. Such programs are portable ... composable and have a future-proof scalability. oneTBB provides you with functions, interfaces, and classes...
  • Code2Inv

  • Referenced in 1 article [sw41066]
  • Code2Inv: a deep learning framework for program verification. We propose a general ... proof checker as input, and automatically learns a valid proof for the verification task ... instances: a loop invariant synthesizer for C programs, and a Constrained Horn Clause (CHC) solver...
  • mural

  • Referenced in 9 articles [sw23627]
  • Appendix C (88 pp) containing the complete specification of the proof assistant. The first ... system. Chapters 3--6 describe the proof assistant in more detail. The third chapter ... detailed walk into the specification of the proof assistant and assumes the reader ... proof steps, and chapter 6 summarizes the lessons the authors learned during implementing the proof...
  • Eleven82

  • Referenced in 1 article [sw17445]
  • technique capable of automatically proving that a program correctly recovers from a crash ... states into a symbolic search for a proof that recovery terminates and every recovered execution ... tool called Eleven82, capable of analyzing C programs to detect recoverability bugs or prove their...
  • Nebelung

  • Referenced in 1 article [sw13045]
  • writing parallel programs on shared-memory architectures, for C, C++ and Fortran ... scalable performance. The paper presents a first proof-of-concept implementation of OpenMP with...
  • TUAnalyzer

  • Referenced in 1 article [sw13103]
  • that extracts the template structure of C++ programs on the basis ... that depend on the particular instantiation of C++ templates and to relate them to their ... essential to understand real-world legacy C++ applications. We present how our tool extracts this ... been validated on real code as proof of concept. The results obtained with TUAnalyzer enable...
  • Ariel

  • Referenced in 2 articles [sw24050]
  • subset of C. We formulated a notion of correctness of numerical programs, called asymptotic correctness ... proved to be of general utility in program verification.par By ideal machine we mean ... semantics for the language in which the programs we wish to verify are written ... which executes the program to be verified. The meaning of the program is identified with...