Showing 1–2 of 2 results for author: Shinn, M
-
Refinement type contracts for verification of scientific investigative software
Authors:
Maxwell Shinn
Abstract:
Our scientific knowledge is increasingly built on software output. User code which defines data analysis pipelines and computational models is essential for research in the natural and social sciences, but little is known about how to ensure its correctness. The structure of this code and the development process used to build it limit the utility of traditional testing methodology. Formal methods…
▽ More
Our scientific knowledge is increasingly built on software output. User code which defines data analysis pipelines and computational models is essential for research in the natural and social sciences, but little is known about how to ensure its correctness. The structure of this code and the development process used to build it limit the utility of traditional testing methodology. Formal methods for software verification have seen great success in ensuring code correctness but generally require more specialized training, development time, and funding than is available in the natural and social sciences. Here, we present a Python library which uses lightweight formal methods to provide correctness guarantees without the need for specialized knowledge or substantial time investment. Our package provides runtime verification of function entry and exit condition contracts using refinement types. It allows checking hyperproperties within contracts and offers automated test case generation to supplement online checking. We co-developed our tool with a medium-sized ($\approx$3000 LOC) software package which simulates decision-making in cognitive neuroscience. In addition to hel** us locate trivial bugs earlier on in the development cycle, our tool was able to locate four bugs which may have been difficult to find using traditional testing methods. It was also able to find bugs in user code which did not contain contracts or refinement type annotations. This demonstrates how formal methods can be used to verify the correctness of scientific software which is difficult to test with mainstream approaches.
△ Less
Submitted 1 September, 2019;
originally announced September 2019.
-
Versatility of nodal affiliation to communities
Authors:
Maxwell Shinn,
Rafael Romero-Garcia,
Jakob Seidlitz,
František Váša,
Petra E. Vértes,
Edward Bullmore
Abstract:
Graph theoretical analysis of the community structure of networks attempts to identify the communities (or modules) to which each node affiliates. However, this is in most cases an ill-posed problem, as the affiliation of a node to a single community is often ambiguous. Previous solutions have attempted to identify all of the communities to which each node affiliates. Instead of taking this approa…
▽ More
Graph theoretical analysis of the community structure of networks attempts to identify the communities (or modules) to which each node affiliates. However, this is in most cases an ill-posed problem, as the affiliation of a node to a single community is often ambiguous. Previous solutions have attempted to identify all of the communities to which each node affiliates. Instead of taking this approach, we introduce versatility, $V$, as a novel metric of nodal affiliation: $V \sim 0$ means that a node is consistently assigned to a specific community; $V \gg 0$ means it is inconsistently assigned to different communities. Versatility works in conjunction with existing community detection algorithms, and it satisfies many theoretically desirable properties in idealised networks designed to maximise ambiguity of modular decomposition. The local minima of global mean versatility identified the resolution parameters of a hierarchical community detection algorithm that least ambiguously decomposed the community structure of a social (karate club) network and the mouse brain connectome. Our results suggest that nodal versatility is useful in quantifying the inherent ambiguity of modular decomposition.
△ Less
Submitted 2 January, 2017;
originally announced January 2017.
