-
phyloDB: A framework for large-scale phylogenetic analysis
Authors:
Bruno Lourenço,
Cátia Vaz,
Miguel E. Coimbra,
Alexandre P. Francisco
Abstract:
phyloDB is a modular and extensible framework for large-scale phylogenetic analyses, which are essential for understanding epidemics evolution. It relies on the Neo4j graph database for data storage and processing, providing a schema and an API for representing and querying phylogenetic data. Custom algorithms are also supported, allowing to perform heavy computations directly over the data, and t…
▽ More
phyloDB is a modular and extensible framework for large-scale phylogenetic analyses, which are essential for understanding epidemics evolution. It relies on the Neo4j graph database for data storage and processing, providing a schema and an API for representing and querying phylogenetic data. Custom algorithms are also supported, allowing to perform heavy computations directly over the data, and to store results in the database. Multiple computation results are stored as multilayer networks, promoting and facilitating comparative analyses, as well as avoiding unnecessary ab initio computations. The experimental evaluation results showcase that phyloDB is efficient and scalable with respect to both API operations and algorithms execution.
△ Less
Submitted 19 October, 2023;
originally announced October 2023.
-
Cloud Classification with Unsupervised Deep Learning
Authors:
Takuya Kurihana,
Ian Foster,
Rebecca Willett,
Sydney Jenkins,
Kathryn Koenig,
Ruby Werman,
Ricardo Barros Lourenco,
Casper Neo,
Elisabeth Moyer
Abstract:
We present a framework for cloud characterization that leverages modern unsupervised deep learning technologies. While previous neural network-based cloud classification models have used supervised learning methods, unsupervised learning allows us to avoid restricting the model to artificial categories based on historical cloud classification schemes and enables the discovery of novel, more detail…
▽ More
We present a framework for cloud characterization that leverages modern unsupervised deep learning technologies. While previous neural network-based cloud classification models have used supervised learning methods, unsupervised learning allows us to avoid restricting the model to artificial categories based on historical cloud classification schemes and enables the discovery of novel, more detailed classifications. Our framework learns cloud features directly from radiance data produced by NASA's Moderate Resolution Imaging Spectroradiometer (MODIS) satellite instrument, deriving cloud characteristics from millions of images without relying on pre-defined cloud types during the training process. We present preliminary results showing that our method extracts physically relevant information from radiance data and produces meaningful cloud classes.
△ Less
Submitted 30 September, 2022;
originally announced September 2022.
-
A Simplified Treatment of Ramana's Exact Dual for Semidefinite Programming
Authors:
Bruno F. Lourenço,
Gábor Pataki
Abstract:
In semidefinite programming the dual may fail to attain its optimal value and there could be a duality gap, i.e., the primal and dual optimal values may differ. In a striking paper, Ramana proposed a polynomial size extended dual that does not have these deficiencies and yields a number of fundamental results in complexity theory. In this work we walk the reader through a concise and self-containe…
▽ More
In semidefinite programming the dual may fail to attain its optimal value and there could be a duality gap, i.e., the primal and dual optimal values may differ. In a striking paper, Ramana proposed a polynomial size extended dual that does not have these deficiencies and yields a number of fundamental results in complexity theory. In this work we walk the reader through a concise and self-contained derivation of Ramana's dual, relying mostly on elementary linear algebra.
△ Less
Submitted 6 September, 2022; v1 submitted 26 May, 2022;
originally announced May 2022.
-
Explaining Counterexamples with Giant-Step Assertion Checking
Authors:
Benedikt Becker,
Cláudio Belo Lourenço,
Claude Marché
Abstract:
Identifying the cause of a proof failure during deductive verification of programs is hard: it may be due to an incorrectness in the program, an incompleteness in the program annotations, or an incompleteness of the prover. The changes needed to resolve a proof failure depend on its category, but the prover cannot provide any help on the categorisation. When using an SMT solver to discharge a proo…
▽ More
Identifying the cause of a proof failure during deductive verification of programs is hard: it may be due to an incorrectness in the program, an incompleteness in the program annotations, or an incompleteness of the prover. The changes needed to resolve a proof failure depend on its category, but the prover cannot provide any help on the categorisation. When using an SMT solver to discharge a proof obligation, that solver can propose a model from a failed attempt, from which a possible counterexample can be derived. But the counterexample may be invalid, in which case it may add more confusion than help. To check the validity of a counterexample and to categorise the proof failure, we propose the comparison between the run-time assertion-checking (RAC) executions under two different semantics, using the counterexample as an oracle. The first RAC execution follows the normal program semantics, and a violation of a program annotation indicates an incorrectness in the program. The second RAC execution follows a novel "giant-step" semantics that does not execute loops nor function calls but instead retrieves return values and values of modified variables from the oracle. A violation of the program annotations only observed under giant-step execution characterises an incompleteness of the program annotations. We implemented this approach in the Why3 platform for deductive program verification and evaluated it using examples from prior literature.
△ Less
Submitted 6 August, 2021;
originally announced August 2021.
-
Running the Network Harder: Connection Provisioning under Resource Crunch
Authors:
Rafael B. R. Lourenco,
Massimo Tornatore,
Charles U. Martel,
Biswanath Mukherjee
Abstract:
Traditionally, networks operate at a small fraction of their capacities; however, recent technologies, such as Software-Defined Networking, may let operators run their networks harder (i.e., at higher utilization levels). Higher utilization can increase the network operator's revenue, but this gain comes at a cost: daily traffic fluctuations and failures might occasionally overload the network. We…
▽ More
Traditionally, networks operate at a small fraction of their capacities; however, recent technologies, such as Software-Defined Networking, may let operators run their networks harder (i.e., at higher utilization levels). Higher utilization can increase the network operator's revenue, but this gain comes at a cost: daily traffic fluctuations and failures might occasionally overload the network. We call such situations Resource Crunch. Dealing with Resource Crunch requires certain types of flexibility in the system. We focus on scenarios with flexible bandwidth requirements, e.g., some connections can tolerate lower bandwidth allocation. This may free capacity to provision new requests that would otherwise be blocked. For that, the network operator needs to make an informed decision, since reducing the bandwidth of a high-paying connection to allocate a low-value connection is not sensible. We propose a strategy to decide whether or not to provision a request (and which other connections to degrade) focusing on maximizing profits during Resource Crunch. To address this problem, we use an abstraction of the network state, called a Connection Adjacency Graph (CAG). We propose PROVISIONER, which integrates our CAG solution with an efficient Linear Program (LP). We compare our method to existing greedy approaches and to LP-only solutions, and show that our method outperforms them during Resource Crunch.
△ Less
Submitted 25 April, 2018; v1 submitted 29 September, 2017;
originally announced October 2017.
-
A Single-Assignment Translation for Annotated Programs
Authors:
Cláudio Belo Lourenço,
Maria João Frade,
Jorge Sousa Pinto
Abstract:
We present a translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct. We prove that the translation is sound and complete. This is a companion report to our paper Formalizing Single-assignment Program Verification: an Adaptation-complete Approach [6].
We present a translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct. We prove that the translation is sound and complete. This is a companion report to our paper Formalizing Single-assignment Program Verification: an Adaptation-complete Approach [6].
△ Less
Submitted 5 May, 2016; v1 submitted 4 January, 2016;
originally announced January 2016.
