default search action
Miroslav N. Velev
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
- [c58]Miroslav N. Velev
:
Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction. iFM 2023: 193-213
2010 – 2019
- 2018
- [c57]Miroslav N. Velev:
Survey of Techniques for Efficient Solving of Boolean Formulas from Formal Verification of Pipelined, Superscalar, and VLIW Microprocessors at a High Level of Abstraction. ISAIM 2018 - 2017
- [j9]Krishnendu Chakrabarty
Editorial. IEEE Trans. Very Large Scale Integr. Syst. 25(1): 1-20 (2017) - [e1]Laleh Behjat, Jie Han, Miroslav N. Velev, Deming Chen:
Proceedings of the on Great Lakes Symposium on VLSI 2017, Banff, AB, Canada, May 10-12, 2017. ACM 2017, ISBN 978-1-4503-4972-7 [contents] - 2016
- [c56]Prab Varma, Miroslav N. Velev
Welcome Message. HLDVT 2016: 1 - [c55]Miroslav N. Velev, Ping Gao:
Application of Hierarchical Hybrid Encodings to Solve CSPs as Equivalent SAT Problems. ISAIM 2016 - 2015
- [c54]Miroslav N. Velev
Exploiting abstraction, learning from random simulation, and SVM classification for efficient dynamic prediction of software health problems. ISQED 2015: 412-418 - 2014
- [j8]Miroslav N. Velev
Application of constraints to formal verification and artificial intelligence. Ann. Math. Artif. Intell. 70(4): 313-314 (2014) - [c53]Miroslav N. Velev
Efficient parallel GPU algorithms for BDD manipulation. ASP-DAC 2014: 750-755 - [c52]Miroslav N. Velev
Improving the efficiency of automated debugging of pipelined microprocessors by symmetry breaking in modular schemes for boolean encoding of cardinality. ICCAD 2014: 676-683 - [c51]Miroslav N. Velev
Formal verification of safety of polymorphic heterogeneous multi-core architectures. ISQED 2014: 611-617 - 2013
- [c50]Van-Hau Nguyen, Miroslav N. Velev
Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. ICTAI 2013: 1028-1035 - 2012
- [c49]Miroslav N. Velev
Automated debugging of counterexamples in formal verification of pipelined microprocessors. ASP-DAC 2012: 689-694 - 2011
- [c48]Miroslav N. Velev
Automatic formal verification of reconfigurable DSPs. ASP-DAC 2011: 293-296 - [c47]Miroslav N. Velev
Automatic formal verification of multithreaded pipelined microprocessors. ICCAD 2011: 679-686 - [c46]Miroslav N. Velev
Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units. ICFEM 2011: 307-322 - [c45]Miroslav N. Velev
CNF encodings of cardinality in formal methods for robustness checking of gate-level circuits. ISCAS 2011: 1479-1482 - [c44]Miroslav N. Velev, Ping Gao:
Efficient Pseudo-Boolean Satisfiability Encodings for Routing and Wavelength Assignment in Optical Networks. SARA 2011 - [c43]Miroslav N. Velev, Ping Gao:
Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors. SARA 2011 - 2010
- [c42]Miroslav N. Velev
A method for debugging of pipelined processors in formal verification by correspondence checking. ASP-DAC 2010: 619-624 - [c41]Miroslav N. Velev
Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors. ICFEM 2010: 355-370 - [c40]Miroslav N. Velev, Ping Gao:
Design of parallel portfolios for SAT-based solving of Hamiltonian cycle problems. ISAIM 2010
2000 – 2009
- 2009
- [c39]Miroslav N. Velev
Efficient SAT Techniques for Relative Encoding of Permutations with Constraints. Australasian Conference on Artificial Intelligence 2009: 517-527 - [c38]Miroslav N. Velev
Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality. HLDVT 2009: 8-13 - [c37]Miroslav N. Velev
Efficient SAT-based techniques for Design of Experiments by using static variable ordering. ISQED 2009: 371-376 - [c36]Miroslav N. Velev, Ping Gao:
Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles. SARA 2009 - 2008
- [j7]Miroslav N. Velev:
Editor's Introduction to the Special Volume on Application of Constraints to Formal Verification. J. Satisf. Boolean Model. Comput. 5(1-4) (2008) - [c35]Miroslav N. Velev
Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems. DATE 2008: 1268-1273 - 2007
- [c34]Miroslav N. Velev
Exploiting hierarchy and structure to efficiently solve graph coloring as SAT. ICCAD 2007: 135-142 - 2006
- [c33]Miroslav N. Velev
Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction. ISQED 2006: 51-56 - [c32]Miroslav N. Velev
Formal Verification of Pipelined Microprocessors with Delayed Branches. ISQED 2006: 296-299 - 2005
- [j6]Miroslav N. Velev
TLSim and EVC: a term-level symbolic simulator and an efficient decision procedure for the logic of equality with uninterpreted functions and memories. Int. J. Embed. Syst. 1(1/2): 134-149 (2005) - [j5]Miroslav N. Velev
Integrating formal verification into an advanced computer architecture course. IEEE Trans. Educ. 48(2): 216-222 (2005) - [c31]Miroslav N. Velev
Comparison of schemes for encoding unobservability in translation to SAT. ASP-DAC 2005: 1056-1059 - [c30]Miroslav N. Velev
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. CHARME 2005: 97-113 - 2004
- [j4]Miroslav N. Velev:
Tuning SAT for Formal Verification and Testing. J. Univers. Comput. Sci. 10(12): 1559-1561 (2004) - [c29]Miroslav N. Velev:
Efficient translation of boolean formulas to CNF in formal verification of microprocessors. ASP-DAC 2004: 310-315 - [c28]Miroslav N. Velev:
Using positive equality to prove liveness for pipelined microprocessors. ASP-DAC 2004: 316-321 - [c27]Miroslav N. Velev
Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors. DATE 2004: 266-271 - [c26]Miroslav N. Velev
Efficient formal verification of pipelined processors with instruction queues. ACM Great Lakes Symposium on VLSI 2004: 92-95 - [c25]Miroslav N. Velev
Formal verification of pipelined processors with load-value prediction. HLDVT 2004: 41-46 - [c24]Miroslav N. Velev
Comparative Study of Strategies for Formal Verification of High-Level Processors. ICCD 2004: 119-124 - [c23]Miroslav N. Velev:
Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors. AI&M 2004 - [c22]Miroslav N. Velev:
A new generation of ISCAS benchmarks from formal verification of high-level microprocessors. ISCAS (5) 2004: 213-216 - [c21]Miroslav N. Velev:
Encoding Global Unobservability for Efficient Translation to SAT. SAT 2004 - 2003
- [j3]Miroslav N. Velev
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. 35(2): 73-106 (2003) - [c20]Miroslav N. Velev:
Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs. ITC 2003: 138-147 - [c19]Sudarshan K. Srinivasan, Miroslav N. Velev
Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions. MEMOCODE 2003: 65-74 - [c18]Miroslav N. Velev
Automatic Abstraction of Equations in a Logic of Equality. TABLEAUX 2003: 196-213 - 2002
- [j2]Randal E. Bryant, Miroslav N. Velev
Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. 3(4): 604-627 (2002) - [c17]Miroslav N. Velev
Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. DATE 2002: 28-35 - 2001
- [j1]Randal E. Bryant, Steven M. German, Miroslav N. Velev
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Log. 2(1): 93-134 (2001) - [c16]Miroslav N. Velev
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. CAV 2001: 235-240 - [c15]Miroslav N. Velev, Randal E. Bryant:
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. DAC 2001: 226-231 - [c14]Miroslav N. Velev
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. TACAS 2001: 252-267 - 2000
- [c13]Randal E. Bryant, Miroslav N. Velev
Boolean Satisfiability with Transitivity Constraints. CAV 2000: 85-98 - [c12]Miroslav N. Velev
Formal Verification of VLIW Microprocessors with Speculative Execution. CAV 2000: 296-311 - [c11]Miroslav N. Velev, Randal E. Bryant:
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. DAC 2000: 112-117 - [i2]Randal E. Bryant, Miroslav N. Velev:
Boolean Satisfiability with Transitivity Constraints. CoRR cs.LO/0008001 (2000)
1990 – 1999
- 1999
- [c10]Randal E. Bryant, Steven M. German, Miroslav N. Velev
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. CAV 1999: 470-482 - [c9]Miroslav N. Velev
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. CHARME 1999: 37-53 - [c8]Miroslav N. Velev
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. DAC 1999: 397-401 - [c7]Randal E. Bryant, Steven M. German, Miroslav N. Velev
Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. TABLEAUX 1999: 1-13 - [i1]Randal E. Bryant, Steven M. German, Miroslav N. Velev:
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic. CoRR cs.LO/9910014 (1999) - 1998
- [c6]Miroslav N. Velev
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD 1998: 200-212 - [c5]Miroslav N. Velev
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. FMCAD 1998: 18-35 - [c4]Miroslav N. Velev, Randal E. Bryant:
Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. ICCD 1998: 400-406 - [c3]Miroslav N. Velev
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. TACAS 1998: 136-150 - 1997
- [c2]Randal E. Bryant, Miroslav N. Velev
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. ASIAN 1997: 18-31 - [c1]Miroslav N. Velev
Efficient Modeling of Memory Arrays in Symbolic Simulation. CAV 1997: 388-399
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-03 20:13 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: