
CBMC
 Referenced in 86 articles
[sw09719]
 CBMC is a Bounded Model Checker for ANSIC and C++ programs. It also ... supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety...

INTLAB
 Referenced in 472 articles
[sw04004]
 slopes (sequential approach, slow for many variables) verified integration of (simple) univariate functions univariate ... slow) multiple precision interval arithmetic with error bounds (does the job, slow...

UCLID
 Referenced in 25 articles
[sw04657]
 UCLID: As a verifier, for termlevel bounded model checking, correspondence checking, deductive verification ... verification, analyzing software for security exploits, and verifying distributed algorithms...

ACETAF
 Referenced in 7 articles
[sw00014]
 ACETAF: A software package for computing validated bounds for Taylor coefficients of analytic functions. This ... presents methods for practical computation of verified bounds for Taylor coefficients of analytic functions. These...

C2e2
 Referenced in 11 articles
[sw20139]
 Engine (C2E2) is a tool for verifying boundedtime invariant properties of hybrid system...

PHAVer
 Referenced in 118 articles
[sw04123]
 ground as a potentially powerful tool for verifying hybrid systems – yet it has remained severely ... properties of hybrid systems with piecewise constant bounds on the derivatives. Aﬃne dynamics are handled...

MRMC
 Referenced in 73 articles
[sw04129]
 Checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL ... support for computing time and rewardbounded reachability probabilities, (propertydriven) bisimulation minimization, and precise...

VSDP
 Referenced in 12 articles
[sw04003]
 that is designed for the computation of verified results in conic programming. The current version ... computing rigorous error bounds of the true optimal value, verified enclosures of εoptimal solutions...

AFiD_GPU
 Referenced in 7 articles
[sw24939]
 unprecedented in thermallydriven wallbounded turbulence. To verify the accuracy of the code, turbulent...

SMACK
 Referenced in 9 articles
[sw23311]
 default mode, assertions are verified up to a given bound on loop iterations and recursion...

ESBMC
 Referenced in 8 articles
[sw09946]
 ESBMC is a contextbounded model checker for embedded C/C++ software based on Satisfiability Modulo ... allows the verification engineer (i) to verify single and multithreaded software (with shared variables ... array bounds, atomicity and order violations, deadlock and data race; (iii) to verify programs that...

core 2
 Referenced in 7 articles
[sw04960]
 based on iterative verified approximations, combined with constructive zero bounds. This paper describes Core...

MAVEN
 Referenced in 10 articles
[sw07659]
 aspect is bound (woven) to an underlying system. The MAVEN tool verifies the correctness...

Crust
 Referenced in 1 article
[sw34343]
 Crust: A Bounded Verifier for Rust (N). Rust is a modern systems language that provides ... tool combining exhaustive test generation and bounded model checking to detect memory safety errors...

DiVer
 Referenced in 10 articles
[sw01938]
 verifying large designs. The engines with their respective roles are as follows: Bounded Model Checking ... combination with PBIA in BMC for verifying embedded memory systems with multiple memories (with multiple...

Hybrid Trace Verifier
 Referenced in 2 articles
[sw20335]
 Computing bounded reach sets from sampled simulation traces. This paper presents an algorithm which uses ... algorithm in a tool, Hybrid Trace Verifier (HTV), uses Mathwork’s Simulink/Stateflow (SLSF) environment ... overapproximation relies on computing error bounds in the dynamics obtained from the formal model. Verification...

CPBPV
 Referenced in 5 articles
[sw00164]
 programming framework for bounded program verification. This paper studies how to verify the conformity ... proposes a novel constraintprogramming framework for bounded program verification (CPBPV). The CPBPV framework uses...

ACRITHXSC
 Referenced in 49 articles
[sw00015]
 deliver results of high accuracy which are verified to be correct by the computer. Thus ... complete sample program for computing continuous bounds on the solution of an initial value problem...

EdmondsKarp
 Referenced in 6 articles
[sw28548]
 formally prove a bound on its complexity. Further refinement yields a verified implementation, whose execution...

TESTAS
 Referenced in 19 articles
[sw00957]
 strictly locally testable, or piecewise testable. The bounds on order of local testability of transition ... testability of transition graph is verified. Some new effective polynomial time algorithms are used. These...