The SCEAS System
| |||||||

## Search the dblp DataBase
Miroslav N. Velev:
[Publications]
[Author Rank by year]
[Co-authors]
[Prefers]
[Cites]
[Cited by]
## Publications of Author- 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] - 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] - 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] - 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] - Miroslav N. Velev
**Using positive equality to prove liveness for pipelined microprocessors.**[Citation Graph (0, 0)][DBLP] ASP-DAC, 2004, pp:316-321 [Conf] - 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] - 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] - Randal E. Bryant, Miroslav N. Velev
**Boolean Satisfiability with Transitivity Constraints.**[Citation Graph (0, 0)][DBLP] CAV, 2000, pp:85-98 [Conf] - Miroslav N. Velev
**Formal Verification of VLIW Microprocessors with Speculative Execution.**[Citation Graph (0, 0)][DBLP] CAV, 2000, pp:296-311 [Conf] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - 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] - Miroslav N. Velev
**Formal Verification of Pipelined Microprocessors with Delayed Branches.**[Citation Graph (0, 0)][DBLP] ISQED, 2006, pp:296-299 [Conf] - 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] - 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] - Miroslav N. Velev
**Encoding Global Unobservability for Efficient Translation to SAT.**[Citation Graph (0, 0)][DBLP] SAT, 2004, pp:- [Conf] - 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] - Miroslav N. Velev
**Automatic Abstraction of Equations in a Logic of Equality.**[Citation Graph (0, 0)][DBLP] TABLEAUX, 2003, pp:196-213 [Conf] - 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] - 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] - Randal E. Bryant, Miroslav N. Velev
**Boolean Satisfiability with Transitivity Constraints**[Citation Graph (0, 0)][DBLP] CoRR, 2000, v:0, n:, pp:- [Journal] - 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] - 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] - 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] - 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] - 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] **Efficient SAT Techniques for Relative Encoding of Permutations with Constraints.**[Citation Graph (, )][DBLP]**Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems.**[Citation Graph (, )][DBLP]**Exploiting hierarchy and structure to efficiently solve graph coloring as SAT.**[Citation Graph (, )][DBLP]**Efficient SAT-based techniques for Design of Experiments by using static variable ordering.**[Citation Graph (, )][DBLP]**Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles.**[Citation Graph (, )][DBLP]
Search in 0.023secs, Finished in 0.025secs | |||||||

| |||||||

| |||||||

System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002 for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002 |