
ABC
 Referenced in 40 articles
[sw12910]
 publicdomain system for logic synthesis and formal verification of binary logic circuits appearing ... focus on the synergy of sequential synthesis and sequential verification leads to improvements in both ... development, and illustrates its use in formal verification...

VIS
 Referenced in 17 articles
[sw40003]
 with Synthesis) is a system for formal verification, synthesis, and simulation of finite state systems ... recently, interest has increased in methods of formal verification, such as language containment and temporal...

LEGO
 Referenced in 107 articles
[sw09685]
 synthesis and universe polymorphism make proof checking more practical by bringing the level of formalization...

RATSY
 Referenced in 10 articles
[sw15042]
 Requirements Analysis Tool with Synthesis. Formal specifications play an increasingly important role in system design ... approach. Third, it allows correctbyconstruction synthesis of systems from their temporal properties. These...

Metropolis
 Referenced in 17 articles
[sw16265]
 system design that supports simulation, formal analysis, and synthesis...

Vertaf
 Referenced in 4 articles
[sw08200]
 design of reusable software components, the synthesis and generation of software code, and the automatic ... which integrates software componentbased reuse, formal synthesis, and formal verification. A formal UMLbased ... model is proposed for component reuse. Formal synthesis employs quasistatic and quasidynamic scheduling ... automatic generation of multilayer portable efficient code. Formal verification integrates a model checker kernel from...

Oyster
 Referenced in 33 articles
[sw19629]
 program synthesis with Oyster. MartinLöf type theory provides a formal framework for the construction ... approach. We illustrate this by describing the synthesis of a simple evaluator of arithmetic expressions...

ROCS
 Referenced in 5 articles
[sw28114]
 nonlinear dynamical systems. Different from other formal control synthesis tools, it guarantees to generate...

IMITATOR
 Referenced in 29 articles
[sw00439]
 systems with parameters. It relies on the formalism of networks of parametric timed automata, augmented ... stopwatches. It implemented several algorithms including safety synthesis, robustness, untimed language preservation, nonZeno...

APTS
 Referenced in 4 articles
[sw03405]
 Program synthesis from formal requirements specifications using APTS...

WoLFram
 Referenced in 15 articles
[sw02075]
 WoLFram  a word level framework for formal verification and its application. A framework that automatically ... SystemC is presented. The integrated flow of synthesis, verification and debugging of WoLFram is successfully ... shown, that modern SAT solvers can formally verify PLC programs within a short run time...

Sapo
 Referenced in 4 articles
[sw23566]
 Parameter Synthesis of Polynomial Dynamical Systems. Sapo is a tool for the formal analysis ... initial conditions, and 2) Parameter synthesis, i.e., the refinement of a set of parameters ... represented with polytopes while specifications are formalized as Signal Temporal Logic (STL) formulas...

JAHUEL
 Referenced in 2 articles
[sw10084]
 Jahuel: A Formal Framework for Software Synthesis. We present a theoretically sound and automated model ... architectures. The framework consists in (1) a formal language which provides platformindependent constructs...

StocHy
 Referenced in 3 articles
[sw36937]
 StocHy: automated verification and synthesis of stochastic processes. StocHy is a software tool ... given time horizon; and to automatically construct formal abstractions of the SHS. Abstractions are then ... employed for (ii) formal verification or (iii) control (policy, strategy) synthesis. StocHy allows for modular...

Liss
 Referenced in 4 articles
[sw20205]
 based Synchronisation Synthesis). This is the version of Liss for our FMSD (Formal Methods ... preemptive to Preemptive Scheduling using Synchronization Synthesis. In FMSD (2015), submitted [2] http://thorstent.github.io/theses/...

AutoBayes/CC
 Referenced in 4 articles
[sw01806]
 synthesis with automatic code certification  system description. Code certification is a lightweight approach to formally...

miz3
 Referenced in 11 articles
[sw18631]
 interactive theorem proving. We propose a synthesis of the two proof styles of interactive theorem ... declarative style – the possibility to write formal proofs like normal mathematical text – and the procedural...

Amphion
 Referenced in 5 articles
[sw09953]
 creating a diagram that represents the formal specification through menus based upon the domain theory ... also serves to document the specification. Program synthesis is based upon constructive theorem proving...

DaDRA
 Referenced in 1 article
[sw40400]
 verification and controller synthesis. Though traditional approaches to reachability analysis provide formal guarantees...

QuteRTL
 Referenced in 2 articles
[sw12872]
 gatelevel netlist, and link to logic synthesis/ optimization tools (e.g. Berkeley ABC). We have ... QuteRTL on various RTL designs and applied formal equivalence checking with third party tool...