arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Eric Mercer

58 papers · 2001–2024

2001: 22002: 32003: 42004: 12005: 32006: 12007: 32008: 22009: 72010: 12011: 22012: 32013: 22014: 42015: 62016: 12017: 02018: 32019: 22020: 22021: 12022: 32023: 12024: 1
2001peak 7 in 20092024

Frequent co-authors

Papers

showing 1–25 of 58 RSS

Synchronous interlocked pipelines

Hans M. Jacobson, Prabhakar Kudva, Pradip Bose +4 more

Hardware and Architecture · · cited 86× · DOI ↗ · more like this ·

Locality principles are becoming paramount in controlling advancement of data through pipelined systems. Achieving fine grained power down and progressive pipeline stalls at the local stage level is therefore becoming increasingly, important to enable lower dynamic power consumption while keeping introduced switching noise under control as well as avoiding global distribution of timing critical stall signals. It has long been known that the interlocking properties of as asynchronous pipelined systems have a potential to provide such benefits. However it has not been understood how such interlocking can be achieved in synchronous pipelines. This paper presents a novel technique based on local clock gating and synchronous handshake protocols that achieves stage level interlocking characteristics in synchronous pipelines similar to that of asynchronous pipelines. The presented technique is…

Load Balancing Parallel Explicit State Model Checking

Rahul Kumar, Eric Mercer

Computational Theory and Mathematics · Electronic Notes in Theoretical Computer Science · · cited 55× · DOI ↗ · more like this ·

This paper first identifies some of the key concerns about the techniques and algorithms developed for parallel model checking; specifically, the inherent problem with load balancing and large queue sizes resultant in a static partition algorithm. This paper then presents a load balancing algorithm to improve the run time performance in distributed model checking, reduce maximum queue size, and reduce the number of states expanded before error discovery. The load balancing algorithm is based on generalized dimension exchange (GDE). This paper presents an empirical analysis of the GDE based load balancing algorithm on three different supercomputing architectures—distributed memory clusters, Networks of Workstations (NOW) and shared memory machines. The analysis shows increased speedup, lower maximum queue sizes and fewer total states explored before error discovery on each of the…

MCC: A runtime verification tool for MCAPI user applications

Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer +1 more

Computational Theory and Mathematics · ScholarsArchive (Brigham Young University) · · cited 25× · DOI ↗ · more like this ·

We present a dynamic verification tool MCC for Multicore Communication API applications - a new API for communication among cores. MCC systematically explores all relevant interleavings of an MCAPI application using a tailor-made dynamic partial order reduction algorithm (DPOR). Our contributions are (i) a way to model the non-overtaking message matching relation underlying MCAPI calls with a high level algorithm to effect DPOR for MCAPI that controls the lower level details so that the intended executions happen at runtime; and (ii) a list of default safety properties that can be utilized in the process of verification. To our knowledge, this is the first push button model checker for MCAPI application writers that, at present, deals with an interesting subset of MCAPI calls. Our result is the demonstration that we can indeed develop a dynamic model checker for MCAPI that can directly…

Modular verification of timed circuits using automatic abstraction

Hao Zheng, Eric Mercer, C. Myers

Computational Theory and Mathematics · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · · cited 25× · DOI ↗ · more like this ·

The major barrier that prevents the application of formal verification to large designs is state explosion. This paper presents a new approach for verification of timed circuits using automatic abstraction. This approach partitions the design into modules, each with constrained complexity. Before verification is applied to each individual module, irrelevant information to the behavior of the selected module is abstracted away. This approach converts a verification problem with big exponential complexity to a set of subproblems, each with small exponential complexity. Experimental results are promising in that they indicate that our approach has the potential of completing much faster while using less memory than traditional flat analysis.

Clash of the Titans

Neha Rungta, Eric Mercer

Software · · cited 19× · DOI ↗ · more like this ·

