• ModelPlex

  • Referenced in 4 articles [sw23944]
  • making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior...
  • FCALGS

  • Referenced in 13 articles [sw29550]
  • tools implementing algorithms for Formal Concept Analysis (FCA) – a method of qualitative data analysis founded ... high-performance command-line tools for computing formal concepts, (frequent) itemsets, nonredundant bases, boolean matrix...
  • Gauss

  • Referenced in 2 articles [sw08835]
  • There is very little use of formal methods to debug software in this area, given ... scientific computing community and the formal methods community have not traditionally worked together. The Utah ... combines expertise from scientific computing and formal methods in addressing this problem. We currently focus ... that extracts from MPI C programs a formal model consisting of communicating processes represented...
  • ReLaTIve

  • Referenced in 8 articles [sw07068]
  • inversion of the Laplace transform, formally characterized as collocation methods (C-methods...
  • hexbin

  • Referenced in 10 articles [sw04519]
  • relies on grid graphics and formal (S4) classes and methods...
  • JavaSPI

  • Referenced in 3 articles [sw23647]
  • protocol implementations and specifications every year. Formal methods can alleviate this problem by backing implementations ... with rigorous proofs about their behavior. However, formally-based development typically requires domain specific knowledge...
  • NAT2TEST

  • Referenced in 3 articles [sw16844]
  • also allows an early application of formal methods within the software development process. This strategy ... Tester) or based on a formal conformance relation using tools like...
  • GenMul

  • Referenced in 3 articles [sw37910]
  • architectures. Overall, this allows to challenge formal methods as shown by experiments which compare recent...
  • UMLsec

  • Referenced in 3 articles [sw12754]
  • graduate students in UML or formal methods and security, and for advanced professionals writing critical...
  • VeriStar

  • Referenced in 3 articles [sw09393]
  • within the reach of formal methods. As a pair, VeriStar and VeriSmall represent the first...
  • Atelier B

  • Referenced in 16 articles [sw07086]
  • Method to develop defect-free proven software (formal software). Two versions are available: Community Edition...
  • ABS

  • Referenced in 31 articles [sw21211]
  • interfaces for encapsulation, and cooperative scheduling of method activations inside concurrent objects. This feature combination ... discuss central design issues for ABS and formalize the type system and semantics of Core ... typedness is preserved during execution; in particular, “method not understood” errors do not occur...
  • MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • MPTP project is to make the large formal Mizar Mathematical Library (MML) available to current ... knowledge-based, and generally AI-based ATP methods. This version of MPTP switches ... Mizar proof constructs into the TPTP formalism. The proofs using second-order Mizar schemes...
  • LATIN

  • Referenced in 16 articles [sw19699]
  • developing methods, techniques, and tools for interfacing logics and related formal systems. These systems...
  • Transalg

  • Referenced in 4 articles [sw17349]
  • based on propositional encoding methods for formal computing models and on the concept of symbolic...
  • COMBINE

  • Referenced in 1 article [sw01423]
  • COMBINE: a tool on combined formal methods for bindingly verification. Theorem proving and model checking ... well-known formal methods emerging recently for software verification. Each of them ... verification tool known as COMBINE (Combined fOrmal Methods for BINdingly vErification). Suggested by its name...
  • MizarMode

  • Referenced in 18 articles [sw01973]
  • maintaining a very large body of formalized mathematics. par Mizar is a non-programmable ... compile-correct” software programming loop. While this method is in the beginning more laborious than ... methods employed in tactical and programmable proof assistants, it makes the “proof code ... long-term and large-scale formalization effort. MizarMode has been designed with...
  • Wolf

  • Referenced in 2 articles [sw01299]
  • hunter for concurrent software using formal methods Wolf is a “push-button” model checker...
  • VERIFAI

  • Referenced in 2 articles [sw32550]
  • seeks to address challenges with applying formal methods to perception and ML components, including those ... VERIFAI which centers on simulation guided by formal models and specifications. Several use cases...
  • PVSio-web

  • Referenced in 2 articles [sw11949]
  • barriers that prevent non-experts in formal methods from using PVS. Designers load a picture ... then explore the behaviour of the formal user interface specification through point-and-click interactions...