• AutoSyn

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

  • Referenced in 4 articles [sw24777]
  • implementation verification by checking trace containment; (5) a proof manager that aids compositional and assume ... rapid and structured development of new verification algorithms. jMocha is available publicly...
  • RGITL

  • Referenced in 6 articles [sw13917]
  • RGITL: A temporal logic framework for compositional reasoning about interleaved programs. This paper gives ... symbolic execution and induction, known from the verification of sequential programs, which are transferred ... logic. We include an interleaving operator with compositional semantics. As a consequence, the calculus permits ... freedom. RGITL is implemented in the interactive verification environment KIV. It has been used...
  • Ivy

  • Referenced in 9 articles [sw41668]
  • infinite-state systems via three modes: deductive verification using an SMT solver, abstraction and model ... supports light-weight formal methods via compositional specification-based testing and bounded model checking ... counterexamples, automatically audits proofs for decidability of verification conditions, and provides modular hiding of theories...
  • TVT

  • Referenced in 2 articles [sw09811]
  • processes. TVT supports compositional state space construction, stubborn sets and visual verification...
  • CSimpl

  • Referenced in 2 articles [sw22725]
  • oriented language features and verification techniques. We prove the compositionality of the CSimpl semantics...
  • Java+ITP

  • Referenced in 8 articles [sw32259]
  • experimental tool for the verification of properties of a sequential imperative subset of the Java ... equational theory in Maude. It supports compositional reasoning in a Hoare logic for this Java ... translated into semantically equivalent first-order verification conditions (VCs) which are then sent to Maude...
  • CertiKOS

  • Referenced in 8 articles [sw21503]
  • building certified concurrent OS kernels. Complete formal verification of a non-trivial concurrent OS kernel ... grand challenge. We present a novel compositional approach for building certified concurrent OS kernels. Concurrency...
  • Stabhyli

  • Referenced in 5 articles [sw20122]
  • Stabhyli -- a tool for automatic stability verification of non-linear hybrid systems. We present Stabhyli ... Lyapunov theory combined with decomposition and composition techniques...
  • ORIGEN2

  • Referenced in 3 articles [sw18052]
  • nuclear fuel cycles and calculating the nuclide compositions and characteristics of materials contained therein ... Canada deuterium uranium reactors. A number of verification activities have been undertaken, including (a) comparison ... comparison of predicted spent fuel compositions with measured values. The agreement between ORIGEN2 ... maintenance and user support along with additional verification studies and limited modifications to enhance...
  • SeismoStruct

  • Referenced in 4 articles [sw17671]
  • variety of pre-defined steel, concrete and composite section configurations. The program has been extensively ... checked and validated, as described in its Verification Report...
  • Moby/DC

  • Referenced in 5 articles [sw01395]
  • intermediate language for the analysis and verification of real-time system descriptions that contain timing ... algorithm for phase automata. The algorithm applies compositional model-checking techniques and handles parameters...
  • PGWFT

  • Referenced in 3 articles [sw10573]
  • PGWFT: A Petri Net Based Grid Workflow Verification and Optimization Toolkit. Graphical workflow modeling tools ... this paper, we propose a service composition oriented grid workflow model and its related ... present a Petri net based grid workflow verification and optimization toolkit, called PGWFT, to help...
  • DLC

  • Referenced in 2 articles [sw19394]
  • verification such as model-checking. An LNT specification is made of a parallel composition...
  • VeriCon

  • Referenced in 5 articles [sw16297]
  • then implements classical Floyd-Hoare-Dijkstra deductive verification using Z3. Our preliminary experience indicates that ... simple core SDN programs. VeriCon is compositional, in the sense that it verifies the correctness...
  • Sigali

  • Referenced in 1 article [sw12303]
  • dedicated to controller synthesis, optimal control or verification. Of course, one can also manipulate ILTS ... compose them according to different composition operators). Functions allowing to compute the successors (resp. predecessors...
  • ITACA

  • Referenced in 5 articles [sw15257]
  • ITACA: an integrated toolbox for the automatic composition and adaptation of web services. Adaptation ... contracts involving several services; (ii) simulation and verification techniques which help to identify and correct...
  • NetSketch

  • Referenced in 2 articles [sw20006]
  • Safe compositional network sketches: formal framework. NetSketch is a tool for the specification of constrained ... outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power ... whole-system analysis with a more flexible compositional analysis. The compositional analysis is based...
  • Weak2SC

  • Referenced in 1 article [sw18521]
  • problem for weak memory models to the verification on SC. The reduction proceeds by generating ... additional interleavings on SC. Our technique is compositional in the sense that program generation ... concurrent program. We formally prove compositionality as well as soundness of our technique ... allow for a wide range of verification options. We demonstrate the effectiveness of our technique...
  • LTL_to_DRA

  • Referenced in 1 article [sw28829]
  • monolithic structure, the new method is compositional. Furthermore, in some cases the resulting automata ... this entry contains a complete formalisation and verification of the translation. Furthermore from this basis...