Publications

This paper introduces the first tool suite built around MoXI, a model-exchange language intended to serve as a common standard for symbolic model checking. The work presents translators into and out of MoXI, an initial benchmark collection, and practical guidance on using and extending the tooling, showing that the approach is useful beyond hardware-only settings and can support future research-community interoperability.

This work targets sequential redundancy removal in hardware designs, where uncovering and eliminating redundant logic can improve the quality and downstream efficiency of verification and optimization flows. The paper advances methods aimed at making redundancy removal more exhaustive in practice, with an emphasis on scaling the analysis while preserving usefulness for industrial sequential circuits.

This paper proposes MoXI, an intermediate language for symbolic model checking designed to improve standardization and open-source interoperability across model-checking tools. Building on SMT-LIB, MoXI is intended to represent verification tasks for hardware, software, and other infinite-state systems while remaining simple enough to support tool translation, experimentation, and broader community adoption.

This paper studies model predictive runtime verification for cyber-physical systems that must satisfy timing constraints in real time. The approach combines runtime monitoring with predictive reasoning so the monitor can forecast impending violations early enough to enable preventive action, and the paper evaluates the idea on a representative CPS setting with hard deadlines.

This paper extends IC3 to learn invariants over internal signals in addition to state variables, addressing cases where compact state-only invariants are hard to derive. The method improves sequential equivalence checking and shows strong results on industrial and competition benchmarks.

This work improves parallel hardware verification for designs with many properties by combining affinity-based partitioning, better work distribution, and less redundant computation. The result is faster verification with lower overall CPU cost across challenging experiments.

This paper speeds up multi-property verification by grouping properties with strong structural and semantic affinity. The grouping strategy improves concurrent solving and enables better reuse of effort across related properties.

This paper introduces assumption-literal heuristics that improve SAT-based bug finding in CAR and related model-checking techniques. The method increases efficiency, exposes different classes of bugs, and transfers to IC3/PDR-style reasoning as well.

This paper presents SimpleCAR, a reference implementation of Complementary Approximate Reachability for safety hardware model checking. The tool is especially effective for bug finding and performs competitively on difficult HWMCC benchmarks.

This paper tackles LTL model checking over large design spaces by exploiting dependencies among related models and properties. Its D3 algorithm prunes unnecessary checks and significantly reduces verification cost while preserving complete results for every model-property pair.

This paper introduces FuseIC3, an incremental verification algorithm for checking related models in a design space. By reusing and repairing learned reachability information across runs, it reduces repeated work and improves scalability on large benchmark sets.

This case study analyzes a hybrid wired and wireless aircraft communication network with attention to safety, security, and availability. Formal modeling and model checking are used to study privacy-preserving communication, fault tolerance, and tradeoffs between bandwidth and resilience.

This journal article extends the FuseIC3 approach to incremental verification across large design spaces. It studies how reusable reachability approximations, model ordering, and property grouping can reduce redundant work and improve scalability when many related models must be checked.

This paper develops a formal framework for analyzing safety, security, and availability in wireless aircraft communication networks. The framework supports model checking, fault analysis, and quantitative tradeoff studies between bandwidth, reliability, and privacy-preserving operation.

This dissertation studies how to scale model checking across large design spaces rather than isolated models. It develops theory, algorithms, and experimental techniques for design-space reduction, incremental verification, multi-property verification, and parallel orchestration, showing how relationships among models and properties can be exploited to improve verification efficiency without sacrificing coverage.

This student-forum paper outlines the challenge of scaling verification when many properties must be checked on the same design. It summarizes early results and future directions on exploiting property relationships, subproblem sharing, and improved orchestration.

This paper presents an early view of the model-set checking problem, where many related system variants must be analyzed together. It motivates algorithms that exploit relationships across models to make design-space verification more scalable.

This paper proposes a formal approach for comparing wired and wireless avionics communication networks from a safety perspective. The framework helps identify failure causes, estimate reliability, and support design decisions about whether wireless alternatives can meet required fault-tolerance levels.

This introductory book provides a practical foundation for working with Stellaris ARM Cortex-M embedded processors. It focuses on helping readers get started with the architecture, development workflow, and hands-on programming concepts needed to build embedded systems on the platform.