Author of the publication

TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories.

, and . Int. J. Embed. Syst., 1 (1/2): 134-149 (2005)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Encoding Global Unobservability for Efficient Translation to SAT.. SAT, (2004)TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories., and . Int. J. Embed. Syst., 1 (1/2): 134-149 (2005)Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation., and . ASIAN, volume 1345 of Lecture Notes in Computer Science, page 18-31. Springer, (1997)Using positive equality to prove liveness for pipelined microprocessors.. ASP-DAC, page 316-321. IEEE Computer Society, (2004)Efficient translation of boolean formulas to CNF in formal verification of microprocessors.. ASP-DAC, page 310-315. IEEE Computer Society, (2004)Automatic Abstraction of Equations in a Logic of Equality.. TABLEAUX, volume 2796 of Lecture Notes in Computer Science, page 196-213. Springer, (2003)Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs.. ITC, page 138-147. IEEE Computer Society, (2003)Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors.. DATE, page 266-271. IEEE Computer Society, (2004)Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic., and . CHARME, volume 1703 of Lecture Notes in Computer Science, page 37-53. Springer, (1999)Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality., and . HLDVT, page 8-13. IEEE Computer Society, (2009)