We demonstrate the “Comparative Prints Suite”, a browser-based family of tools developed for the United States House of Representatives to track changes in United States federal legislation. The tools use a model grammar to parse amendments to bills, execute those amendments into law, and compare versions of bills. The tools are available at to Members and staff in the U.S. House, the Congressional Research Service of the Library of Congress, and other Congressional entities to support the legislative process.

We describe a system to execute U.S. federal bills into law, as part of a working application for the United States House. This system is based on a formal grammar we developed, which achieves greater than 94% accuracy in parsing amendatory phrases in bills; it is in production at the United States House of Representatives and is used to produce official ‘Comparative Print’ reports showing how a bill would amend current law. The grammar consists of two components: CItation Modeling and Processing Language (CIMPL), which captures citations to current law as they are found in bill amendments, and AMendment Processing Language (AMPL), which includes directive language to amend the text referred to by the CIMPL phrase. Here, we describe the analysis that led to development of the grammar, and provide an overview of how the grammar is applied to execute proposed amendments in the Comparative Print Suite of the U.S. House of Representatives. This application is available to all Members and staff at the internal site, compare.house.gov. Both the executable grammar and the full, point-in-time U.S. law dataset upon which they act, are publicly described here in technical detail for the first time.

With the maturing of technology for model checking and constraint solving, there is an emerging opportunity to develop programming tools that can transform the way systems are specified. In this paper, we propose a new way to program distributed protocols using concolic snippets. Concolic snippets are sample execution fragments that contain both concrete and symbolic values. The proposed approach allows the programmer to describe the desired system partially using the traditional model of communicating extended finite-state-machines (EFSM), along with high-level invariants and concrete execution fragments. Our synthesis engine completes an EFSM skeleton by inferring guards and updates from the given fragments which is then automatically analyzed using a model checker with respect to the desired invariants. The counterexamples produced by the model checker can then be used by the programmer to add new concrete execution fragments that describe the correct behavior in the specific scenario corresponding to the counterexample.

Memory consistency litmus tests are small parallel programs that are designed to illustrate subtle differences between memory consistency models by exhibiting different outcomes for different models. In this paper, we show that for a class of memory models that is restricted yet expressive enough to include all store-atomic hardware memory models, litmus tests of a bounded size are sufficient for illustrating differences between memory consistency models in this class. We establish a bound of two threads and no more than six memory access instructions for differentiating litmus tests in this class of models. Thus, we can prove equivalence of two specification of memory consistency models in this class by exploring a bounded number of litmus tests. We build a tool for comparing memory models based on this result, and we use the tool to explore and map the space of this class of models.