• ABC

  • Referenced in 37 articles [sw12910]
  • public-domain 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...
  • 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 correct-by-construction 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 component-based reuse, formal synthesis, and formal verification. A formal UML-based ... model is proposed for component reuse. Formal synthesis employs quasi-static and quasi-dynamic 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. Martin-Lö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...
  • 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, non-Zeno...
  • APTS

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

  • Referenced in 3 articles [sw28114]
  • nonlinear dynamical systems. Different from other formal control synthesis tools, it guarantees to generate...
  • 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 3 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 platform-independent 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...
  • QuteRTL

  • Referenced in 2 articles [sw12872]
  • gate-level 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...
  • Limi

  • Referenced in 4 articles [sw20206]
  • identical up to swapping independent symbols. The formal definition is given in our paper ... preemptive to Preemptive Scheduling using Synchronization Synthesis...
  • AutoSyn

  • Referenced in 3 articles [sw02043]
  • AutoSyn: A new approach to automated synthesis of composite web services with correctness guarantee ... composite service beforehand and then perform certain formal verification to guarantee the correctness ... where the correctness is guaranteed in the synthesis process. For a given set of services...