In this work we focus on creating a benchmark suite of concurrent programs for various programming languages to evaluate the bug detection capabilities of various tools and techniques. We have compiled a set of Java benchmarks from various sources and our own efforts. For many of the Java examples we have created equivalent C# programs. All the benchmarks are available for download. In our multi-language benchmark suite we compare results from various tools: CalFuzzer, ConTest, CHESS, and Java Pathfinder. In Java Pathfinder we provide extensive results for state-less random walk, randomized depth-first search, and guided search using abstraction refinement. Using data from our study we argue that iterative context-bounding and dynamic partial order reduction are not sufficient to render model checking for testing concurrent programs tractable and secondary techniques such as guidance…

Improved POSET Timing Analysis in Timed Petri Nets

Eric Mercer, Chris J. Myers, Tomohiro Yoneda

Computational Theory and Mathematics · Molecular Immunology · · cited 16× · DOI ↗ · more like this ·

Phosphoglucomutase 3 (PGM3) protein catalyzes the conversion of N-acetyl-d-glucosamine-6-phosphate (GlcNAc-6-P) to N-acetyl-d-glucosamine-1-phosphate (GlcNAc-1-P), which is required for the synthesis of uridine diphosphate N-acetylglucosamine (UDP-GlcNAc) an important precursor for protein glycosylation. Mutations in PGM3 gene have been recently shown to underlie a new congenital disorder of glycosylation often associated to elevated IgE. Herein, we report twelve PGM3 deficient patients. They belong to three highly consanguineous families, originating from a rural district in the west central Tunisia. The patient's clinical phenotype is characterized by severe respiratory and cutaneous infections as well as developmental delay and severe mental retardation. Fourteen patients died in early infancy before diagnosis supporting the severity of the clinical phenotype. Laboratory findings…

Improving Translation of Live Sequence Charts to Temporal Logic

Rahul Kumar, Eric Mercer, A.S. Bunker

Computational Theory and Mathematics · Electronic Notes in Theoretical Computer Science · · cited 15× · DOI ↗ · more like this ·

An efficient and mathematically rigorous translation from Live Sequence Charts (LSCs) to temporal logic is essential to providing an end-to-end specification and verification method for System on Chip (SoC) protocols. Without mathematical rigor, no translation can be trusted to completely represent the LSC specification, while inefficiency renders even provably sound translations useless in verifying the correctness of industrial-strength protocols. Previous work shows that the LSC-to-temporal logic and LSC-to-automata translations can be automated and formalized for the LSC language. In the LSC-to-temporal logic translation, the extraordinary size of the resulting formula limits the scalability of the charts that can be translated and verified. Our work, on the other hand, leverages intuitive temporal logic reductions to generate a formula that is at most quadratic in the size of the…

A context-sensitive structural heuristic for guided search model checking

Neha Rungta, Eric Mercer

Computational Theory and Mathematics · ScholarsArchive (Brigham Young University) · · cited 13× · DOI ↗ · more like this ·

In this paper we build on the FSM distance heuristic for guided model checking by using the runtime stack to reconstruct calling context in procedural calls. We first build a more accurate static representation of the program by including a bounded level of calling context. We then use the calling context in the runtime stack with the more accurate control flow graph to estimate the distance to the possible error state. The heuristic is computed using both the dynamic and static construction of the program. We evaluate the new heuristic on models with concurrency errors. In these examples, experimental results show that for programs with function calls, the new heuristic better guides the search toward the error while the traditional FSM distance heuristic degenerates into a random search.

GEESE

Aadesh Neupane, Michael A. Goodrich, Eric Mercer

Artificial Intelligence · Proceedings of the Genetic and Evolutionary Computation Conference · · cited 12× · DOI ↗ · more like this ·

Animals such as bees, ants, birds, fish, and others are able to perform complex coordinated tasks like foraging, nest-selection, flocking and escaping predators efficiently without centralized control or coordination. Conventionally, mimicking these behaviors with robots requires researchers to study actual behaviors, derive mathematical models, and implement these models as algorithms. We propose a distributed algorithm, Grammatical Evolution algorithm for Evolution of Swarm bEhaviors (GEESE), which uses genetic methods to generate collective behaviors for robot swarms. GEESE uses grammatical evolution to evolve a primitive set of human-provided rules into productive individual behaviors. The GEESE algorithm is evaluated in two different ways. First, GEESE is compared to state-of-the-art genetic algorithms on the canonical Santa Fe Trail problem. Results show that GEESE outperforms the…

