Mechanizing Proofs of Computation Equivalence. - Marcelo Glusman; Shmuel Katz (CAV, 1999)

Extending Memory Consistency of Finite Prefixes to Infinite Computations. - Marcelo Glusman; Shmuel Katz (CONCUR, 2001)

Model Checking Conformance with Scenario-Based Specifications. - Marcelo Glusman; Shmuel Katz (CAV, 2003)

Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. - Marcelo Glusman; Gila Kamhi; Sela Mador-Haim; Ranan Fraer; Moshe Y. Vardi (TACAS, 2003)

A Mechanized Proof Environment for the Convenient Computations Proof Method. - Marcelo Glusman; Shmuel Katz (Formal Methods Syst. Des., 2003)

Mechanizing proofs of computation equivalence. - Marcelo Glusman (2003)