My current research is in Model Checking techniques. A model checking technique is defined as the use of an algorithmic technique to verify that the behavior of a sequential system (hardware, software or a combination of hardware and software) is complying with its specifications. Model checking automatically verifies the temporal specifications of the sequential system by exploring its reachable states. If the sequential system fails to satisfy a specification, the model checking technique generates a counterexample in a form of a sequence of states that witnesses the failing of the specification.

My main interest is in proving termination in Bounded Model Checking (BMC). Bounded model checking is an LTL model checking technique that uses SAT solvers to search for a bounded-length counterexample to an LTL property. Finding counterexamples is significantly important in helping debugging a structure model. However, the knowledge that no counterexamples exist up to a certain length may help to terminate the search soon and conclude that the property passes.

1. "Proving More Properties with Bounded Model Checking," M. Awedh and F. Somenzi. Sixteenth Conference on Computer Aided Verification (CAV'04), Boston, MA, July 2004. Download
2. "Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States," M. Awedh and F. Somenzi. Formal Methods in Computer Aided Design (FMCAD'04), Austin, TX, November 2004. Download
3. "CirCUs: A Satisfiability Solver Geared Towards Bounded Model Checkin," H. Jin and M. Awedh and F. Somenzi. Sixteenth Conference on Computer Aided Verification (CAV'04), Boston, MA, July 2004. Download
4. "Termination Criteria for Bounded Model Checking: Extensions and Comparison," M. Awedh and F. Somenzi. Third International Workshop on Bounded Model Checking (BMC'05), July 11, 2005, The University of Edinburgh, Scotland, UK. Download
5. "Automatic Invariant Strengthening to Prove Properties in Bounded Model Checking," M. Awedh and F. Somenzi. To appear Download

1. "Symbolic Model Checking without BDDs," A. Biere and A. Cimatti and E. Clarke and Y. Zhu. Fifth International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99), Amsterdam, The Netherlands.
2. "Symbolic Model Checking Using SAT Procedures Instead of BDDs," A. Biere and A. Cimatti and E. Clarke and M. Fujita and Y. Zhu. DAC,
3. "A Fixpoint Based Encoding for Bounded Model Checking," A. Frisch and D. Sheridan and T. Walsh. Formal Methods in Computer Aided Design, 2002
4. "Simple Bounded LTL Model Checking," T. Latvala and A. Biere and K. Helijanko and T. Junttil. Formal Methods in Computer Aided Desig, Austin, TX, 2004
5. "Checking Safety Properties Using Induction and a SAT-Solver," M. Sheeran and S. Singh and G. Stalmarck. Formal Methods in Computer Aided Desig, 2000
6. "Benefits of Bounded Model Checking at an Industrial Setting, " G. Berry and H. Comon and A. Finkel, Thirteenth Conference on Computer Aided Verification (CAV'01), 2001

• VIS home page
• CAV Conferences
• University of Colorado at Boulder
• Department of Electrical and Computer Engineering
• Department of Computer Science

• ECEN5129
• ECEN5139