• OBJ3

  • Referenced in 140 articles [sw05370]
  • OBJ3 is a program specification and proof system based on order sorted equational logic ... parameterized programming and its module system influenced the designs of the Ada, C...
  • ASTREE

  • Referenced in 115 articles [sw13704]
  • errors in programs written in the C programming language. It has been applied with success ... automatically from synchronous specifications, producing a correctness proof for complex software without any false alarm...
  • SETHEO

  • Referenced in 122 articles [sw00707]
  • used as an interpreter for the programming language LOP (under development). The inference machine ... proof procedure is realized as a WAM, factorization, lemma generation and the application of proof ... entire system is implemented in the language $C$ and is running on several machines...
  • seL4

  • Referenced in 91 articles [sw15222]
  • guarantee that a system is free of programming errors. We present our experience in performing ... from an abstract specification down to its C implementation. We assume correctness of compiler, assembly ... knowledge, this is the first formal proof of functional correctness of a complete, general-purpose...
  • CompCert

  • Referenced in 49 articles [sw09737]
  • compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly ... prescribed by the semantics of the source program. By ruling out the possibility of compiler ... source programs. The main result of the project is the CompCert C verified compiler...
  • Pinocchio

  • Referenced in 42 articles [sw10193]
  • additional feature, Pinocchio generalizes to zero-knowledge proofs at a negligible cost over the base ... toolchain that compiles a subset of C into programs that implement the verifiable computation protocol...
  • Infer

  • Referenced in 12 articles [sw20862]
  • memory safety of C programs. It attempts to build a compositional proof of the program...
  • VST-Floyd

  • Referenced in 2 articles [sw28118]
  • foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable ... helping users build functional correctness proofs for C programs using Verifiable...
  • F*

  • Referenced in 20 articles [sw27563]
  • proof assistant based on dependent types. After verification, F* programs can be extracted to efficient ... OCaml, F#, C or ASM code. This enables verifying the functional correctness and security ... allow expressing precise and compact specifications for programs, including functional correctness and security properties ... that programs meet their specifications using a combination of SMT solving and interactive proofs...
  • KITTeL

  • Referenced in 9 articles [sw17045]
  • automated termination analysis of C programs. In this paper we present the tool KITTeL based ... this approach. For this, programs in the compiler intermediate language are translated into term rewrite ... systems (TRSs), and the termination proof itself is then performed on the automatically generated ... evaluation on a large collection of C programs shows the effectiveness and practicality...
  • Ivy

  • Referenced in 9 articles [sw41668]
  • solver, abstraction and model checking, and manual proofs using natural deduction. It supports light-weight ... extract executable distributed programs by translation to efficient C++ code. It is designed to support ... decidable automated reasoning, to improve proof stability and to provide transparency in the case...
  • AstraVer

  • Referenced in 1 article [sw26809]
  • Lemma Functions for Frama-C: C Programs as Proofs. This paper describes the development ... auto-active verification technique in the Frama-C framework. We outline the lemma functions method...
  • LCTD

  • Referenced in 1 article [sw17728]
  • LCTD: test-guided proofs for C programs on LLVM. Recently there has been much interest...
  • DSDP5

  • Referenced in 30 articles [sw04411]
  • interior-point algorithm, written entirely in ANSI C, is freely available under an open source ... purpose solver for semidefinite programming. Its features include a convergence proof with polynomially bounded worst...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • front-ends for the programming languages C# and C enriched by annotations in first-order ... this paper, however, we present a proof-environment, HOL-BoogieP, that combines Boogie with...
  • cminor

  • Referenced in 19 articles [sw09739]
  • level imperative programming language; there are proved-correct optimizing compilers from C to cminor ... concurrent extensions. We detail a machine-checked proof of soundness of our Separation Logic. This ... first large-scale machine-checked proof of a Separation Logic w.r.t. a small-step semantics ... proof assistant. It is a first step towards an environment in which concurrent cminor programs...
  • versat

  • Referenced in 10 articles [sw08417]
  • efficient low-level data structures like mutable C arrays for clauses and other solver state ... implementation and proofs are written in Guru, a verified-programming language. We compare versat...
  • MC++

  • Referenced in 12 articles [sw13199]
  • ordinary differential equations (ODEs). MC++ is programmed in C++ and makes extensive use of class ... flexibility and is particularly well suited for proof-of-concept implementations. Moreover, it is perfectly...
  • Verasco

  • Referenced in 12 articles [sw19985]
  • C 1999 that establishes the absence of run-time errors in analyzed programs. The analyzer ... specified and proved sound using the Coq proof assistant. Verasco’s proof guarantees, with mathematical...
  • VeriSmall

  • Referenced in 6 articles [sw09788]
  • C minor. Thus when our VeriSmall static analyzer claims some shape property of a program ... machine-checked proof guarantees that the assembly language of the compiled program will actually have...