My main interest is in the area of Formal Verification of Reactive Systems.

Under the term formal verification we comprise the techniques used to reason formally about the behavior of digital systems. In a general way, the verification problem may be stated as follows: Given a specification of the behavior of a system and an implementation, verify formally that the implementation satisfies the specification. This definition is very general in the sense that there may be different types of specification, different types of implementations, and also, the concept of "satisfaction" may be interpreted in different ways. The main focus of our group is in the area of Model Checking and Language Containment. The former assumes a temporal logic formulation of the specification and it tries to prove that the implementation is a model of the specification. The latter models both the specification and implementation as automata defining languages, and it tries to prove that the language accepted by the implementation is contained on the language accepted by the specification. As an example of where formal verification can be applied is the (in)famous error in the Intel Pentium Chip. The processor computed an incorrect division whenever certain combination of operands were present. Formal verification specifically tries to avoid this kind of error by guaranteeing that the final product is "correct".

Here are some publications related to my work in this area.

Incremental CTL Model Checking Using BDD Subsetting. Abelardo Pardo and Gary Hachtel. Design Automation Conference, 1998, San Francisco, CA, USA.

Automatic Abstraction Techniques for Formal Verification of Digital Systems. Abelardo Pardo. Ph. D. Thesis Dissertation. August 1997.

Automatic Abstraction Techniques for Propositional µ-calculus Model Checking . Abelardo Pardo and Gary Hachtel. Computer Aided Verification, CAV'97. Haifa Israel.

Modular Verification of Multipliers. Kavita Ravi, Abelardo Pardo, Gary Hachtel and Fabio Somenzi. International Conference on Formal Methods for Computer-aided Design. Palo Alto, California, USA. November 1996.

Tearing Based Automatic Abstraction for CTL Model Checking Woohyuk Lee, Abelardo Pardo, Jang-Jae Young, Gary Hachtel and Fabio Somenzi. ICCAD'96, San Jose, USA. (Click here to obtain the submission document.)

VIS: A System for Verification and Synthesis.R.K. Brayton, A. Sangiovanni-Vincentelli, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, S. Qadeer, R.K. Ranjan, T. R. Shiple, G. Swamy, T. Villa, G. D. Hachtel, F. Somenzi, Abelardo Pardo and S. Sarwary. CAV'96. New Jersey, USA.