Rohit Dureja, PhD

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 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 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 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.