A means for translating MCNP5 input files into a form that can be run by Mercury, a modern Monte Carlo particle transport code, will allow MCNP5 users to more easily take advantage of the high-performance computing benefits ...

For narrowing with a set of rules \Delta modulo a set of axioms B almost nothing is known about terminating narrowing strategies, and basic narrowing is known to be incomplete for B=AC. In this work we ask and answer the ...

Decision procedures can be either theory-specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure ...

Although different satisfiability decision procedures can be combined by algorithms such as those of Nelson-Oppen or Shostak, current tools typically can only support a finite number of theories to use in such ...

Both the measurement and simulation of unsteady flow yield huge datasets of time-varying volumetric vector fields. Flow dynamics researchers face the very difficult task of finding, extracting and analyzing important flow ...

Cyber-physical systems (CPS) use networked control software to interact with and manipulate the physical world. Examples of cyber-physical systems include smart buildings, power distribution networks, and fleets of autonomous ...

This report describes our effort to model and verify the Casper blockchain finality system in the Coq proof assistant. We outline the salient details on blockchain systems using Casper, describe previous verification ...

We consider the problem of verifying the security of finitely many sessions of a protocol that tosses coins in addition to standard cryptographic primitives against a Dolev-Yao adversary. Two properties are investigated ...

Finally, we present incremental state space exploration (ISSE), a technique that aims to provide a speedup in the state space exploration time of evolving simulation models; i.e., simulation models whose code changes from ...

Verification and Validation (V&V) is a critically important phase in the development life cycle of a simulation model. In the context of network simulation, traditional network simulators perform well in using a simulation ...