BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Canada
1 × Germany
1 × Israel
1 × Portugal
2 × Italy
3 × France
4 × USA
Collaborated with:
R.E.Bryant P.Gao S.M.German A.Jain
Talks about:
microprocessor (7) formal (7) verif (6) equal (6) exploit (4) memori (4) effici (4) posit (4) function (3) satisfi (3)

Person: Miroslav N. Velev

DBLP DBLP: Velev:Miroslav_N=

Contributed to:

DATE 20082008
DATE v1 20042004
SAT 20042004
DATE 20022002
CAV 20012001
DAC 20012001
TACAS 20012001
CAV 20002000
DAC 20002000
CAV 19991999
DAC 19991999
TACAS 19981998
CAV 19971997

Wrote 14 papers:

DATE-2008-VelevG #comparison #encoding #problem #satisfiability
Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems (MNV, PG), pp. 1268–1273.
DATE-v1-2004-Velev #performance #verification
Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors (MNV), pp. 266–271.
SAT-2004-Velev #encoding #performance #satisfiability
Encoding Global Unobservability for Efficient Translation to SAT (MNV), pp. 197–204.
DATE-2002-Velev #similarity #using #verification
Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer (MNV), pp. 28–35.
CAV-2001-VelevB #logic #named #similarity
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations (MNV, REB), pp. 235–240.
DAC-2001-VelevB #effectiveness #satisfiability #using #verification
Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors (MNV, REB), pp. 226–231.
TACAS-2001-Velev #abstraction #automation #verification
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors (MNV), pp. 252–267.
CAV-2000-BryantV #constraints #satisfiability #transitive
Boolean Satisfiability with Transitivity Constraints (REB, MNV), pp. 85–98.
CAV-2000-Velev #execution #verification
Formal Verification of VLIW Microprocessors with Speculative Execution (MNV), pp. 296–311.
DAC-2000-VelevB #branch #exception #functional #multi #predict #verification
Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction (MNV, REB), pp. 112–117.
CAV-1999-BryantGV #logic #similarity
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions (REB, SMG, MNV), pp. 470–482.
DAC-1999-VelevB #pipes and filters #similarity #verification
Exploiting Positive Equality and Partial Non-Consistency in the Formal Verification of Pipelined Microprocessors (MNV, REB), pp. 397–401.
TACAS-1998-VelevB #array #memory management #modelling #performance #simulation
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation (MNV, REB), pp. 136–150.
CAV-1997-VelevBJ #array #memory management #modelling #performance #simulation
Efficient Modeling of Memory Arrays in Symbolic Simulation (MNV, REB, AJ), pp. 388–399.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.