
MATISSE
 Referenced in 28 articles
[sw06311]
 free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear ... framework of abstracting linear systems using approximate bisimulation relations [1,2,3,4]. Contrary ... abstraction. Approximate bisimulation based abstraction is particularly useful for the safety verification problem which consists ... more approximations are possible which confirms the intuitive fact that the verification of robustly safe...

SpaceEx
 Referenced in 75 articles
[sw10939]
 SpaceEx: Scalable Verification of Hybrid Systems. We present a scalable reachability algorithm for hybrid systems ... continuous sets to compute an overapproximation of the reachable states. The algorithm improves over ... bound. In addition, we propose an improved approximation model, which drastically improves the accuracy ... implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr...

APMC
 Referenced in 29 articles
[sw11483]
 Approximate probabilistic model checking. Symbolic model checking methods have been extended recently to the verification ... algorithm. In this paper, we propose an approximation method to verify quantitative properties on discrete...

Augur 2
 Referenced in 13 articles
[sw08403]
 design and the present state of the verification tool Augur 2 which is currently being ... which can analyze graph transformation systems by approximating them by Petri nets. The main reason ... create an open, flexible and extensible verification environment. Also, compared to the previous version, Augur...

NeuroDiff
 Referenced in 1 article
[sw42704]
 NeuroDiff: Scalable Differential Verification of Neural Networks using FineGrained Approximation. As neural networks make ... networks. Due to overly conservative approximation, differential verification lacks scalability in terms of both accuracy ... finegrained approximation technique that drastically increases the accuracy of differential verification while achieving many ... contributions. The first one is new convex approximations that more accurately bound the difference neurons...

FunFrog
 Referenced in 6 articles
[sw06571]
 summaries as overapproximation of function calls. In every successful verification run, FunFrog generates function...

YASM
 Referenced in 14 articles
[sw09470]
 Yasm: A Software ModelChecker for Verification and Refutation. This paper presents Yasm ... Traditional software modelcheckers build overapproximating abstractions of the programs they analyze and typically ... that a (safety) property of interest holds (verification). On the other hand, since modelcheckers...

UnitWalk
 Referenced in 36 articles
[sw00993]
 ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized ... also prove that our algorithm is probabilistically approximately complete...

Reveal
 Referenced in 22 articles
[sw00801]
 describe the Reveal formal functional verification system and its application to four representative hardware test ... Reveal performs automatic datapath abstraction yielding an approximation of the original design with a much ... correctness of control logic interactions. If the approximation proves to be too coarse ... this system, we believe that automating the verification for a useful class of hardware designs...

SPeeDI
 Referenced in 8 articles
[sw00896]
 SPeeDI  a verification tool for polygonal hybrid systems Hybrid systems combining discrete and continuous dynamics ... artificial and natural systems, and as an approximation to complex continuous systems. A very important ... hybrid systems this and all interesting verification problems are undecidable. Most of the proved decidability ... major drawback of setpropagation, reachset approximation procedures is that they pay little attention...

Spacer
 Referenced in 12 articles
[sw19496]
 based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular ... approaches, it maintains both over and underapproximations of procedure summaries. Underapproximations are used...

Breach
 Referenced in 26 articles
[sw20822]
 Breach, a toolbox for verification and parameter synthesis of hybrid systems. We describe Breach ... variation. The latter is used to perform approximate reachability analysis and parameter synthesis. A major...

PolyPaver
 Referenced in 3 articles
[sw08771]
 focus of our work is the verification of tight functional properties of numerical programs, such ... approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification ... claim of expressivity, we outline the verification of four example programs, including the integration example ... This algorithm is based on automatic polynomial approximation of nonlinear real and realinterval...

SReachTools
 Referenced in 6 articles
[sw30627]
 approximations of the stochastic reach set. SReachTools can be used to perform probabilistic verification...

maDG
 Referenced in 2 articles
[sw40566]
 development, verification, and validation of a discontinuous Galerkin solver for the NavierStokes equations ... implicit time integration of discontinuous Galerkin (DG) approximations...

UppSAT
 Referenced in 2 articles
[sw26289]
 Exploring approximations for floatingpoint arithmetic using uppsat. We consider the problem of solving floating ... from software verification. We present UppSAT  an new implementation of a systematic approximation refinement framework...

HolBA
 Referenced in 1 article
[sw40808]
 choose decomposition strategy during verification while avoiding stepindexed approximations and global invariants. The logic ... toolbox HolBA for semiautomated program verification, making it applicable to the ARMv6 and ARMv8...

DC2
 Referenced in 1 article
[sw15730]
 software verification. However, lack of scalability makes these tools hard to apply. Furthermore, approximations ... false alarms. This paper proposes DC2, a verification framework using scopebounding to bridge these...

CRASH
 Referenced in 7 articles
[sw18109]
 code for radiative shock hydrodynamics: implementation and verification. We describe the Center for Radiative Shock ... method and uses a fluxlimited diffusion approximation to recover the freestreaming limit. Electrons ... energy exchange. We present a suite of verification test problems to demonstrate the accuracy...

CSHORe
 Referenced in 6 articles
[sw13319]
 functional programs with a number of new verification techniques employing HORS modelchecking as their ... able to use information gathered from an approximate forward reachability analysis to guide its backward ... tool with the stateoftheart verification tools for HORS and obtain encouraging results...