Abstract is missing.
- Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal ReasoningTilman Glökler, Jason Baumgartner, Devi Shanmugam, A. E. (Rick) Seigler, Gary A. Van Huben, Barinjato Ramanandray, Hari Mony, Paul Roessler. 3-10 [doi]
- Post-reboot Equivalence and Compositional Verification of HardwareZurab Khasidashvili, Marcelo Skaba, Daher Kaiss, Ziyad Hanna. 11-18 [doi]
- Synchronous Elastic NetworksSava Krstic, Jordi Cortadella, Michael Kishinevsky, John O Leary. 19-30 [doi]
- Finite Instantiations for Integer Difference LogicHyondeuk Kim, Fabio Somenzi. 31-38 [doi]
- Tracking MUSes and Strict Inconsistent CoversÉric Grégoire, Bertrand Mazure, Cédric Piette. 39-46 [doi]
- Ario: A Linear Integer Arithmetic Logic SolverHossein M. Sheini, Karem A. Sakallah. 47-48 [doi]
- Understanding the Dynamic Behavior of Modern DPLL SAT Solvers through Visual AnalysisCameron Brien, Sharad Malik. 49-50 [doi]
- Over-Approximating Boolean Programs with Unbounded Thread CreationByron Cook, Daniel Kroening, Natasha Sharygina. 53-59 [doi]
- An Improved Distance Heuristic Function for Directed Software Model CheckingNeha Rungta, Eric G. Mercer. 60-67 [doi]
- Liveness and Boundedness of Synchronous Data Flow GraphsAmir Hossein Ghamarian, Marc Geilen, Twan Basten, Bart D. Theelen, Mohammad Reza Mousavi, Sander Stuijk. 68-75 [doi]
- Model Checking Data-Dependent Real-Time Properties of the European Train Control SystemJohannes Faber, Roland Meyer. 76-77 [doi]
- Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/GuaranteeXiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Ching-Tsun Chou. 81-88 [doi]
- Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier SchedulingFlorian Pigorsch, Christoph Scholl, Stefan Disch. 89-96 [doi]
- Symmetry Reduction for STE Model CheckingAshish Darbari. 97-105 [doi]
- Thorough Checking RevisitedShiva Nejati, Mihaela Gheorghiu, Marsha Chechik. 106-116 [doi]
- Optimizations for LTL SynthesisBarbara Jobstmann, Roderick Bloem. 117-124 [doi]
- From PSL to NBA: a Modular Symbolic EncodingAlessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta. 125-133 [doi]
- Assume-Guarantee Reasoning for DeadlockSagar Chaki, Nishant Sinha. 134-144 [doi]
- A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware VerificationHusam Abu-Haimed, David L. Dill, Sergey Berezin. 145-152 [doi]
- An Integration of HOL and ACL2Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann. 153-160 [doi]
- ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification ToolJun Sawada, Erik Reeber. 161-170 [doi]
- Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-ChipC. Helmstetter, Florence Maraninchi, Laurent Maillet-Contoz, Matthieu Moy. 171-178 [doi]
- Simulation Bounds for Equivalence Verification of Arithmetic Datapaths with Finite Word-Length OperandsNamrata Shekhar, Priyank Kalla, M. Brandon Meredith, Florian Enescu. 179-186 [doi]
- Design for Verification of the PCI-X BusHaja Moinudeen, Ali Habibi, Sofiène Tahar. 187-188 [doi]
- Formal Analysis and Verification of an OFDM Modem Design using HOLAbu Nasser M. Abdullah, Behzad Akbarpour, Sofiène Tahar. 189-190 [doi]
- A Formal Model of Lower System LayersJulien Schmaltz. 191-192 [doi]