Miroslav N. Velev
Orcid: 0000-0001-7775-5186
According to our database1,
Miroslav N. Velev
authored at least 65 papers
between 1997 and 2023.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis Dataset OtherLinks
Online presence:
-
on orcid.org
On csauthors.net:
Bibliography
2023
Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction.
Proceedings of the iFM 2023 - 18th International Conference, 2023
2018
Survey of Techniques for Efficient Solving of Boolean Formulas from Formal Verification of Pipelined, Superscalar, and VLIW Microprocessors at a High Level of Abstraction.
Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2018
2017
2016
Application of Hierarchical Hybrid Encodings to Solve CSPs as Equivalent SAT Problems.
Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2016
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016
2015
Exploiting abstraction, learning from random simulation, and SVM classification for efficient dynamic prediction of software health problems.
Proceedings of the Sixteenth International Symposium on Quality Electronic Design, 2015
2014
Ann. Math. Artif. Intell., 2014
Proceedings of the Fifteenth International Symposium on Quality Electronic Design, 2014
Improving the efficiency of automated debugging of pipelined microprocessors by symmetry breaking in modular schemes for boolean encoding of cardinality.
Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, 2014
Proceedings of the 19th Asia and South Pacific Design Automation Conference, 2014
2013
Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT.
Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence, 2013
2012
Automated debugging of counterexamples in formal verification of pipelined microprocessors.
Proceedings of the 17th Asia and South Pacific Design Automation Conference, 2012
2011
Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors.
Proceedings of the Ninth Symposium on Abstraction, Reformulation, and Approximation, 2011
Efficient Pseudo-Boolean Satisfiability Encodings for Routing and Wavelength Assignment in Optical Networks.
Proceedings of the Ninth Symposium on Abstraction, Reformulation, and Approximation, 2011
CNF encodings of cardinality in formal methods for robustness checking of gate-level circuits.
Proceedings of the International Symposium on Circuits and Systems (ISCAS 2011), 2011
Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units.
Proceedings of the Formal Methods and Software Engineering, 2011
Proceedings of the 2011 IEEE/ACM International Conference on Computer-Aided Design, 2011
Proceedings of the 16th Asia South Pacific Design Automation Conference, 2011
2010
Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2010
Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors.
Proceedings of the Formal Methods and Software Engineering, 2010
A method for debugging of pipelined processors in formal verification by correspondence checking.
Proceedings of the 15th Asia South Pacific Design Automation Conference, 2010
2009
Efficient SAT Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles.
Proceedings of the Eighth Symposium on Abstraction, Reformulation, and Approximation, 2009
Efficient SAT-based techniques for Design of Experiments by using static variable ordering.
Proceedings of the 10th International Symposium on Quality of Electronic Design (ISQED 2009), 2009
Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2009
Proceedings of the AI 2009: Advances in Artificial Intelligence, 2009
2008
Editor's Introduction to the Special Volume on Application of Constraints to Formal Verification.
J. Satisf. Boolean Model. Comput., 2008
Proceedings of the Design, Automation and Test in Europe, 2008
2007
Proceedings of the 2007 International Conference on Computer-Aided Design, 2007
2006
Proceedings of the 7th International Symposium on Quality of Electronic Design (ISQED 2006), 2006
Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction.
Proceedings of the 7th International Symposium on Quality of Electronic Design (ISQED 2006), 2006
2005
IEEE Trans. Educ., 2005
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., 2005
Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units.
Proceedings of the Correct Hardware Design and Verification Methods, 2005
Proceedings of the 2005 Conference on Asia South Pacific Design Automation, 2005
2004
Proceedings of the SAT 2004, 2004
A new generation of ISCAS benchmarks from formal verification of high-level microprocessors.
Proceedings of the 2004 International Symposium on Circuits and Systems, 2004
Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors.
Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2004
Proceedings of the 22nd IEEE International Conference on Computer Design: VLSI in Computers & Processors (ICCD 2004), 2004
Proceedings of the Ninth IEEE International High-Level Design Validation and Test Workshop 2004, 2004
Proceedings of the 14th ACM Great Lakes Symposium on VLSI 2004, 2004
Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors.
Proceedings of the 2004 Design, 2004
Proceedings of the 2004 Conference on Asia South Pacific Design Automation: Electronic Design and Solution Fair 2004, 2004
Efficient translation of boolean formulas to CNF in formal verification of microprocessors.
Proceedings of the 2004 Conference on Asia South Pacific Design Automation: Electronic Design and Solution Fair 2004, 2004
2003
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
J. Symb. Comput., 2003
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2003
Formal Verification of an Intel XScale Processor Model with Scoreboarding, Specialized Execution Pipelines, and Impress Data-Memory Exceptions.
Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003
Collection of High-Level Microprocessor Bugs from Formal Verification of Pipelined and Superscalar Designs.
Proceedings of the Proceedings 2003 International Test Conference (ITC 2003), Breaking Test Interface Bottlenecks, 28 September, 2003
2002
Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer.
Proceedings of the 2002 Design, 2002
2001
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic.
ACM Trans. Comput. Log., 2001
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001
2000
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction.
Proceedings of the 37th Conference on Design Automation, 2000
Proceedings of the Computer Aided Verification, 12th International Conference, 2000
1999
Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1999
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors.
Proceedings of the 36th Conference on Design Automation, 1999
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic.
Proceedings of the Correct Hardware Design and Verification Methods, 1999
Proceedings of the Computer Aided Verification, 11th International Conference, 1999
1998
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998
Incorporating timing constraints in the efficient memory model for symbolic ternary simulation.
Proceedings of the International Conference on Computer Design: VLSI in Computers and Processors, 1998
Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking.
Proceedings of the Formal Methods in Computer-Aided Design, 1998
Verification of Pipelined Microprocessors by Correspondence Checking in Symbolic Ternary Simulation.
Proceedings of the 1st International Conference on Application of Concurrency to System Design (ACSD '98), 1998
1997
Proceedings of the Computer Aided Verification, 9th International Conference, 1997
Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation.
Proceedings of the Advances in Computing Science, 1997