9. FMCAD 2010: Lugano, Switzerland
Roderick Bloem, Natasha Sharygina (Eds.): Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23. IEEE 2010- Sumit Gulwani: Dimensions in program synthesis. 1
- Warren A. Hunt: Verifying VIA Nano microprocessor components. 3-10
- Joseph Sifakis: Embedded systems design - Scientific challenges and work directions. 11
- B. A. Krishna, Anamaya Sullerey, Alok Jain: Formal verification of an ASIC ethernet switch block. 13-20
- Gadiel Auerbach, Fady Copty, Viresh Paruthi: Formal verification of arbiters using property strengthening and underapproximations. 21-24
- Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel: SAT-based semiformal verification of hardware. 25-32
- Lopamudra Sen, Amit Roy, Supriya Bhattacharjee, Bijitendra Mittra, Subir K. Roy: DFT logic verification through property based formal methods - SOC to IP. 33
- Thomas Ball, Ella Bounimova, Rahul Kumar, Vladimir Levin: SLAM2: Static driver verification with under 4% false alarms. 35-42
- Alessandro Cimatti, Andrea Micheli, Iman Narasamdya, Marco Roveri: Verifying SystemC: A software model checking approach. 51-59
- Jason Baumgartner, Michael L. Case, Hari Mony: Coping with Moore's Law (and more): Supporting arrays in state-of-the-art model checkers. 61-69
- Pierluigi Nuzzo, Alberto Puggelli, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli: CalCS: SMT solving for non-linear convex constraints. 71-79
- Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. 81-89
- ShengYu Shen, Ying Qin, Jianmin Zhang, Sikun Li: A halting algorithm to determine the existence of decoder. 91-99
- Jad Hamza, Barbara Jobstmann, Viktor Kuncak: Synthesis for regular specifications over unbounded domains. 101-109
- Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev: Applying SMT in symbolic execution of microcode. 121-128
- Ulrich Kühne, Sven Beyer, Jörg Bormann, John Barstow: Automated formal verification of processors based on architectural models. 129-136
- Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov: Encoding industrial hardware verification problems into effectively propositional logic. 137-144
- Hamid Savoj, David Berthelot, Alan Mishchenko, Robert K. Brayton: Combinational techniques for sequential equivalence checking. 145-149
- Jun Sawada: Automatic verification of estimate functions with polynomials of bounded functions. 151-158
- Peter Böhm: A framework for incremental modelling and verification of on-chip protocols. 159-166
- Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Hristo Pentchev: Modular specification and verification of interprocess communication. 167-174
- Viresh Paruthi: Large-scale application of formal verification: From fiction to fact. 175-180
- Niklas Eén, Alan Mishchenko, Nina Amla: A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. 181-188
- Dirk Beyer, M. Erkan Keremoglu, Philipp Wendler: Predicate abstraction with adjustable-block encoding. 189-197
- Nishant Sinha: Modular bug detection with inertial refinement. 199-206
- Joakim Urdahl, Dominik Stoffel, Jörg Bormann, Markus Wedler, Wolfgang Kunz: Path predicate abstraction by complete interval property checking. 207-215
- Alexander Nadel: Boosting minimal unsatisfiable core extraction. 221-229
- Malay K. Ganai: Propelling SAT and SAT-based BMC using careset. 231-238
- Christoph M. Wintersteiger, Youssef Hamadi, Leonardo Mendonça de Moura: Efficiently solving quantified bit-vector formulas. 239-246
- Alfons Laarman, Jaco van de Pol, Michael Weber: Boosting multi-core reachability performance with shared hash tables. 247-255
- Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan: Incremental component-based construction and verification using invariants. 257-256
- Eyad Alkassar, Ernie Cohen, Mark A. Hillebrand, Mikhail Kovalev, Wolfgang J. Paul: Verifying shadow page table algorithms. 267-270
- Massimo Roselli: Impacting verification closure using formal analysis. 271
- Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang: Scalable and precise program analysis at NEC. 273-274
- Michael Siegel: Achieving earlier verification closure using advanced formal verification. 275
- Hana Chockler: PINCETTE - Validating changes and upgrades in networked software. 277
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18T211851 by the dblp team