2015
Democratization of Formal Verification with Collective Intelligence.
Proceedings of the Formal Methods in Computer-Aided Design, 2015
2014
Challenging problems in industrial formal verification.
Proceedings of the Formal Methods in Computer-Aided Design, 2014
2012
Formal Analysis of Security Data Paths in RTL Design.
Proceedings of the Hardware and Software: Verification and Testing, 2012
2011
A symbolic execution framework for algorithm-level modelling and verification of computer microarchitecture.
PhD thesis, 2011
2009
A symbolic execution framework for algorithm-level modelling.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2009
2007
Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver.
Proceedings of the Theory and Applications of Satisfiability Testing, 2007
Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification.
Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007
Abstract Modeling and Formal Verification of Microprocessors.
Proceedings of the Computer Science, 2007
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007
An Efficient Diagnostic Test Pattern Generation Framework Using Boolean Satisfiability.
Proceedings of the 16th Asian Test Symposium, 2007
2006
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction.
Proceedings of the Theory and Applications of Satisfiability Testing, 2006
Post-reboot Equivalence and Compositional Verification of Hardware.
Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006
Generation of shorter sequences for high resolution error diagnosis using sequential SAT.
Proceedings of the 2006 Conference on Asia South Pacific Design Automation: ASP-DAC 2006, 2006
2005
Encoding RTL Constructs for MathSAT: a Preliminary Report.
Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005
A Clause-Based Heuristic for SAT Solvers.
Proceedings of the Theory and Applications of Satisfiability Testing, 2005
Bounded Model Checking with QBF.
Proceedings of the Theory and Applications of Satisfiability Testing, 2005
Simultaneous SAT-Based Model Checking of Safety Properties.
Proceedings of the Hardware and Software Verification and Testing, 2005
Space-Efficient Bounded Model Checking.
Proceedings of the 2005 Design, 2005
2004
A Signal Correlation Guided Circuit-SAT Solver.
J. Univers. Comput. Sci., 2004
Parallel Multithreaded Satisfiability Solver: Design and Implementation.
Proceedings of the 3rd International Workshop on Parallel and Distributed Methods in Verification, 2004
Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints.
Proceedings of the 2004 International Conference on Computer-Aided Design, 2004
2003
Design automation with mixtures of proof strategies for propositional logic.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003
SAT-based methods for sequential hardware equivalence verification without synchronization.
Proceedings of the First International Workshop on Bounded Model Checking, 2003
A signal correlation guided ATPG solver and its applications for solving difficult industrial cases.
Proceedings of the 40th Design Automation Conference, 2003
2002
High capacity and automatic functional extraction tool for industrial VLSI circuit designs.
Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, 2002
Alignability equivalence of synchronous sequential circuits.
Proceedings of the Seventh IEEE International High-Level Design Validation and Test Workshop 2002, 2002
TRANS: efficient sequential verification of loop-free circuits.
Proceedings of the Seventh IEEE International High-Level Design Validation and Test Workshop 2002, 2002
A proof engine approach to solving combinational design automation problems.
Proceedings of the 39th Design Automation Conference, 2002
2001
An enhanced cut-points algorithm in formal equivalence verification.
Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop 2001, 2001
CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001