Abstract is missing.
- Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMCJocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik. 3-12 [doi]
- Improved Design Debugging Using Maximum SatisfiabilitySean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, Karem A. Sakallah. 13-19 [doi]
- Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence VerificationDaher Kaiss, Marcelo Skaba, Ziyad Hanna, Zurab Khasidashvili. 20-26 [doi]
- Boosting Verification by Automatic Tuning of Decision ProceduresFrank Hutter, Domagoj Babic, Holger H. Hoos, Alan J. Hu. 27-34 [doi]
- Verifying Correctness of Transactional MemoriesAriel Cohen 0002, John W. O Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck. 37-44 [doi]
- Algorithmic Analysis of Piecewise FIFO SystemsNaghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler. 45-52 [doi]
- Transaction Based Modeling and Verification of Hardware ProtocolsXiaofang Chen, Steven M. German, Ganesh Gopalakrishnan. 53-61 [doi]
- Automating Hazard Checking in Transaction-Level Microarchitecture ModelsYogesh S. Mahajan, Sharad Malik. 62-65 [doi]
- Computing Predicate Abstractions by Integrating BDDs and SMT SolversRoberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar. 69-76 [doi]
- Induction in CEGAR for Detecting CounterexamplesChao Wang, Aarti Gupta, Franjo Ivancic. 77-84 [doi]
- Lifting Propositional Interpolants to the Word-LevelDaniel Kroening, Georg Weissenbacher. 85-89 [doi]
- Global Optimization of Compositional SystemsFadi A. Zaraket, John Pape, Adnan Aziz, Margarida F. Jacome, Sarfraz Khurshid. 93-100 [doi]
- Cross-Entropy Based TestingHana Chockler, Eitan Farchi, Benny Godlin, Sergey Novikov. 101-108 [doi]
- Automatic Abstraction Refinement for Generalized Symbolic Trajectory EvaluationYan Chen, Yujing He, Fei Xie, Jin Yang. 111-118 [doi]
- A Logic for GSTEEdward Smith. 119-126 [doi]
- Automatic Abstraction in Symbolic Trajectory EvaluationSara Adams, Magnus Björk, Thomas F. Melham, Carl-Johan H. Seger. 127-135 [doi]
- A Coverage Analysis for Safety Property ListsKoen Claessen. 139-145 [doi]
- What Triggers a Behavior?Orna Kupferman, Yoad Lustig. 146-153 [doi]
- Two-Dimensional Regular Expressions for Compositional Bus ProtocolsKathi Fisler. 154-157 [doi]
- A Quantitative Completeness Analysis for Property-SetsMartin Oberkönig, Martin Schickel, Hans Eveking. 158-161 [doi]
- Automated Extraction of Inductive Invariants to Aid Model CheckingMichael L. Case, Alan Mishchenko, Robert K. Brayton. 165-172 [doi]
- Checking Safety by Inductive Generalization of Counterexamples to InductionAaron R. Bradley, Zohar Manna. 173-180 [doi]
- Fast Minimum-Register Retiming via Binary Maximum-FlowAaron P. Hurst, Alan Mishchenko, Robert K. Brayton. 181-187 [doi]
- Formal Verification of Partial Good Self-Test Fencing StructuresAdrian E. Seigler, Gary A. Van Huben, Hari Mony. 188-191 [doi]
- Case study: Integrating FV and DV in the Verification of the Intel Core:::TM::: 2 Duo MicroprocessorAlon Flaisher, Alon Gluska, Eli Singerman. 192-195 [doi]
- Circuit Level Verification of a High-Speed ToggleChao Yan, Mark R. Greenstreet. 199-206 [doi]
- Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS DesignsMohamed H. Zaki, Ghiath Al Sammane, Sofiène Tahar, Guy Bois. 207-215 [doi]
- Analyzing Gene Relationships for Down Syndrome with Labeled Transition GraphsNeha Rungta, Hyrum Carroll, Eric G. Mercer, Randall J. Roper, Mark J. Clement, Quinn Snell. 216-219 [doi]
- A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered HardwareJulien Schmaltz. 223-230 [doi]
- Modeling Time-Triggered Protocols and Verifying Their Real-Time SchedulesLee Pike. 231-238 [doi]
- A Mechanized Refinement Framework for Analysis of Custom MemoriesSandip Ray, Jayanta Bhadra. 239-242 [doi]