
CPBPV
 Referenced in 5 articles
[sw00164]
 CPBPV: a constraintprogramming framework for bounded program verification. This paper studies how to verify ... novel constraintprogramming 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 78 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 highlevel timing analysis of programs to infer exact loop bounds and safe...

SMACK
 Referenced in 8 articles
[sw23311]
 SMACK is both a modular software verification toolchain and a selfcontained 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...

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...

LazyCSeq
 Referenced in 5 articles
[sw13773]
 effective symbolic verification technique for concurrent C programs using POSIX threads. LazyCSeq, a tool ... Software Verification. The tool encodes all thread schedules up to a given bound into ... single nondeterministic 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 onceandforall 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 interpolationbased 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/postconditions, but allows the user to state ... Eclipse plugin. 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...

Spacer
 Referenced in 11 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 worstcase bounds...

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 realtime properties of Java programs. Properties can be expressed ... properties, to calculate, if possible, an upperbound 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...

TACO
 Referenced in 6 articles
[sw07668]
 efficient bounded verification. SATbased bounded verification of annotated code consists of translating the code ... based analysis of JMLannotated Java sequential programs dealing with complex linked data structures ... parallel, automated computation of tight bounds for Java fields. Experiments show that the translations...

CalCS
 Referenced in 7 articles
[sw13098]
 linear convex constraints. Certain formal verification tasks require reasoning about Boolean combinations of nonlinear ... fundamental results from the theory of convex programming to realize a satisfiability modulo theory ... several benchmarks including formulas generated from bounded model checking of hybrid automata and static analysis...