We present an approach to understanding first-order theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, configurations, and software designs. For the analyses we offer, users are not required to frame formal properties or construct derivations. Rather, they can explore examples of their designs, confirming the expected instances and perhaps recognizing bugs inherent in surprising instances. Key foundational ideas include: the information preorder on models given by homomorphism, an inductively-defined refinement of the Herbrand base of a theory, and a notion of provenance for elements and facts in models. The implementation makes use of SMT-solving and an algorithm for minimization with respect to the information preorder on models. Our approach is embodied in a tool, Razor, that is complete for finite satisfiability and provides a read-eval-print loop used to navigate the set of finite models of a theory and to display provenance.

A Body Area Network (BAN) consists of a set of sensing devices deployed on a person (user) typically for health monitoring purposes. The BAN continuously monitors various physiological and environmental parameters and typically transfers this information to a base station for processing and storage in a back-end medical cloud. Despite the incredible potential that these systems offer, their utilization is largely limited to lab settings. One of the requirements for adoption in the real-world is the ease of deployment and configuration of such systems for the users. Much work has been done in developing middleware-based solutions that enable easy application development for BANs by abstracting out the details of the devices and sensors. However, none of the current approaches extend this capability to the users of the system. What is required is the ability to provide a means to dynamically add diverse devices into the system without requiring substantial reprogramming of the device and the base station. In this paper, we present BAN-PnP, a communication protocol for enabling devices and the base station (or middleware) to communicate effectively with minimal user involvement. The key idea of the protocol is to allow the devices in the BAN to "teach" the base station about their capabilities. By adding a few extra control messages, we are able to transform a traditional BAN into a plug-n-play BAN that is easy for the usually non-tech-savvy users of such systems to deploy. The performance analysis of the BAN-PnP protocol demonstrates that the protocol enables plug-n-play operation of BANs with an affordable increase in overhead.