Hardness for Explicit State Software Model Checking Benchmarks

Neha Rungta, Eric Mercer

Computational Theory and Mathematics · ScholarsArchive (Brigham Young University) · · cited 12× · DOI ↗ · more like this ·

Directed model checking algorithms focus computation resources in the error-prone areas of concurrent systems. The algorithms depend on some empirical analysis to report their performance gains. Recent work characterizes the hardness of models used in the analysis as an estimated number of paths in the model that contain an error. This hardness metric is computed using a stateless random walk. We show that this is not a good hardness metric because models labeled hard with a stateless random walk metric have easily discoverable errors with a stateful randomized search. We present an analysis which shows that a hardness metric based on a stateful randomized search is a tighter bound for hardness in models used to benchmark explicit state directed model checking techniques. Furthermore, we convert easy models into hard models as measured by our new metric by pushing the errors deeper in…

Synthesizing Verified Components for Cyber Assured Systems Engineering

Eric Mercer, Konrad Slind, Isaac Amundson +3 more

Computational Theory and Mathematics · · cited 11× · DOI ↗ · more like this ·

Cyber-physical systems, such as avionics, must be tolerant to cyber-attacks in the same way they are tolerant to random faults: they either gracefully recover or safely shut down as requirements dictate. The DARPA Cyber Assured Systems Engineering program is developing tools for design, analysis, and verification that enable systems engineers to design-in cyber-resiliency in a Model-Based Systems Engineering environment. This paper describes automated model transformations that introduce high-assurance cyber-resiliency components into a system, in particular filters and monitors that prevent malicious input and detect supply chain attacks, respectively. A formal specification defines each high-assurance component, and is used to verify that the component addresses system level cyber requirements. Implementations for these high-assurance components are directly synthesized from their…

Proving MCAPI executions are correct using SMT

Yu Huang, Eric Mercer, Jay McCarthy

Computational Theory and Mathematics · · cited 11× · DOI ↗ · more like this ·

Asynchronous message passing is an important paradigm in writing applications for embedded heterogeneous multicore systems. The Multicore Association (MCA), an industry consortium promoting multicore technology, is working to standardize message passing into a single API, MCAPI, for bare metal implementation and portability across platforms. Correctness in such an API is difficult to reason about manually, and testing against reference solutions is equally difficult as reference solutions implement an unknown set of allowed behaviors, and programmers have no way to directly control API internals to expose or reproduce errors. This paper provides a way to encode an MCAPI execution as a Satisfiability Modulo Theories (SMT) problem, which if satisfiable, yields a feasible execution schedule on the same trace, such that it resolves non-determinism in the MCAPI runtime in a way that it now…

An Improved Distance Heuristic Function for Directed Software Model Checking

Neha Rungta, Eric Mercer

Software · ScholarsArchive (Brigham Young University) · · cited 11× · DOI ↗ · more like this ·

State exploration in directed software model checking is guided using a heuristic function to move states near errors to the front of the search queue. Distance heuristic functions rank states based on the number of transitions needed to move the current program state into an error location. Lack of calling context information causes the heuristic function to underestimate the true distance to the error; however, inlining functions at call sites in the control flow graph to capture calling context leads to an exponential growth in the computation. This paper presents a new algorithm that implicitly inlines functions at call sites to compute distance data with unbounded calling context that is polynomial in the number of nodes in the control flow graph. The new algorithm propagates distance data through call sites during a depth-first traversal of the program. We show in a series of…

CORRECTNESS AND REDUCTION IN TIMED CIRCUIT ANALYSIS

Eric Mercer, Chris J. Myers, Peter A. Beerel +5 more

Computational Theory and Mathematics · AORN Journal · · cited 10× · DOI ↗ · more like this ·

To increase performance, circuit designers are experimenting with timed circuits -- a class of circuits that rely on a complex set of timing constraints for correct functionality. This is evidenced in published experimental designs from industry. Timing constraints are key to the success of these designs, and algorithms to verify timing constraints are required to make them practical in commercial applications. Due to the complexity of the constraints, however, traditional static timing analysis is not adequate. Timed state space analysis is required; thus, improved timed state space analysis is paramount to producing efficient timed circuits. This diss

