The probabilistic termination tool amber.

We describe the Amber tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner. Amber combines martingale theory with properties of asymptotic bounding functions and implements relaxed versions of existing probabilistic termination proof rules to prove/disprove (positive) almost sure termination of probabilistic loops. Amber supports programs parametrized by symbolic constants and drawing from common probability distributions.

Quantitative Regular Expressions for Arrhythmia Detection.

Implantable medical devices are safety-critical systems whose incorrect operation can jeopardize a patient's health, and whose algorithms must meet tight platform constraints like memory consumption and runtime. In particular, we consider here the case of implantable cardioverter defibrillators, where peak detection algorithms and various others discrimination algorithms serve to distinguish fatal from non-fatal arrhythmias in a cardiac signal. Motivated by the need for powerful formal methods to reason about the performance of arrhythmia detection algorithms, we show how to specify all these algorithms using Quantitative Regular Expressions (QREs).

Quantitative monitoring of STL with edit distance.

In cyber-physical systems (CPS), physical behaviors are typically controlled by digital hardware. As a consequence, continuous behaviors are discretized by sampling and quantization prior to their processing. Quantifying the similarity between CPS behaviors and their specification is an important ingredient in evaluating correctness and quality of such systems.

Computational Modeling, Formal Analysis, and Tools for Systems Biology.

As the amount of biological data in the public domain grows, so does the range of modeling and analysis techniques employed in systems biology. In recent years, a number of theoretical computer science developments have enabled modeling methodology to keep pace. The growing interest in systems biology in executable models and their analysis has necessitated the borrowing of terms and methods from computer science, such as formal analysis, model checking, static analysis, and runtime verification.

Curvature analysis of cardiac excitation wavefronts.

We present the Spiral Classification Algorithm (SCA), a fast and accurate algorithm for classifying electrical spiral waves and their associated breakup in cardiac tissues. The classification performed by SCA is an essential component of the detection and analysis of various cardiac arrhythmic disorders, including ventricular tachycardia and fibrillation. Given a digitized frame of a propagating wave, SCA constructs a highly accurate representation of the front and the back of the wave, piecewise interpolates this representation with cubic splines, and subjects the result to an accurate curvature analysis.

UBioLab: a web-laboratory for ubiquitous in-silico experiments.

The huge and dynamic amount of bioinformatic resources (e.g., data and tools) available nowadays in Internet represents a big challenge for biologists –for what concerns their management and visualization– and for bioinformaticians –for what concerns the possibility of rapidly creating and executing in-silico experiments involving resources and activities spread over the WWW hyperspace.

Teaching cardiac electrophysiology modeling to undergraduate students: laboratory exercises and GPU programming for the study of arrhythmias and spiral wave dynamics.

As part of a 3-wk intersession workshop funded by a National Science Foundation Expeditions in Computing award, 15 undergraduate students from the City University of New York(1) collaborated on a study aimed at characterizing the voltage dynamics and arrhythmogenic behavior of cardiac cells for a broad range of physiologically relevant conditions using an in silico model. The primary goal of the workshop was to cultivate student interest in computational modeling and analysis of complex systems by introducing them through lectures and laboratory activities to current research in cardiac modeling and by engaging them in a hands-on research experience. The success of the workshop lay in the exposure of the students to active researchers and experts in their fields, the use of hands-on activities to communicate important concepts, active engagement of the students in research, and explanations of the significance of results as the students generated them.

CellExcite: an efficient simulation environment for excitable cells.

Background: Brain, heart and skeletal muscle share similar properties of excitable tissue, featuring both discrete behavior (all-or-nothing response to electrical activation) and continuous behavior (recovery to rest follows a temporal path, determined by multiple competing ion flows). Classical mathematical models of excitable cells involve complex systems of nonlinear differential equations. Such models not only impair formal analysis but also impose high computational demands on simulations, especially in large-scale 2-D and 3-D cell networks.

An agent-based multilayer architecture for bioinformatics grids.

Due to the huge volume and complexity of biological data available today, a fundamental component of biomedical research is now in silico analysis. This includes modelling and simulation of biological systems and processes, as well as automated bioinformatics analysis of high-throughput data. The quest for bioinformatics resources (including databases, tools, and knowledge) becomes therefore of extreme importance.

BioWMS: a web-based Workflow Management System for bioinformatics.

Background: An in-silico experiment can be naturally specified as a workflow of activities implementing, in a standardized environment, the process of data and control analysis. A workflow has the advantage to be reproducible, traceable and compositional by reusing other workflows. In order to support the daily work of a bioscientist, several Workflow Management Systems (WMSs) have been proposed in bioinformatics.

Biowep: a workflow enactment portal for bioinformatics applications.

Background: The huge amount of biological information, its distribution over the Internet and the heterogeneity of available software tools makes the adoption of new data integration and analysis network tools a necessity in bioinformatics. ICT standards and tools, like Web Services and Workflow Management Systems (WMS), can support the creation and deployment of such systems. Many Web Services are already available and some WMS have been proposed.

Expressionview: visualization of quantitative trait loci and gene-expression data in Ensembl.

We present here a software tool for combined visualization of gene-expression data and quantitative trait loci (QTL). The application is implemented as an extension to the Ensembl project and caters for a direct transition from microarray experiments of gene or protein expression levels to the genomic context of individual genes and QTL. It supports the visualization of gene clusters and the selection of functional candidate genes in the context of research on complex traits.