


default search action
10th FMCAD 2010: Lugano, Switzerland
- Roderick Bloem, Natasha Sharygina:
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23. IEEE 2010, ISBN 978-1-4577-0734-6 - Sumit Gulwani:
Dimensions in program synthesis. 1 - Warren A. Hunt Jr.:
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 - Johannes Kinder, Helmut Veith:
Precise static analysis of untrusted driver binaries. 43-50 - 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 - Michael Kuperstein, Martin T. Vechev, Eran Yahav:
Automatic inference of memory fences. 111-119 - 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 - Leopold Haller, Satnam Singh:
Relieving capacity limits on FPGA-based SAT-solvers. 217-220 - 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.