JPF verification of habanero Java programs

Peter Anderson, Brandon Chase, Eric Mercer

Hardware and Architecture · ACM SIGSOFT Software Engineering Notes · · cited 9× · DOI ↗ · more like this ·

Habanero Java (HJ), a mid-level concurrent language, provides several correctness advantages if it is data race free: deadlock freedom, determinism, serialization, etc. An HJ program execution can only demonstrate data race freedom for one scheduling path, but the correctness property only holds if it is data race free for all paths. Verifying an HJ program with a tool such as Java Path Finder (JPF) for complete data race freedom is time and memory consuming because of the numerous JPF state expansions. This paper provides a small, stand-alone, alternative, HJ verification runtime (VR) that is more suited for verification in JPF. Additionally, this paper presents an alternative JPF scheduler that will explore only relevant HJ related scheduling paths in the VR. Finally, this paper shows state expansion results in JPF using HJ benchmarks with the HJ library, VR with and without the…

Design, verification and applications of a new read-write lock algorithm

Jun Shirako, Nick Vrvilo, Eric Mercer +1 more

Computer Networks and Communications · · cited 9× · DOI ↗ · more like this ·

Coordination and synchronization of parallel tasks is a major source of complexity in parallel programming. These constructs take many forms in practice including directed barrier and point-to-point synchronizations, termination detection of child tasks, and mutual exclusion in accesses to shared resources.

Guided model checking for programs with polymorphism

Neha Rungta, Eric Mercer

Software · · cited 9× · DOI ↗ · more like this ·

Exhaustive model checking search techniques are ineffective for error discovery in large and complex multi-threaded software systems. Distance estimate heuristics guide the concrete execution of the program toward a possible error location. The estimate is a lower-bound computed on a statically generated abstract model of the program that ignores all data values and only considers control flow. In this paper we describe a new distance estimate heuristic that efficiently computes a tighter lower-bound in programs with polymorphism when compared to the state of the art distance heuristic. We statically generate conservative distance estimates and refine the estimates when the targets of dynamic method invocations are resolved. In our empirical analysis the state of the art approach is computationally infeasible for large programs with polymorphism while our new distance heuristic can…

Vector-clock based partial order reduction for JPF

Eric S. Noonan, Eric Mercer, Neha Rungta

Computational Theory and Mathematics · ACM SIGSOFT Software Engineering Notes · · cited 8× · DOI ↗ · more like this ·

Java Pathfinder (JPF) employs a dynamic partial order reduction based on sharing and state hashing to reduce the schedules in concurrent systems. That partial order reduction is believed to be complete in the new version of JPF using search global IDs (SGOIDs) but does miss behaviors when SGOIDs are not employed. More importantly, it is not clear how such a dynamic partial order reduction, with or without SGOIDs, compares to other dynamic partial order reductions based on persistent sets, sleep sets, or clock vectors. In order to understand JPF's native dynamic partial order reduction better, this paper discusses an implementation of Flanagan and Goidefroid's clock vector partial order reduction in JPF. Then, the performance of JPF's native dynamic partial order reduction and the clock vector partial order reduction in JPF using SGOIDs will be compared in an effort to understand JPF's…

Or Best Offer: A Privacy Policy Negotiation Protocol

Daniel D. Walker, Eric Mercer, Kent Seamons

Sociology and Political Science · ScholarsArchive (Brigham Young University) · · cited 8× · DOI ↗ · more like this ·

Privacy policy languages, such as P3P, allow websites to publish their privacy practices and policies in machine readable form. Currently, software agents designed to protect users' privacy follow a "take it or leave it" approach that is inflexible and gives the server ultimate control. Privacy policy negotiation is one approach to leveling the playing field by allowing a client to negotiate with a server to determine how that server collects and uses the client's data. We present a privacy policy negotiation protocol, "Or Best Offer", that includes a formal model for specifying privacy preferences and reasoning about privacy policies. The protocol is guaranteed to terminate within three rounds of negotiation while producing policies that are Pareto-optimal, and thus fair to both the client and the server.

