The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Miroslav N. Velev: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Miroslav N. Velev, Randal E. Bryant
    Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. [Citation Graph (0, 0)][DBLP]
    ACSD, 1998, pp:200-212 [Conf]
  2. Miroslav N. Velev
    Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors. [Citation Graph (0, 0)][DBLP]
    AMAI, 2004, pp:- [Conf]
  3. Randal E. Bryant, Miroslav N. Velev
    Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. [Citation Graph (0, 0)][DBLP]
    ASIAN, 1997, pp:18-31 [Conf]
  4. Miroslav N. Velev
    Efficient translation of boolean formulas to CNF in formal verification of microprocessors. [Citation Graph (0, 0)][DBLP]
    ASP-DAC, 2004, pp:310-315 [Conf]
  5. Miroslav N. Velev
    Using positive equality to prove liveness for pipelined microprocessors. [Citation Graph (0, 0)][DBLP]
    ASP-DAC, 2004, pp:316-321 [Conf]
  6. Miroslav N. Velev
    Comparison of schemes for encoding unobservability in translation to SAT. [Citation Graph (0, 0)][DBLP]
    ASP-DAC, 2005, pp:1056-1059 [Conf]
  7. Randal E. Bryant, Steven M. German, Miroslav N. Velev
    Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. [Citation Graph (0, 0)][DBLP]
    CAV, 1999, pp:470-482 [Conf]
  8. Randal E. Bryant, Miroslav N. Velev
    Boolean Satisfiability with Transitivity Constraints. [Citation Graph (0, 0)][DBLP]
    CAV, 2000, pp:85-98 [Conf]
  9. Miroslav N. Velev
    Formal Verification of VLIW Microprocessors with Speculative Execution. [Citation Graph (0, 0)][DBLP]
    CAV, 2000, pp:296-311 [Conf]
  10. Miroslav N. Velev, Randal E. Bryant
    EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. [Citation Graph (0, 0)][DBLP]
    CAV, 2001, pp:235-240 [Conf]
  11. Miroslav N. Velev, Randal E. Bryant, Alok Jain
    Efficient Modeling of Memory Arrays in Symbolic Simulation. [Citation Graph (0, 0)][DBLP]
    CAV, 1997, pp:388-399 [Conf]
  12. Miroslav N. Velev
    Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. [Citation Graph (0, 0)][DBLP]
    CHARME, 2005, pp:97-113 [Conf]
  13. Miroslav N. Velev, Randal E. Bryant
    Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. [Citation Graph (0, 0)][DBLP]
    CHARME, 1999, pp:37-53 [Conf]
  14. Miroslav N. Velev, Randal E. Bryant
    Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. [Citation Graph (0, 0)][DBLP]
    DAC, 2000, pp:112-117 [Conf]
  15. Miroslav N. Velev, Randal E. Bryant
    Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. [Citation Graph (0, 0)][DBLP]
    DAC, 2001, pp:226-231 [Conf]
  16. Miroslav N. Velev, Randal E. Bryant
    Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. [Citation Graph (0, 0)][DBLP]
    DAC, 1999, pp:397-401 [Conf]
  17. Miroslav N. Velev
    Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. [Citation Graph (0, 0)][DBLP]
    DATE, 2002, pp:28-35 [Conf]
  18. Miroslav N. Velev
    Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors. [Citation Graph (0, 0)][DBLP]
    DATE, 2004, pp:266-271 [Conf]
  19. Miroslav N. Velev, Randal E. Bryant
    Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. [Citation Graph (0, 0)][DBLP]
    FMCAD, 1998, pp:18-35 [Conf]
  20. Miroslav N. Velev
    Efficient formal verification of pipelined processors with instruction queues. [Citation Graph (0, 0)][DBLP]
    ACM Great Lakes Symposium on VLSI, 2004, pp:92-95 [Conf]
  21. Miroslav N. Velev
    Comparative Study of Strategies for Formal Verification of High-Level Processors. [Citation Graph (0, 0)][DBLP]
    ICCD, 2004, pp:119-124 [Conf]
  22. Miroslav N. Velev
    A new generation of ISCAS benchmarks from formal verification of high-level microprocessors. [Citation Graph (0, 0)][DBLP]
    ISCAS (5), 2004, pp:213-216 [Conf]
  23. Miroslav N. Velev
    Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction. [Citation Graph (0, 0)][DBLP]
    ISQED, 2006, pp:51-56 [Conf]
  24. Miroslav N. Velev
    Formal Verification of Pipelined Microprocessors with Delayed Branches. [Citation Graph (0, 0)][DBLP]
    ISQED, 2006, pp:296-299 [Conf]
  25. Miroslav N. Velev
    Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs. [Citation Graph (0, 0)][DBLP]
    ITC, 2003, pp:138-147 [Conf]
  26. Sudarshan K. Srinivasan, Miroslav N. Velev
    Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions. [Citation Graph (0, 0)][DBLP]
    MEMOCODE, 2003, pp:65-74 [Conf]
  27. Miroslav N. Velev
    Encoding Global Unobservability for Efficient Translation to SAT. [Citation Graph (0, 0)][DBLP]
    SAT, 2004, pp:- [Conf]
  28. Randal E. Bryant, Steven M. German, Miroslav N. Velev
    Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. [Citation Graph (0, 0)][DBLP]
    TABLEAUX, 1999, pp:1-13 [Conf]
  29. Miroslav N. Velev
    Automatic Abstraction of Equations in a Logic of Equality. [Citation Graph (0, 0)][DBLP]
    TABLEAUX, 2003, pp:196-213 [Conf]
  30. Miroslav N. Velev
    Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. [Citation Graph (0, 0)][DBLP]
    TACAS, 2001, pp:252-267 [Conf]
  31. Miroslav N. Velev, Randal E. Bryant
    Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. [Citation Graph (0, 0)][DBLP]
    TACAS, 1998, pp:136-150 [Conf]
  32. Randal E. Bryant, Miroslav N. Velev
    Boolean Satisfiability with Transitivity Constraints [Citation Graph (0, 0)][DBLP]
    CoRR, 2000, v:0, n:, pp:- [Journal]
  33. Randal E. Bryant, Steven M. German, Miroslav N. Velev
    Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic [Citation Graph (0, 0)][DBLP]
    CoRR, 1999, v:0, n:, pp:- [Journal]
  34. Miroslav N. Velev, Randal E. Bryant
    Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 2003, v:35, n:2, pp:73-106 [Journal]
  35. Miroslav N. Velev
    Tuning SAT for Formal Verification and Testing. [Citation Graph (0, 0)][DBLP]
    J. UCS, 2004, v:10, n:12, pp:1559-1561 [Journal]
  36. Randal E. Bryant, Steven M. German, Miroslav N. Velev
    Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Comput. Log., 2001, v:2, n:1, pp:93-134 [Journal]
  37. Randal E. Bryant, Miroslav N. Velev
    Boolean satisfiability with transitivity constraints. [Citation Graph (0, 0)][DBLP]
    ACM Trans. Comput. Log., 2002, v:3, n:4, pp:604-627 [Journal]

  38. Efficient SAT Techniques for Relative Encoding of Permutations with Constraints. [Citation Graph (, )][DBLP]


  39. Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems. [Citation Graph (, )][DBLP]


  40. Exploiting hierarchy and structure to efficiently solve graph coloring as SAT. [Citation Graph (, )][DBLP]


  41. Efficient SAT-based techniques for Design of Experiments by using static variable ordering. [Citation Graph (, )][DBLP]


  42. Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles. [Citation Graph (, )][DBLP]


Search in 0.095secs, Finished in 0.096secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002