Software Projects

The BIGNUM Library for Multiple Precision Arithmetic

A C++ library for fast basic operations (add, sub, mul, div, bit operations) in arbitrary precision. Like 1,000,000,000 digits. Or more.

SMTcut — Computing Tropical Prevarieties With Satisfiability Modulo Theories (SMT) Solvers

Basically, a two-part operation: First, tropicalize the polynomials and get a conjunction of disjunctions of polyhedra. Second, resolve the conjunction and return a disjunction of polyhedra.

The computation is done using an SMT solver (CVC4, MathSAT, Yices, Z3).

PtCut — Compute Tropical Prevarieties of Polynomial Systems

Like SMTcut, PtCut tropicalizes the polynomials and computes a disjunction of polyhedra. This time, it does so using PPLpy, a polyhedral library. PtCut is an earlier project and is typically slower than SMTcut.

ODEbase — Symbolic Computation Input Data Derived from Established Biomodels

Symbolic computation allows qualitative answers to biological questions. Qualitative methods analyze dynamical input systems as formal objects, in contrast to numerical simulation, which investigates only a subset of the state space. However, symbolic computation tools and libraries have a different set of requirements for their input data than their numerical counterparts. A common format used in mathematical modeling of biological processes is SBML. The use of SBML data in symbolic computation requires significant pre-processing, incorporating external biological and mathematical expertise. ODEbase provides high-quality symbolic computation input data derived from established biomodels.