• CVPP

  • Referenced in 7 articles [sw00179]
  • describes CVPP, a tool set for compositional verification of control-flow safety properties for programs ... with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed ... manipulate, in particular when it comes to verification or the construction of maximal models. Therefore ... paper presents the underlying framework for compositional verification and the components of the tool...
  • LTSA-WS

  • Referenced in 13 articles [sw10585]
  • tool for model-based verification of web service compositions and choreography. In this paper ... approach to verifying compositions of web service implementations. The tool supports verification of properties created ... design verification and validation, the implementation, testing and deployment of web service compositions ... specification, formal modeling, verification and validation of the composition process...
  • WSAT

  • Referenced in 37 articles [sw01022]
  • service composition. (2) Asynchronous messaging makes most interesting verification problems undecidable, even when XML message...
  • Rebeca

  • Referenced in 8 articles [sw09422]
  • effort to bridge the gap between formal verification approaches and real applications. Rebeca is supported ... Rebeca are used to introduce compositional verification, abstraction, symmetry and partial order reduction techniques...
  • ECDAR

  • Referenced in 10 articles [sw02824]
  • Ecdar a new tool for compositional design and verification of real time systems. In Ecdar ... supports the important operations of a good compositional reasoning theory: composition, conjunction, quotient, consistency/satisfaction checking ... between components. The compositional approach allows for scalability in the verification...
  • fc2tools

  • Referenced in 11 articles [sw12386]
  • algebra theory, for syntax and semantics; verification by compositional reductions and abstraction; alternative or combined ... exchange format for easy interface with other verification softwares...
  • D-Finder

  • Referenced in 14 articles [sw00200]
  • Finder tool implements a compositional method for the verification of component-based systems described...
  • ProMoVer

  • Referenced in 4 articles [sw06738]
  • previously developed tool set for compositional verification of control flow safety properties, and provides appropriate...
  • Pilsner

  • Referenced in 6 articles [sw20004]
  • Pilsner: a compositionally verified compiler for a higher-order imperative language. Compiler verification is essential ... compilers, it is important to develop a compositional notion of compiler correctness that is modular ... develop a novel approach to compositional compiler verification based on parametric inter-language simulations (PILS ... PILS are modular: they enable compiler verification in a manner that supports separate compilation. PILS...
  • ERA-PAT

  • Referenced in 2 articles [sw13259]
  • Automatic compositional verification of timed systems. Specification and verification of real-time systems are important ... modeling, animated simulation, and fully automatic compositional verification based on learning techniques. Experimental results show...
  • Exp.Open

  • Referenced in 10 articles [sw07702]
  • Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods. It is desirable ... tool of the Cadp verification toolbox which combines several features. First, Exp.Open 2.0 allows ... describe concurrent systems as a composition of finite state machines, using either synchronization vectors...
  • CMC

  • Referenced in 34 articles [sw12422]
  • paper we present a tool (CMC) for compositional model-checking of real-time systems ... different method compared to existing real-time verification tools (HYTECH, KRONOS, UPPAAL). After a description...
  • visualSTATE

  • Referenced in 9 articles [sw07481]
  • Verification of large state/event systems using compositionality and dependency analysis A state/event model ... This paper introduces a technique that uses compositionality and dependency analysis to significantly improve ... state/event models. It makes possible automated verification of large industrial designs with...
  • XYZ/SE

  • Referenced in 2 articles [sw03027]
  • enhance the readability and to simplify the verification of temporal logic programs ... partial correctness of XYZ/SE programs in a compositional way. Moreover, we show that every XYZ/BE ... have developed a general compositional verification method in the XYZ system concerning the sequential case...
  • PeCAn

  • Referenced in 1 article [sw30318]
  • PeCAn: compositional verification of Petri nets made easy. This paper introduces PeCAn, a tool supporting ... compositional verification of Petri nets. Beyond classical features (such as on-the-fly analysis ... their composition to support modular abstractions of multiple Petri nets for more efficient verification. Furthermore...
  • Threader

  • Referenced in 14 articles [sw09938]
  • programs. Threader is a tool that automates verification of safety and termination properties for multi ... reasoning that is compositional with regards to the thread structure of the verified program. This ... paper describes the verification approach taken by Threader and provides instructions on how to install...
  • METROPOLIS

  • Referenced in 2 articles [sw24044]
  • that their composition satisfies a set of given properties thus making the verification problem much ... tool in METROPOLIS for supporting compositional modeling and verification of METROPOLIS specifications and present...
  • SOLOIST

  • Referenced in 1 article [sw16438]
  • services involved in a service composition make verification activities crucial. On a par with verification ... service compositions, with the related issue of balancing expressiveness and support for automated verification. This ... language for formalizing the interactions of service compositions. SOLOIST has been designed with the primary ... using SOLOIST with established verification techniques, both at design time and at run time...
  • Infer

  • Referenced in 10 articles [sw20862]
  • programs. Infer is a new automatic program verification tool aimed at proving memory safety ... programs. It attempts to build a compositional proof of the program at hand by composing...
  • AutoSyn

  • Referenced in 3 articles [sw02043]
  • behaviors of a composite service beforehand and then perform certain formal verification to guarantee...