• GROOVE

  • Referenced in 44 articles [sw09480]
  • GRaphs for Object-Oriented VErification (GROOVE). GROOVE is a project centered around ... dynamic semantics through an (automatic) analysis of the resulting graph transformation systems, for instance using...
  • TopSpin

  • Referenced in 12 articles [sw00972]
  • automatically modifies the model checking algorithm employed by SPIN to exploit these symmetries during verification ... This can result in significantly reduced memory consumption, and in many cases also in faster...
  • OFMC

  • Referenced in 26 articles [sw09466]
  • automatically translated to IF.par OFMC performs both protocol falsification and bounded session verification by exploring ... demand-driven way, the transition system resulting from an IF specification. OFMC’s effectiveness...
  • FoCs

  • Referenced in 19 articles [sw01591]
  • FoCs -- automatic generation of simulation checkers from formal specifications. For the foreseeable future, industrial hardware ... simulation and model checking in the design verification process. To date, these techniques are applied ... different formulations of the problem. This results in cumulative high cost and little...
  • ERA-PAT

  • Referenced in 2 articles [sw13259]
  • simulation, and fully automatic compositional verification based on learning techniques. Experimental results show that...
  • ModelPlex

  • Referenced in 4 articles [sw23944]
  • with the model so that offline verification results no longer apply, ModelPlex initiates provably safe ... systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic ... imply that the offline safety verification results about the CPS model apply to the present...
  • HMC

  • Referenced in 5 articles [sw09867]
  • Milner-Cousots (HMC), an algorithm that reduces verification of safety properties of typed higher-order ... have implemented HMC and describe preliminary experimental results using two imperative checkers – armc and interproc ... abstract interpretation, HMC enables the fully automatic verification of programs written in modern programming languages...
  • OSMOSE

  • Referenced in 5 articles [sw21412]
  • program source code. However, in certain circumstances verification is more relevant when performed ... machine-code level. This paper focuses on automatic test data generation from a stand-alone ... technologies and innovative techniques. The results have been implemented in a tool named OSMOSE...
  • ProMoVer

  • Referenced in 4 articles [sw06738]
  • verification tasks resulting from changes in the code and the specifications. The verification task ... support for abstraction from private methods and automatic extraction of candidate specifications from method implementations...
  • GKLEE

  • Referenced in 8 articles [sw12794]
  • GKLEE: concolic verification and test generation for GPUs. Programs written for GPUs often contain correctness ... races, deadlocks, or may compute the wrong result. Existing debugging tools often miss these errors ... modeling of SIMD concurrency generate false alarms resulting in wasted bug-hunting. They also often ... bugs. For these programs, GKLEE can also automatically generate tests that provide high coverage. These...
  • PIC2LNT

  • Referenced in 2 articles [sw13368]
  • transition systems). Although a lot of theoretical results have been achieved on this language ... verification tools have been designed for analysing π-calculus specifications automatically. The two most famous...
  • GPUVerify

  • Referenced in 6 articles [sw11260]
  • lock-step semantics for analysis and verification of GPU kernels. We study semantics ... both semantics compute identical results or both behave erroneously.par The result induces a method that ... which our novel method can handle fully automatically, but the previous method could not. Overall ... method comes at a modest price: Verification across our benchmark set was 2.25 times slower...
  • Memorax

  • Referenced in 2 articles [sw09759]
  • based CEGAR loop to make possible the verification of control state reachability for concurrent programs ... variables. The reachability procedure is used to automatically compute possible memory fence placements that guarantee ... sense that removing any fence would result in the reachability of the bad control states ... first freely available, open source, push-button verification and fence insertion tool for programs running...
  • DynaMate

  • Referenced in 2 articles [sw14286]
  • automatic full functional verification. DYNAMATE is a tool that automatically infers loop invariants and uses ... postconditions, it automatically discharged over 97% of all proof obligations, resulting in automatic complete correctness...
  • evt

  • Referenced in 6 articles [sw09805]
  • overview of the main results of the project “Verification of ERLANG Programs ”, which is funded ... initiative. Its main outcome is the ERLANG Verification Tool (EVT), a theorem prover which assists ... recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning ... summarised, and an approach for supporting verification in the presence of program libraries is outlined...
  • verifier

  • Referenced in 1 article [sw12878]
  • verification of Shor and Preskill’s unconditional security proof of BB84. As a result ... against an unlimited adversary’s attack semi-automatically, i.e., it is automatic except for giving...
  • SeVe

  • Referenced in 2 articles [sw06547]
  • SeVe: automatic tool for verification of security protocols Security protocols play more and more important ... this framework, and the verification algorithms are also given. The results of this paper ... simulating, and verifying security protocols. The experimental results show that a SeVe module is capable ... also proves the ability in building an automatic verifier for security protocols related to privacy...
  • REFINER

  • Referenced in 3 articles [sw24290]
  • REFINER: Towards Formal Verification of Model Transformations. We present the Refiner tool, which offers techniques ... model until it is concrete enough to automatically generate source code from it. Properties that ... existing model checking toolsets mCRL2 and Cadp, resulting in a complete model checking approach...
  • RUGVEF

  • Referenced in 1 article [sw09868]
  • Automatic testing of real-time graphics systems. In this paper we deal with the general ... verification of real-time graphics systems. In particular we present the Runtime Graphics Verification Framework ... RUGVEF), where we combine techniques from runtime verification and image analysis to automate testing ... Swedish Broadcasting Corporation. We report on experimental results from the evaluation, in particular the discovery...
  • ARIAL

  • Referenced in 1 article [sw02284]
  • functional visualization and verification of signal or image-processing applications. An automatic translator is created ... henceforth the manual translation stage. As a result, a signal-processing designer develops complex applications...