• MPTP 0.2

  • Referenced in 43 articles [sw02589]
  • project is to make the large formal Mizar Mathematical Library (MML) available to current first...
  • GRTensorII

  • Referenced in 40 articles [sw00393]
  • package contains a library of standard definitions of a large number of commonly used curvature ... tensors, as well as the Newman-Penrose formalism. The standard object libraries are easily expandable...
  • MPTP

  • Referenced in 22 articles [sw02489]
  • arise with the existence of large integral bodies of formalized mathematics. Then we proceed ... which makes the largest existing corpus of formalized mathematics available to theorem provers. MPTP (Mizar ... system for translating the Mizar Mathematical Library (MML) into untyped first order format suitable ... used for selecting suitable axioms from the large library for an arbitrary problem, and again...
  • CoqHammer

  • Referenced in 12 articles [sw29396]
  • find appropriate lemmas in a large collection of all accessible lemmas and combine them ... given formalization, not only the lemmas from predefined libraries or hint databases. At present, however...
  • booleannet

  • Referenced in 7 articles [sw22019]
  • research increasingly relies on computational solutions, from large scale data analyses to theoretical modeling. Within ... biological observations and hypotheses into a mathematical formalism. The conceptual underpinnings of Boolean modeling ... used in Boolean simulations, present a software library that can perform these simulations based ... inputs and give three case studies. The large scale simulations in these case studies demonstrate...
  • VATA

  • Referenced in 7 articles [sw09917]
  • automata library applicable, e.g., in formal verification. The library supports both explicit and semi-symbolic ... encoding is intended for tree automata with large alphabets. For storing their transition functions...
  • MTBDD

  • Referenced in 5 articles [sw12873]
  • automata library applicable, e.g., in formal verification. The library supports both explicit and semi-symbolic ... encoding is intended for tree automata with large alphabets. For storing their transition functions...
  • Proofwatch

  • Referenced in 3 articles [sw28654]
  • Prover9 theorem provers, both for interactive formalizations and for human-assisted proving of open conjectures ... watchlists in large theories coming from first-order translations of large ITP libraries, aiming...
  • Gmeta

  • Referenced in 3 articles [sw10110]
  • lemmas and definitions required in mechanizations of formal metatheory. The key idea is to employ ... representing a large family of object languages we define datatype-generic libraries of infrastructure...
  • QHOPDM

  • Referenced in 5 articles [sw04335]
  • modularly structured library of FORTRAN subroutines for large scale linear optimization. We broadened this software ... presenting QHOPDM, a library for convex quadratic optimization with linear constraints. Formally, we solve...
  • simpA

  • Referenced in 7 articles [sw00863]
  • platforms -- Java is a main example -- with libraries providing fine-grained mechanisms and idioms ... pure object-oriented abstractions help building large component-based programs. To this end, in this ... examples. Finally, we define an operational semantics formalizing the main aspects of this programming model...
  • libVATA

  • Referenced in 1 article [sw33005]
  • library is to be used in formal verification, but we believe that ... encoding of tree automata supported by the library: explicit and semi-symbolic. The semi-symbolic ... used for automata with large alphabets, which appear in several formal verification techniques using tree ... theory of k successors (WSkS). Moreover, the library can also be used for finite word...
  • Gauss

  • Referenced in 2 articles [sw08835]
  • project combines expertise from scientific computing and formal methods in addressing this problem. We currently ... Message Passing Interface (MPI) library. Large-scale MPI programs also employ shared memory threads ... styles can result in additional bugs. MPI libraries themselves can be buggy as they strive ... that extracts from MPI C programs a formal model consisting of communicating processes represented...
  • IFP-C3D

  • Referenced in 5 articles [sw09125]
  • internal engines. IFP-C3D uses an unstructured formalism, the finite volume method on staggered grids ... deal with complex moving geometries with large volume deformation induced by all moving geometrical parts ... spray modelling enable the simulation of a large variety of innovative engine configurations from ... direct injection hydrogen internal combustion engines. Large super-scalar machines up to 1 000 processors...
  • SOSpin

  • Referenced in 1 article [sw22163]
  • present in this paper the SOSpin library, which calculates an analytic decomposition of the Yukawa ... make use of the oscillator expansion formalism, where the 𝖲𝖮(2N) spinor representations are expressed ... large products of creation and annihilation operators. We illustrate the use of our library with...
  • BANE

  • Referenced in 1 article [sw30929]
  • implementation of program analyses around a library of generic constraint solvers promotes reuse, gives control ... formalism of mixed constraints which provides a combination of several constraint formalisms with distinct precision ... techniques to support the practical resolution of large constraint systems. We give empirical results supporting...
  • RoutingLib

  • Referenced in 1 article [sw28638]
  • Discrete Data”. That paper investigates a large class of iterative algorithms that can be transformed ... distributed computation, making formal verification worthwhile.{ }Our Agda library provides users with a collection...
  • AGD

  • Referenced in 12 articles [sw00022]
  • AGD-Library: A Library of Algorithms for Graph...
  • ANSYS

  • Referenced in 641 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...
  • CGAL

  • Referenced in 334 articles [sw00118]
  • The goal of the CGAL Open Source Project...