• CBMC

  • Referenced in 77 articles [sw09719]
  • Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot ... Verilog. The verification is performed by unwinding the loops in the program and passing...
  • CakeML

  • Referenced in 42 articles [sw08799]
  • implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code ... permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics ... demonstrating that each piece of such a verification effort can in practice be composed with ... more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself...
  • TVOC

  • Referenced in 19 articles [sw02521]
  • compiler optimizations: for a given source program, TVOC proves the equivalence of the source code ... phases to the verification process: the first phase verifies loop transformations using the proof rule...
  • SMACK

  • Referenced in 7 articles [sw23311]
  • SMACK is both a modular software verification toolchain and a self-contained software verifier ... programs. In its default mode, assertions are verified up to a given bound on loop ... depth; it contains experimental support for unbounded verification as well. Under the hood, SMACK...
  • Leon

  • Referenced in 10 articles [sw09159]
  • present the Leon verification system for a subset of the Scala programming language. Along with ... supports imperative constructs such as mutations and loops, using a translation into recursive functional form...
  • Memorax

  • Referenced in 3 articles [sw09759]
  • weak memory models. The verification task is non-trivial as it involves exploring state spaces ... arbitrary or even infinite sizes. Even for programs that only manipulate finite range variables ... CEGAR loop to make possible the verification of control state reachability for concurrent programs involving...
  • TRACER

  • Referenced in 11 articles [sw09484]
  • verification tool based on symbolic execution for finite-state C sequential programs developed at National ... path then the program is reported as safe. Otherwise, either the program may contain ... number of program branches, and infinite-length symbolic paths due to unbounded loops. TRACER computes...
  • JBMC

  • Referenced in 1 article [sw25908]
  • assertions. The verification is performed by unwinding the loops in the program and passing...
  • TransLucid

  • Referenced in 2 articles [sw21486]
  • TransLucid: Iteration, dataflow, intensional and Cartesian programming. We present the development of the Lucid language ... formal verification, was used to formalise the iteration in while-loop programs. The pLucid language...
  • FunFrog

  • Referenced in 6 articles [sw06571]
  • analyzed program functions and reuses them to reduce the complexity of the successive verification ... tool incorporates a counter-example-guided refinement loop. Experimental evaluation demonstrates competitiveness of FunFrog with...
  • Alpha

  • Referenced in 6 articles [sw13717]
  • guide the transformations towards imperative loop code for general purpose (sequential or parallel) processors. This ... calculus, abstract and non-standard interpretation, program verification, optimization, architecture synthesis, VLSI, FPGA, systolic arrays...
  • QuIt

  • Referenced in 1 article [sw29333]
  • framework to analyze and verify programs containing loops by using a first-order language ... express both functional and temporal properties of loops. We prove soundness and completeness ... correctness verification, termination analysis and invariant generation. For doing so, we express the loop semantics ... supports full first-order reasoning, including proving program properties with alternation of quantifiers. Our work...
  • DynaMate

  • Referenced in 2 articles [sw14286]
  • automatic full functional verification. DYNAMATE is a tool that automatically infers loop invariants and uses ... them to prove Java programs correct with respect to a given JML functional specification. DYNAMATE...
  • Valigator

  • Referenced in 3 articles [sw00994]
  • Valigator, a software tool for imperative program verification that efficiently combines symbolic computation and automated ... generating and proving verification conditions and, most importantly, for automatically inferring loop invariants and bound...
  • FocusCheck

  • Referenced in 3 articles [sw01298]
  • verification and easy debugging of assertion violations in sequential C programs. The main functionalities ... ability to: (a) identify all minimum-recursion, loop-free counter-examples in a C program...
  • Smacc

  • Referenced in 2 articles [sw14305]
  • programs. It can be used for program verification, bounded model checking and generating SMT benchmarks ... high-level timing analysis of programs to infer exact loop bounds and safe over-approximations...
  • Aligator

  • Referenced in 8 articles [sw00029]
  • We describe the new software package Aligator for...
  • Apron

  • Referenced in 66 articles [sw00045]
  • Apron: a library of numerical abstract domains for...
  • cdd

  • Referenced in 107 articles [sw00114]
  • The program cdd+ (cdd, respectively) is a C...
  • CGAL

  • Referenced in 334 articles [sw00118]
  • The goal of the CGAL Open Source Project...