• UNITY

  • Referenced in 173 articles [sw13461]
  • UNITY-based methodology for the construction, analysis and execution of simulation models. The methodology starts ... first into a set of formal assertions, permitting formal verification of the transition systems...
  • PPL

  • Referenced in 91 articles [sw05357]
  • employed in several systems for the analysis and verification of hardware and software components. Current ... thus played an important role in the formal methods community and several critical tasks rely...
  • IMITATOR

  • Referenced in 26 articles [sw00439]
  • verification and robustness analysis of real-time systems with parameters. It relies on the formalism...
  • KJS

  • Referenced in 5 articles [sw18992]
  • used for formal analysis and verification of JavaScript programs. We verified non-trivial programs...
  • GROOVE

  • Referenced in 50 articles [sw09480]
  • GRaphs for Object-Oriented VErification (GROOVE). GROOVE is a project centered around ... transformation and operational semantics. This entails a formal foundation for model transformation and dynamic semantics ... transformation and dynamic semantics through an (automatic) analysis of the resulting graph transformation systems...
  • DREAM Tool

  • Referenced in 3 articles [sw05702]
  • Embedded Analysis Method (DREAM) is a tool and method for the real-time verification ... practical application of formal verification and timing analysis to real-time middleware...
  • Z3str2

  • Referenced in 2 articles [sw30520]
  • essential component in many formal verification, security analysis, and bug-finding tools. Such solvers typically...
  • WSAT

  • Referenced in 37 articles [sw01022]
  • This paper presents Web Service Analysis Tool (WSAT), a tool for analyzing and verifying composite ... standards, most of which lack formal semantics, complicate the formal specification of web service composition ... Asynchronous messaging makes most interesting verification problems undecidable, even when XML message contents are abstracted...
  • CORA

  • Referenced in 6 articles [sw25659]
  • classes for the formal verification of cyber-physical systems using reachability analysis. CORA integrates various...
  • BicolanoMT

  • Referenced in 3 articles [sw28593]
  • formalization is developed to be suited for program verification and static analysis...
  • scyther

  • Referenced in 16 articles [sw09467]
  • scyther tool: verification, falsification, and analysis of security protocols. With the rise of the Internet ... order to provide secure communication. The analysis of such security protocols has turned ... deployment. This has driven the research in formal analysis of security protocols. Unfortunately, there ... efficient protocols, and work on concise formal logics that might allow one to easily prove...
  • MOPS

  • Referenced in 23 articles [sw10117]
  • security properties of software. We describe a formal approach for finding bugs in security-relevant ... Because manual verification is too expensive, we have built a program analysis tool to automate...
  • FShell

  • Referenced in 8 articles [sw14481]
  • FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. Although the principal analogy between ... software testing are quite different from formal verification. Our tool FShell provides a versatile testing ... dispatches queries about the program to program analysis tools. We report on the integration...
  • Mosel

  • Referenced in 5 articles [sw30493]
  • tool-set for the analysis and verification in Monadic Second-order Logic. In this paper ... approach to the logic, based on a formal semantics for a minimal subset, its modular ... integration in a heterogeneous analysis and verification environment...
  • IODINE

  • Referenced in 2 articles [sw26817]
  • properties using dynamic analysis. A practical bottleneck in the formal verification of hardware designs...
  • CVT

  • Referenced in 15 articles [sw09952]
  • viable alternative to a full formal verification of the code-generator program ... freezing” the code generator design after verification. CVT was developed in the context ... techniques based on uninterpreted functions and their analysis over a BDD-represented small model enables...
  • versat

  • Referenced in 9 articles [sw08417]
  • solver. This paper presents versat, a formally verified SAT solver incorporating the essential features ... analysis, non-chronological backtracking, and decision heuristics. Unlike previous related work on SAT-solver verification...
  • EVE

  • Referenced in 1 article [sw31990]
  • Verification Environment) is a formal verification tool for the automated analysis of temporal equilibrium properties...
  • VERSA

  • Referenced in 2 articles [sw21393]
  • time systems analysis. Index Terms Real-time systems, process algebras, specification, verification, formal description techniques...
  • TAXYS

  • Referenced in 21 articles [sw01389]
  • TAXYS: A tool for the development and verification of real-time embedded systems The correct ... TAXYS tool is to produce a formal model that captures the temporal behavior ... environment. For this purpose we use the formal model of timed automata. The choice ... KRONOS model checker for model analysis. From the source code of the application, an ESTEREL...