default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMiroslav 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, Massimo Alioto, Bevan M. Baas, Chirn Chye Boon, Meng-Fan Chang, Naehyuck Chang, Yao-Wen Chang, Chip-Hong Chang, Shih-Chieh Chang, Poki Chen, Masud H. Chowdhury, Pasquale Corsonello, Ibrahim Abe M. Elfadel, Said Hamdioui, Masanori Hashimoto, Tsung-Yi Ho, Houman Homayoun, Yuh-Shyan Hwang, Rajiv V. Joshi, Tanay Karnik, Mehran Mozaffari Kermani, Chulwoo Kim, Tae-Hyoung Kim, Jaydeep P. Kulkarni, Eren Kursun, Erik Larsson, Hai (Helen) Li, Huawei Li, Patrick P. Mercier, Prabhat Mishra, Makoto Nagata, Arun S. Natarajan, Koji Nii, Partha Pratim Pande, Ioannis Savidis, Mingoo Seok, Sheldon X.-D. Tan, Mark M. Tehranipoor, Aida Todri-Sanial, Miroslav N. Velev, Xiaoqing Wen, Jiang Xu, Wei Zhang, Zhengya Zhang, Stacey Weber Jackson:
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, Chaoqiang Zhang, Ping Gao, Alex David Groce:
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, John V. Franco:
Application of constraints to formal verification and artificial intelligence. Ann. Math. Artif. Intell. 70(4): 313-314 (2014) - [c53]Miroslav N. Velev, Ping Gao:
Efficient parallel GPU algorithms for BDD manipulation. ASP-DAC 2014: 750-755 - [c52]Miroslav N. Velev, Ping Gao:
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, Ping Gao:
Formal verification of safety of polymorphic heterogeneous multi-core architectures. ISQED 2014: 611-617 - 2013
- [c50]Van-Hau Nguyen, Miroslav N. Velev, Pedro Barahona:
Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. ICTAI 2013: 1028-1035 - 2012
- [c49]Miroslav N. Velev, Ping Gao:
Automated debugging of counterexamples in formal verification of pipelined microprocessors. ASP-DAC 2012: 689-694 - 2011
- [c48]Miroslav N. Velev, Ping Gao:
Automatic formal verification of reconfigurable DSPs. ASP-DAC 2011: 293-296 - [c47]Miroslav N. Velev, Ping Gao:
Automatic formal verification of multithreaded pipelined microprocessors. ICCAD 2011: 679-686 - [c46]Miroslav N. Velev, Ping Gao:
Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units. ICFEM 2011: 307-322 - [c45]Miroslav N. Velev, Ping Gao:
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, Ping Gao:
A method for debugging of pipelined processors in formal verification by correspondence checking. ASP-DAC 2010: 619-624 - [c41]Miroslav N. Velev, Ping Gao:
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, Ping Gao:
Efficient SAT Techniques for Relative Encoding of Permutations with Constraints. Australasian Conference on Artificial Intelligence 2009: 517-527 - [c38]Miroslav N. Velev, Ping Gao:
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, Ping Gao:
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, Ping Gao:
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, Randal E. Bryant:
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, Randal E. Bryant:
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, Randal E. Bryant:
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, Randal E. Bryant:
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, Randal E. Bryant:
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, Randal E. Bryant:
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD 1998: 200-212 - [c5]Miroslav N. Velev, Randal E. Bryant:
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, Randal E. Bryant:
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, Randal E. Bryant, Alok Jain:
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 21:12 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:
