My area of work is related to automated synthesis and optimization, validation and verification of digital VLSI systems:

• Formal Verification of Hardware Implementations of Cryptography Primitives
  • Verification over Galois Fields using Computer Algebra and Algebraic Geometry
  • Canonical Word-Level Polynomial Abstractions of Bit-Vector Arithmetic using Groebner Bases
• Application of Finite Ring Algebra to Synthesis and Verification of Arithmetic Datapaths with Finite Word-Length Operands:
  • Modeling Bit-Vector Arithmetic as Polynomial Functions over Finite Integer Rings
  • Decision Procedures based on Algorithmic Analysis of Polynomial Ideals and their Varieties
• Design Automation for Optic/Photonic Logic
  • Logic Design and Synthesis in Si-Photonics
  • Physical Design Automation for Si-Photonics Integration
  • Thermal issues in Si-Photonics Design Automation
• Formal Verification of RTL descriptions
  • Equivalence Checks, RTL-Satisfiability, Assertion Checking.
• New Techniques to Guide CNF-SAT Search:
  • Static and Dynamic Variable Orderings, Constraint Partitioning
  • Proving UNSAT by Directly Searching for UNSAT Cores.
• Using Groebner's Proof Systems for Simplification of Design Verification and SAT solving.