Improving Live Sequence Chart to Automata Transformation for Verification

Rahul Kumar, Eric Mercer

Software · ScholarsArchive (Brigham Young University) · · cited 7× · DOI ↗ · more like this ·

This paper presents a Live Sequence Chart (LSC) to automata transformation algorithm that enables the verification of communication protocol implementations. Using this LSC to automata transformation a communication protocol implementation can be verified using a single verification run as opposed to previous techniques that rely on a three stage verification approach. The novelty and simplicity of the transformation algorithm lies in its placement of accept states in the automata generated from the LSC. We present in detail an example of the transformation as well as the transformation algorithm. Further, we present a detailed analysis and an empirical study comparing the verification strategy to earlier work to show the benefits of the improved transformation algorithm.

A standard-cell self-timed multiplier for energy and area critical synchronous systems

Kip Killpack, Eric Mercer, C.J. Meyers

Hardware and Architecture · · cited 7× · DOI ↗ · more like this ·

This paper describes the design of a standard-cell self-timed multiplier for use in energy and area critical synchronous systems. The area of this multiplier is bounded by N rather than N/sup 2/ as seen in more traditional combinational parallel array designs, where N is the word size. Energy has a polynomial growth with word size, but has a coefficient that is much smaller than that seen in a combinational array design. Although the multiplier is self-timed, it can be embedded in a synchronous system appearing as a combinational element. This paper presents latency, area, and energy estimates for the multiplier implemented at various word sizes, and compares these numbers with a traditional combinational array multiplier. The self-timed multiplier uses 1/3 the energy and 1/7 the area of the combinational design for a 24-bit word size.

Modeling complex air traffic management systems

Neha Rungta, Eric Mercer, Franco Raimondi +3 more

Artificial Intelligence · · cited 6× · DOI ↗ · more like this ·

In this work, we propose the use of multi-agent system (MAS) models as the basis for predictive reasoning about various safety conditions and the performance of Air Traffic Management (ATM) Systems. To this end, we describe the engineering of a domain-specific MAS model that provides constructs for creating scenarios related to ATM systems and procedures; we then instantiate the constructs in the ATM model for different scenarios. As a case study we generate a model for a concept that provides the ability to maximize departure throughput at La Guardia airport (LGA) without impacting the flow of the arrival traffic; the model consists of approximately 1.5 hours real time flight data. During this time, between 130 and 150 airplanes are managed by four en-route controllers, three TRACON controllers, and one tower controller at LGA who is responsible for departures and arrivals. The planes…

Computing and visualizing the impact of change with Java PathFinder extensions

Eric Mercer, Suzette Person, Neha Rungta

Information Systems · ACM SIGSOFT Software Engineering Notes · · cited 6× · DOI ↗ · more like this ·

Change impact analysis techniques estimate the potential effects of changes made to software. Directed Incremental Symbolic Execution (DiSE) is a Java PathFinder extension that computes the impact of changes on program execution behaviors. The results of DiSE are a set of impacted path conditions that can be efficiently processed by a subsequent client analysis. Path conditions, however, may not be intuitive for software developers without the context of the source code. In this paper we present a framework for visualizing the results of DiSE. The visualization includes annotated source code and control ow graphs indicating program statements that are changed and statements that may be impacted by the changes. A simulation mode enables users to also observe the impact of changes on symbolic execution of the program, by showing the changes to the path conditions as the user steps through…

Modular Synthesis of Timed Circuits Using Partial Order Reduction

Tomohiro Yoneda, Eric Mercer, Chris J. Myers

Computational Theory and Mathematics · Tokyo Tech Research Repository (Tokyo Institute of Technology) · · cited 6× · OpenAlex ↗ · more like this ·

Abstract — This paper develops a modular synthesis algorithm for timed circuits that is dramatically accelerated by partial order reduction. This algorithm synthesizes each module in a hierarchical design individually. It utilizes partial order reduction to reduce the state space explored for the other modules by considering a single interleaving of concurrently enabled transitions. This approach better manages the state explosion problem resulting in a more than 2 order of magnitude reduction in synthesis time. The improved synthesis time enables the synthesis of a larger class of timed circuits than was previously possible. I.