Abstract is missing.
- Interpolation-sequence based model checkingYakir Vizel, Orna Grumberg. 1-8 [doi]
- Structure-aware computation of predicate abstractionAlessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri. 9-16 [doi]
- Enhanced verification by temporal decompositionMichael L. Case, Hari Mony, Jason Baumgartner, Robert Kanzelman. 17-24 [doi]
- Software model checking via large-block encodingDirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani. 25-32 [doi]
- Verification of recursive methods on tree-like data structuresJyotirmoy V. Deshmukh, E. Allen Emerson. 33-40 [doi]
- MCC: A runtime verification tool for MCAPI user applicationsSubodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt. 41-44 [doi]
- Generalized, efficient array decision proceduresLeonardo Mendonça de Moura, Nikolaj Bjørner. 45-52 [doi]
- Decision diagrams for linear arithmeticSagar Chaki, Arie Gurfinkel, Ofer Strichman. 53-60 [doi]
- Efficient decision procedure for non-linear arithmetic constraints using CORDICMalay K. Ganai, Franjo Ivancic. 61-68 [doi]
- Mixed abstractions for floating-point arithmeticAngelo Brillout, Daniel Kroening, Thomas Wahl. 69-76 [doi]
- Safety first: A two-stage algorithm for LTL gamesSaqib Sohail, Fabio Somenzi. 77-84 [doi]
- Synthesizing robust systemsRoderick Bloem, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann. 85-92 [doi]
- Formal verification of analog designs using MetiTarskiWilliam Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson. 93-100 [doi]
- Formal verification of correctness and performance of random priority-based arbitersKrishnan Kailas, Viresh Paruthi, Brian Monwai. 101-107 [doi]
- Assume-guarantee validation for STE properties within an SVA environmentZurab Khasidashvili, Gavriel Gavrielov, Tom Melham. 108-115 [doi]
- Data mining based decomposition for assume-guarantee reasoningHe Zhu, Fei He, William N. N. Hung, Xiaoyu Song, Ming Gu. 116-119 [doi]
- Scalable conditional equivalence checking: An automated invariant-generation based approachJason Baumgartner, Hari Mony, Michael L. Case, Jun Sawada, Karen Yorav. 120-127 [doi]
- Verifying equivalence of memories using a first order logic theorem proverZurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov. 128-135 [doi]
- A compositional theory for post-reboot observational equivalence checking of hardwareZurab Khasidashvili, Daher Kaiss, Doron Bustan. 136-143 [doi]
- Scaling VLSI design debugging with interpolationBrian Keng, Andreas G. Veneris. 144-151 [doi]
- Debugging formal specifications using simple counterstrategiesRobert Könighofer, Georg Hofferek, Roderick Bloem. 152-159 [doi]
- Connecting pre-silicon and post-silicon verificationSandip Ray, Warren A. Hunt Jr.. 160-163 [doi]
- A verified platform for a gate-level electronic control unitSergey Tverdyshev. 164-171 [doi]
- Protocol verification using flows: An industrial experienceJohn W. O Leary, Murali Talupur, Mark R. Tuttle. 172-179 [doi]
- Industrial strength refinement checkingJesse D. Bingham, John Erickson, Gaurav Singh, Flemming Andersen. 180-183 [doi]
- Towards a formally verified network-on-chipTom van den Broek, Julien Schmaltz. 184-187 [doi]
- Hardware/software co-verification of cryptographic algorithms using CryptolLevent Erkök, Magnus Carlsson, Adam Wick. 188-191 [doi]
- Retiming and resynthesis with sweep are complete for sequential transformationHai Zhou. 192-197 [doi]
- SAT-based synthesis of clock gating functions using 3-valued abstractionEli Arbel, Oleg Rokhlenko, Karen Yorav. 198-204 [doi]
- Finding heap-bounds for hardware synthesisByron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jirà Simsa, Satnam Singh, Viktor Vafeiadis. 205-212 [doi]