• 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 over-approximation 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 Fine-Grained Approximation. As neural networks make ... networks. Due to overly conservative approximation, differential verification lacks scalability in terms of both accuracy ... fine-grained 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 over-approximation of function calls. In every successful verification run, FunFrog generates function...
  • YASM

  • Referenced in 14 articles [sw09470]
  • Yasm: A Software Model-Checker for Verification and Refutation. This paper presents Yasm ... Traditional software model-checkers build over-approximating abstractions of the programs they analyze and typically ... that a (safety) property of interest holds (verification). On the other hand, since model-checkers...
  • 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 set-propagation, reach-set 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 under-approximations of procedure summaries. Under-approximations 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 non-linear real and real-interval...
  • 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 Navier-Stokes equations ... implicit time integration of discontinuous Galerkin (DG) approximations...
  • UppSAT

  • Referenced in 2 articles [sw26289]
  • Exploring approximations for floating-point 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 step-indexed approximations and global invariants. The logic ... toolbox HolBA for semi-automated 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 scope-bounding 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 flux-limited diffusion approximation to recover the free-streaming limit. Electrons ... energy exchange. We present a suite of verification test problems to demonstrate the accuracy...
  • C-SHORe

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