-
Crucible: Graphical Test Cases for Alloy Models
Authors:
Adam G. Emerson,
Allison Sullivan
Abstract:
Alloy is a declarative modeling language that is well suited for verifying system designs. Alloy models are automatically analyzed using the Analyzer, a toolset that helps the user understand their system by displaying the consequences of their properties, hel** identify any missing or incorrect properties, and exploring the impact of modifications to those properties. To achieve this, the Analy…
▽ More
Alloy is a declarative modeling language that is well suited for verifying system designs. Alloy models are automatically analyzed using the Analyzer, a toolset that helps the user understand their system by displaying the consequences of their properties, hel** identify any missing or incorrect properties, and exploring the impact of modifications to those properties. To achieve this, the Analyzer invokes off-the-shelf SAT solvers to search for scenarios, which are assignments to the sets and relations of the model such that all executed formulas hold. To help write more accurate software models, Alloy has a unit testing framework, AUnit, which allows users to outline specific scenarios and check if those scenarios are correctly generated or prevented by their model. Unfortunately, AUnit currently only supports textual specifications of scenarios. This paper introduces Crucible, which allows users to graphically create AUnit test cases. In addition, Crucible provides automated guidance to users to ensure they are creating well structured, valuable test cases. As a result, Crucible eases the burden of adopting AUnit and brings AUnit test case creation more in line with how Alloy scenarios are commonly interacted with, which is graphically.
△ Less
Submitted 13 July, 2023;
originally announced July 2023.
-
Improved statistical benchmarking of digital pathology models using pairwise frames evaluation
Authors:
Ylaine Gerardin,
John Shamshoian,
Judy Shen,
Nhat Le,
Jamie Prezioso,
John Abel,
Isaac Finberg,
Daniel Borders,
Raymond Biju,
Michael Nercessian,
Vaed Prasad,
Joseph Lee,
Spencer Wyman,
Sid Gupta,
Abigail Emerson,
Bahar Rahsepar,
Darpan Sanghavi,
Ryan Leung,
Limin Yu,
Archit Khosla,
Amaro Taylor-Weiner
Abstract:
Nested pairwise frames is a method for relative benchmarking of cell or tissue digital pathology models against manual pathologist annotations on a set of sampled patches. At a high level, the method compares agreement between a candidate model and pathologist annotations with agreement among pathologists' annotations. This evaluation framework addresses fundamental issues of data size and annotat…
▽ More
Nested pairwise frames is a method for relative benchmarking of cell or tissue digital pathology models against manual pathologist annotations on a set of sampled patches. At a high level, the method compares agreement between a candidate model and pathologist annotations with agreement among pathologists' annotations. This evaluation framework addresses fundamental issues of data size and annotator variability in using manual pathologist annotations as a source of ground truth for model validation. We implemented nested pairwise frames evaluation for tissue classification, cell classification, and cell count prediction tasks and show results for cell and tissue models deployed on an H&E-stained melanoma dataset.
△ Less
Submitted 7 June, 2023;
originally announced June 2023.
-
Tunable and Portable Extreme-Scale Drug Discovery Platform at Exascale: the LIGATE Approach
Authors:
Gianluca Palermo,
Gianmarco Accordi,
Davide Gadioli,
Emanuele Vitali,
Cristina Silvano,
Bruno Guindani,
Danilo Ardagna,
Andrea R. Beccari,
Domenico Bonanni,
Carmine Talarico,
Filippo Lunghini,
Jan Martinovic,
Paulo Silva,
Ada Bohm,
Jakub Beranek,
Jan Krenek,
Branislav Jansik,
Luigi Crisci,
Biagio,
Cosenza,
Peter Thoman,
Philip Salzmann,
Thomas Fahringer,
Leila Alexander,
Gerardo Tauriello
, et al. (10 additional authors not shown)
Abstract:
Today digital revolution is having a dramatic impact on the pharmaceutical industry and the entire healthcare system. The implementation of machine learning, extreme-scale computer simulations, and big data analytics in the drug design and development process offers an excellent opportunity to lower the risk of investment and reduce the time to the patient.
Within the LIGATE project, we aim to i…
▽ More
Today digital revolution is having a dramatic impact on the pharmaceutical industry and the entire healthcare system. The implementation of machine learning, extreme-scale computer simulations, and big data analytics in the drug design and development process offers an excellent opportunity to lower the risk of investment and reduce the time to the patient.
Within the LIGATE project, we aim to integrate, extend, and co-design best-in-class European components to design Computer-Aided Drug Design (CADD) solutions exploiting today's high-end supercomputers and tomorrow's Exascale resources, fostering European competitiveness in the field.
The proposed LIGATE solution is a fully integrated workflow that enables to deliver the result of a virtual screening campaign for drug discovery with the highest speed along with the highest accuracy. The full automation of the solution and the possibility to run it on multiple supercomputing centers at once permit to run an extreme scale in silico drug discovery campaign in few days to respond promptly for example to a worldwide pandemic crisis.
△ Less
Submitted 19 April, 2023;
originally announced April 2023.
-
Efficient and Eventually Consistent Collective Operations
Authors:
Roman Iakymchuk,
Amandio Faustino,
Andrew Emerson,
Joao Barreto,
Valeria Bartsch,
Rodrigo Rodrigues,
Jose C. Monteiro
Abstract:
Collective operations are common features of parallel programming models that are frequently used in High-Performance (HPC) and machine/ deep learning (ML/ DL) applications. In strong scaling scenarios, collective operations can negatively impact the overall application performance: with the increase in core count, the load per rank decreases, while the time spent in collective operations increase…
▽ More
Collective operations are common features of parallel programming models that are frequently used in High-Performance (HPC) and machine/ deep learning (ML/ DL) applications. In strong scaling scenarios, collective operations can negatively impact the overall application performance: with the increase in core count, the load per rank decreases, while the time spent in collective operations increases logarithmically.
In this article, we propose a design for eventually consistent collectives suitable for ML/ DL computations by reducing communication in Broadcast and Reduce, as well as by exploring the Stale Synchronous Parallel (SSP) synchronization model for the Allreduce collective. Moreover, we also enrich the GASPI ecosystem with frequently used classic/ consistent collective operations -- such as Allreduce for large messages and AlltoAll used in an HPC code. Our implementations show promising preliminary results with significant improvements, especially for Allreduce and AlltoAll, compared to the vendor-provided MPI alternatives.
△ Less
Submitted 31 March, 2022;
originally announced March 2022.
-
Cost-Aware Automatic Program Repair
Authors:
Roopsha Samanta,
Oswaldo Olivo,
E. Allen Emerson
Abstract:
We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates…
▽ More
We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a " cost-aware" formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstraction-based solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs.
△ Less
Submitted 31 March, 2014; v1 submitted 27 July, 2013;
originally announced July 2013.
