Miroslav N. Velev

70 papers A* 8A 10B 5C 6Misc 3Journal 11Unranked 26

Year	Rank	Type	Title / Venue / Authors
2023	B	`conf`	Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction. iFM Miroslav N. Velev
2018	Misc	`conf`	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 Miroslav N. Velev
2017	J	`jnl`	Editorial. IEEE Trans. Very Large Scale Integr. Syst. 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 Tehranipoor, Aida Todri-Sanial, Miroslav N. Velev, Xiaoqing Wen, Jiang Xu, Wei Zhang, Zhengya Zhang, Stacey Weber Jackson
2017	—	`ed.`	Proceedings of the on Great Lakes Symposium on VLSI 2017, Banff, AB, Canada, May 10-12, 2017 ACM Great Lakes Symposium on VLSI Laleh Behjat, Jie Han, Miroslav N. Velev, Deming Chen
2016	Misc	`conf`	Application of Hierarchical Hybrid Encodings to Solve CSPs as Equivalent SAT Problems. ISAIM Miroslav N. Velev, Ping Gao
2016	—	`conf`	Welcome Message. HLDVT Prab Varma, Miroslav N. Velev
2015	—	`conf`	Exploiting abstraction, learning from random simulation, and SVM classification for efficient dynamic prediction of software health problems. ISQED Miroslav N. Velev, Chaoqiang Zhang, Ping Gao, Alex David Groce
2014	J	`jnl`	Application of constraints to formal verification and artificial intelligence. Ann. Math. Artif. Intell. Miroslav N. Velev, John V. Franco
2014	—	`conf`	Efficient parallel GPU algorithms for BDD manipulation. ASP-DAC Miroslav N. Velev, Ping Gao
2014	—	`conf`	Formal verification of safety of polymorphic heterogeneous multi-core architectures. ISQED Miroslav N. Velev, Ping Gao
2014	A	`conf`	Improving the efficiency of automated debugging of pipelined microprocessors by symmetry breaking in modular schemes for boolean encoding of cardinality. ICCAD Miroslav N. Velev, Ping Gao
2013	B	`conf`	Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT. ICTAI Van-Hau Nguyen, Miroslav N. Velev, Pedro Barahona
2012	—	`conf`	Automated debugging of counterexamples in formal verification of pipelined microprocessors. ASP-DAC Miroslav N. Velev, Ping Gao
2011	A	`conf`	Automatic formal verification of multithreaded pipelined microprocessors. ICCAD Miroslav N. Velev, Ping Gao
2011	—	`conf`	Automatic formal verification of reconfigurable DSPs. ASP-DAC Miroslav N. Velev, Ping Gao
2011	C	`conf`	CNF encodings of cardinality in formal methods for robustness checking of gate-level circuits. ISCAS Miroslav N. Velev, Ping Gao
2011	—	`conf`	Efficient Pseudo-Boolean Satisfiability Encodings for Routing and Wavelength Assignment in Optical Networks. SARA Miroslav N. Velev, Ping Gao
2011	C	`conf`	Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units. ICFEM Miroslav N. Velev, Ping Gao
2011	—	`conf`	Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors. SARA Miroslav N. Velev, Ping Gao
2010	—	`conf`	A method for debugging of pipelined processors in formal verification by correspondence checking. ASP-DAC Miroslav N. Velev, Ping Gao
2010	Misc	`conf`	Design of parallel portfolios for SAT-based solving of Hamiltonian cycle problems. ISAIM Miroslav N. Velev, Ping Gao
2010	C	`conf`	Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors. ICFEM Miroslav N. Velev, Ping Gao
2009	—	`conf`	Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles. SARA Miroslav N. Velev, Ping Gao
2009	—	`conf`	Efficient SAT Techniques for Relative Encoding of Permutations with Constraints. Australasian Conference on Artificial Intelligence Miroslav N. Velev, Ping Gao
2009	—	`conf`	Efficient SAT-based techniques for Design of Experiments by using static variable ordering. ISQED Miroslav N. Velev, Ping Gao
2009	—	`conf`	Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality. HLDVT Miroslav N. Velev, Ping Gao
2008	A	`conf`	Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems. DATE Miroslav N. Velev, Ping Gao
2008	J	`jnl`	Editor's Introduction to the Special Volume on Application of Constraints to Formal Verification. J. Satisf. Boolean Model. Comput. Miroslav N. Velev
2007	A	`conf`	Exploiting hierarchy and structure to efficiently solve graph coloring as SAT. ICCAD Miroslav N. Velev
2006	—	`conf`	Formal Verification of Pipelined Microprocessors with Delayed Branches. ISQED Miroslav N. Velev
2006	—	`conf`	Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction. ISQED Miroslav N. Velev
2005	—	`conf`	Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units. CHARME Miroslav N. Velev
2005	—	`conf`	Comparison of schemes for encoding unobservability in translation to SAT. ASP-DAC Miroslav N. Velev
2005	J	`jnl`	Integrating formal verification into an advanced computer architecture course. IEEE Trans. Educ. Miroslav N. Velev
2005	J	`jnl`	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. Miroslav N. Velev, Randal E. Bryant
2004	—	`conf`	A new generation of ISCAS benchmarks from formal verification of high-level microprocessors. ISCAS (5) Miroslav N. Velev
2004	C	`conf`	Comparative Study of Strategies for Formal Verification of High-Level Processors. ICCD Miroslav N. Velev
2004	—	`conf`	Efficient formal verification of pipelined processors with instruction queues. ACM Great Lakes Symposium on VLSI Miroslav N. Velev
2004	—	`conf`	Efficient translation of boolean formulas to CNF in formal verification of microprocessors. ASP-DAC Miroslav N. Velev
2004	A	`conf`	Encoding Global Unobservability for Efficient Translation to SAT. SAT Miroslav N. Velev
2004	A	`conf`	Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors. DATE Miroslav N. Velev
2004	—	`conf`	Formal verification of pipelined processors with load-value prediction. HLDVT Miroslav N. Velev
2004	J	`jnl`	Tuning SAT for Formal Verification and Testing. J. Univers. Comput. Sci. Miroslav N. Velev
2004	—	`conf`	Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors. AI&M Miroslav N. Velev
2004	—	`conf`	Using positive equality to prove liveness for pipelined microprocessors. ASP-DAC Miroslav N. Velev
2003	B	`conf`	Automatic Abstraction of Equations in a Logic of Equality. TABLEAUX Miroslav N. Velev
2003	A	`conf`	Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs. ITC Miroslav N. Velev
2003	J	`jnl`	Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. Miroslav N. Velev, Randal E. Bryant
2003	C	`conf`	Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions. MEMOCODE Sudarshan K. Srinivasan, Miroslav N. Velev
2002	J	`jnl`	Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Log. Randal E. Bryant, Miroslav N. Velev
2002	A	`conf`	Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer. DATE Miroslav N. Velev
2001	A	`conf`	Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors. TACAS Miroslav N. Velev
2001	A*	`conf`	EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. CAV Miroslav N. Velev, Randal E. Bryant
2001	A*	`conf`	Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. DAC Miroslav N. Velev, Randal E. Bryant
2001	J	`jnl`	Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Log. Randal E. Bryant, Steven M. German, Miroslav N. Velev
2000	J	`jnl`	Boolean Satisfiability with Transitivity Constraints CoRR Randal E. Bryant, Miroslav N. Velev
2000	A*	`conf`	Boolean Satisfiability with Transitivity Constraints. CAV Randal E. Bryant, Miroslav N. Velev
2000	A*	`conf`	Formal Verification of VLIW Microprocessors with Speculative Execution. CAV Miroslav N. Velev
2000	A*	`conf`	Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. DAC Miroslav N. Velev, Randal E. Bryant
1999	A*	`conf`	Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors. DAC Miroslav N. Velev, Randal E. Bryant
1999	A*	`conf`	Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions. CAV Randal E. Bryant, Steven M. German, Miroslav N. Velev
1999	B	`conf`	Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions. TABLEAUX Randal E. Bryant, Steven M. German, Miroslav N. Velev
1999	J	`jnl`	Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic CoRR Randal E. Bryant, Steven M. German, Miroslav N. Velev
1999	—	`conf`	Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. CHARME Miroslav N. Velev, Randal E. Bryant
1998	B	`conf`	Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking. FMCAD Miroslav N. Velev, Randal E. Bryant
1998	A	`conf`	Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. TACAS Miroslav N. Velev, Randal E. Bryant
1998	C	`conf`	Incorporating timing constraints in the efficient memory model for symbolic ternary simulation. ICCD Miroslav N. Velev, Randal E. Bryant
1998	—	`conf`	Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation. ACSD Miroslav N. Velev, Randal E. Bryant
1997	A*	`conf`	Efficient Modeling of Memory Arrays in Symbolic Simulation. CAV Miroslav N. Velev, Randal E. Bryant, Alok Jain
1997	—	`conf`	Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. ASIAN Randal E. Bryant, Miroslav N. Velev