• CPBPV

  • Referenced in 5 articles [sw00164]
  • CPBPV: a constraint-programming framework for bounded program verification. This paper studies how to verify ... novel constraint-programming framework for bounded program verification (CPBPV). The CPBPV framework uses constraint stores ... specification and the program and explores execution paths of bounded length nondeterministically. The CPBPV framework...
  • CBMC

  • Referenced in 77 articles [sw09719]
  • programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer ... Verilog. The verification is performed by unwinding the loops in the program and passing...
  • CiaoPP

  • Referenced in 41 articles [sw12089]
  • computational cost, bounds on sizes of terms in the program, etc. Certain kinds of static ... debugging and verification, finding errors before running the program. This includes checking how programs call...
  • Smacc

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

  • Referenced in 3 articles [sw00994]
  • bound and invariant generation. We describe Valigator, a software tool for imperative program verification that ... proving verification conditions and, most importantly, for automatically inferring loop invariants and bound assertions...
  • SMACK

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

  • Referenced in 5 articles [sw13773]
  • effective symbolic verification technique for concurrent C programs using POSIX threads. Lazy-CSeq, a tool ... Software Verification. The tool encodes all thread schedules up to a given bound into ... single non-deterministic sequential C program and then invokes a C model checker. This paper...
  • CAMPY

  • Referenced in 1 article [sw21704]
  • verification using guided theorem enumeration. Determining if a given program satisfies a given bound ... expressed in decidable theories; however, many practical bounds are expressed in nonlinear theories, which ... automatic verification algorithm, {sc Campy}, that determines if a given program $P$ satisfies a given ... resource bound $B$, which may be expressed using polynomial, exponential, and logarithmic terms...
  • MAVEN

  • Referenced in 10 articles [sw07659]
  • MAVEN: Modular aspect verification and interference analysis. Aspects are program modules that include descriptions ... those key events when the aspect is bound (woven) to an underlying system. The MAVEN ... first technique for once-and-for-all verification of an aspect relative to its specification...
  • TCAS

  • Referenced in 5 articles [sw21413]
  • capabilities of Constraint Programming for automated software verification and testing. We built a dedicated constraint ... propagation with Linear Programming to solve conditional disjunctive constraint systems over bounded integers extracted from...
  • FunFrog

  • Referenced in 6 articles [sw06571]
  • implements a function summarization approach for software bounded model checking. It uses interpolation-based function ... every successful verification run, FunFrog generates function summaries of the analyzed program functions and reuses...
  • ESBMC

  • Referenced in 7 articles [sw09946]
  • Modulo Theories (SMT) solver. It allows the verification engineer (i) to verify single- and multi ... array bounds, atomicity and order violations, deadlock and data race; (iii) to verify programs that ... require the user to annotate the programs with pre/post-conditions, but allows the user to state ... Eclipse plug-in. ESBMC converts the verification conditions using different background theories and passes them...
  • JKelloy

  • Referenced in 2 articles [sw09964]
  • Several tools support Alloy specifications for Java programs. However, they can only check the validity ... those specifications with respect to a bounded domain, and thus, in general, cannot provide correctness ... JKelloy, a tool for deductive verification of Java programs with Alloy specifications. It includes automatically...
  • PolyPaver

  • Referenced in 3 articles [sw08771]
  • Programmers and engineers writing such programs will benefit from verification tools that support an expressive ... work provides a new method for verification of numerical software, supporting a substantially more expressive ... used in the specifications, where the integration bounds can be arbitrary expressions over real variables ... expressivity, we outline the verification of four example programs, including the integration example mentioned earlier...
  • VS3

  • Referenced in 2 articles [sw19492]
  • program verification. We present VS3, a tool that automatically verifies complex properties of programs ... power of SMT solvers. VS3 discovers program invariants with arbitrary, but prespecified, quantification and logical ... verify ∀ ∃ properties of programs and to infer worst case upper bounds and preconditions for functional...
  • LARVA

  • Referenced in 6 articles [sw21408]
  • runtime verification of real-time properties of Java programs. Properties can be expressed ... properties, to calculate, if possible, an upper-bound on the memory and temporal overheads induced...
  • JBMC

  • Referenced in 1 article [sw25908]
  • JBMC is a Bounded Model Checker for Java programs. It checks runtime exceptions and user ... definded assertions. The verification is performed by unwinding the loops in the program and passing...
  • DC2

  • Referenced in 1 article [sw15730]
  • framework for scalable, scope-bounded software verification. Software model checking and static analysis have matured ... decade, enabling their use in automated software verification. However, lack of scalability makes these tools ... apply. Furthermore, approximations in the models of program and environment lead to a profusion ... This paper proposes DC2, a verification framework using scope-bounding to bridge these gaps...
  • TACO

  • Referenced in 5 articles [sw07668]
  • efficient bounded verification. SAT-based bounded verification of annotated code consists of translating the code ... based analysis of JML-annotated Java sequential programs dealing with complex linked data structures ... parallel, automated computation of tight bounds for Java fields. Experiments show that the translations...
  • Spacer

  • Referenced in 8 articles [sw19496]
  • model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes ... proof. We show that for programs and properties over a decidable theory, the algorithm ... Boolean programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds...