
UNITY
 Referenced in 173 articles
[sw13461]
 UNITYbased 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 realtime 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 nontrivial programs...

GROOVE
 Referenced in 50 articles
[sw09480]
 GRaphs for ObjectOriented 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 realtime verification ... practical application of formal verification and timing analysis to realtime middleware...

Z3str2
 Referenced in 2 articles
[sw30520]
 essential component in many formal verification, security analysis, and bugfinding 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 cyberphysical 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 securityrelevant ... 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]
 toolset for the analysis and verification in Monadic Secondorder 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 codegenerator program ... freezing” the code generator design after verification. CVT was developed in the context ... techniques based on uninterpreted functions and their analysis over a BDDrepresented small model enables...

versat
 Referenced in 9 articles
[sw08417]
 solver. This paper presents versat, a formally verified SAT solver incorporating the essential features ... analysis, nonchronological backtracking, and decision heuristics. Unlike previous related work on SATsolver 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 Realtime systems, process algebras, specification, verification, formal description techniques...

TAXYS
 Referenced in 21 articles
[sw01389]
 TAXYS: A tool for the development and verification of realtime 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...