Abstract is missing.
- Dimensions in program synthesisSumit Gulwani. 1 [doi]
- Verifying VIA Nano microprocessor componentsWarren A. Hunt. 3-10 [doi]
- Embedded systems design - Scientific challenges and work directionsJoseph Sifakis. 11 [doi]
- Formal verification of an ASIC ethernet switch blockB. A. Krishna, Anamaya Sullerey, Alok Jain. 13-20 [doi]
- Formal verification of arbiters using property strengthening and underapproximationsGadiel Auerbach, Fady Copty, Viresh Paruthi. 21-24 [doi]
- SAT-based semiformal verification of hardwareSabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel. 25-32 [doi]
- DFT logic verification through property based formal methods - SOC to IPLopamudra Sen, Amit Roy, Supriya Bhattacharjee, Bijitendra Mittra, Subir K. Roy. 33 [doi]
- SLAM2: Static driver verification with under 4 false alarmsThomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin. 35-42 [doi]
- Precise static analysis of untrusted driver binariesJohannes Kinder, Helmut Veith. 43-50 [doi]
- Verifying SystemC: A software model checking approachAlessandro Cimatti, Andrea Micheli, Iman Narasamdya, Marco Roveri. 51-59 [doi]
- Coping with Moore s Law (and more): Supporting arrays in state-of-the-art model checkersJason Baumgartner, Michael L. Case, Hari Mony. 61-69 [doi]
- CalCS: SMT solving for non-linear convex constraintsPierluigi Nuzzo, Alberto Puggelli, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli. 71-79 [doi]
- Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problemsSicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke. 81-89 [doi]
- A halting algorithm to determine the existence of decoderShengYu Shen, Ying Qin, Jianmin Zhang, Sikun Li. 91-99 [doi]
- Synthesis for regular specifications over unbounded domainsJad Hamza, Barbara Jobstmann, Viktor Kuncak. 101-109 [doi]
- Automatic inference of memory fencesMichael Kuperstein, Martin T. Vechev, Eran Yahav. 111-119 [doi]
- Applying SMT in symbolic execution of microcodeAnders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev. 121-128 [doi]
- Automated formal verification of processors based on architectural modelsUlrich Kühne, Sven Beyer, Jörg Bormann, John Barstow. 129-136 [doi]
- Encoding industrial hardware verification problems into effectively propositional logicMoshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov. 137-144 [doi]
- Combinational techniques for sequential equivalence checkingHamid Savoj, David Berthelot, Alan Mishchenko, Robert K. Brayton. 145-149 [doi]
- Automatic verification of estimate functions with polynomials of bounded functionsJun Sawada. 151-158 [doi]
- A framework for incremental modelling and verification of on-chip protocolsPeter Böhm. 159-166 [doi]
- Modular specification and verification of interprocess communicationEyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Hristo Pentchev. 167-174 [doi]
- Large-scale application of formal verification: From fiction to factViresh Paruthi. 175-180 [doi]
- A single-instance incremental SAT formulation of proof- and counterexample-based abstractionNiklas Eén, Alan Mishchenko, Nina Amla. 181-188 [doi]
- Predicate abstraction with adjustable-block encodingDirk Beyer, M. Erkan Keremoglu, Philipp Wendler. 189-197 [doi]
- Modular bug detection with inertial refinementNishant Sinha. 199-206 [doi]
- Path predicate abstraction by complete interval property checkingJoakim Urdahl, Dominik Stoffel, Jörg Bormann, Markus Wedler, Wolfgang Kunz. 207-215 [doi]
- Relieving capacity limits on FPGA-based SAT-solversLeopold Haller, Satnam Singh. 217-220 [doi]
- Boosting minimal unsatisfiable core extractionAlexander Nadel. 221-229 [doi]
- Propelling SAT and SAT-based BMC using caresetMalay K. Ganai. 231-238 [doi]
- Efficiently solving quantified bit-vector formulasChristoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura. 239-246 [doi]
- Boosting multi-core reachability performance with shared hash tablesAlfons Laarman, Jaco van de Pol, Michael Weber 0002. 247-255 [doi]
- Incremental component-based construction and verification using invariantsSaddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan. 257-256 [doi]
- Verifying shadow page table algorithmsEyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Mikhail Kovalev, Wolfgang J. Paul. 267-270 [doi]
- Scalable and precise program analysis at NECGogul Balakrishnan, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang. 273-274 [doi]
- Achieving earlier verification closure using advanced formal verificationMichael Siegel. 275 [doi]
- PINCETTE - Validating changes and upgrades in networked softwareHana Chockler. 277 [doi]