Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan 0001, Edmund M. Clarke |
Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. |
FMCAD |
2010 |
DBLP BibTeX RDF |
|
1 | Jad Hamza, Barbara Jobstmann, Viktor Kuncak |
Synthesis for regular specifications over unbounded domains. |
FMCAD |
2010 |
DBLP BibTeX RDF |
|
1 | Hamid Savoj, David Berthelot, Alan Mishchenko, Robert K. Brayton |
Combinational techniques for sequential equivalence checking. |
FMCAD |
2010 |
DBLP BibTeX RDF |
|
1 | Alfons Laarman, Jaco van de Pol, Michael Weber 0002 |
Boosting multi-core reachability performance with shared hash tables. |
FMCAD |
2010 |
DBLP BibTeX RDF |
|
1 | Gadiel Auerbach, Fady Copty, Viresh Paruthi |
Formal verification of arbiters using property strengthening and underapproximations. |
FMCAD |
2010 |
DBLP BibTeX RDF |
|
1 | Roderick Bloem, Natasha Sharygina (eds.) |
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23 |
FMCAD |
2010 |
DBLP BibTeX RDF |
|
1 | Pierluigi Nuzzo 0002, Alberto Puggelli, Sanjit A. Seshia, Alberto L. Sangiovanni-Vincentelli |
CalCS: SMT solving for non-linear convex constraints. |
FMCAD |
2010 |
DBLP BibTeX RDF |
|
1 | Brian Keng, Andreas G. Veneris |
Scaling VLSI design debugging with interpolation. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Eli Arbel, Oleg Rokhlenko, Karen Yorav |
SAT-based synthesis of clock gating functions using 3-valued abstraction. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Saqib Sohail, Fabio Somenzi |
Safety first: A two-stage algorithm for LTL games. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri |
Structure-aware computation of predicate abstraction. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Angelo Brillout, Daniel Kroening, Thomas Wahl |
Mixed abstractions for floating-point arithmetic. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Tom van den Broek, Julien Schmaltz |
Towards a formally verified network-on-chip. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Sandip Ray, Warren A. Hunt Jr. |
Connecting pre-silicon and post-silicon verification. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | John W. O'Leary, Murali Talupur, Mark R. Tuttle |
Protocol verification using flows: An industrial experience. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Sergey Tverdyshev |
A verified platform for a gate-level electronic control unit. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | He Zhu 0001, Fei He 0001, William N. N. Hung, Xiaoyu Song, Ming Gu 0001 |
Data mining based decomposition for assume-guarantee reasoning. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Beyer 0001, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani |
Software model checking via large-block encoding. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | |
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA |
FMCAD |
2009 |
DBLP BibTeX RDF |
|
1 | Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov |
Verifying equivalence of memories using a first order logic theorem prover. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Malay K. Ganai, Franjo Ivancic |
Efficient decision procedure for non-linear arithmetic constraints using CORDIC. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jesse D. Bingham, John Erickson, Gaurav Singh, Flemming Andersen |
Industrial strength refinement checking. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Robert Könighofer, Georg Hofferek, Roderick Bloem |
Debugging formal specifications using simple counterstrategies. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Subodh Sharma 0001, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt |
MCC: A runtime verification tool for MCAPI user applications. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Michael L. Case, Hari Mony, Jason Baumgartner, Robert Kanzelman |
Enhanced verification by temporal decomposition. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Yakir Vizel, Orna Grumberg |
Interpolation-sequence based model checking. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Zurab Khasidashvili, Daher Kaiss, Doron Bustan |
A compositional theory for post-reboot observational equivalence checking of hardware. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Hai Zhou 0001 |
Retiming and resynthesis with sweep are complete for sequential transformation. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jason Baumgartner, Hari Mony, Michael L. Case, Jun Sawada, Karen Yorav |
Scalable conditional equivalence checking: An automated invariant-generation based approach. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Leonardo Mendonça de Moura, Nikolaj S. Bjørner |
Generalized, efficient array decision procedures. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Levent Erkök, Magnus Carlsson, Adam Wick |
Hardware/software co-verification of cryptographic algorithms using Cryptol. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Byron Cook, Ashutosh Gupta 0001, Stephen Magill, Andrey Rybalchenko, Jirí Simsa, Satnam Singh, Viktor Vafeiadis |
Finding heap-bounds for hardware synthesis. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham |
Assume-guarantee validation for STE properties within an SVA environment. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jyotirmoy V. Deshmukh, E. Allen Emerson |
Verification of recursive methods on tree-like data structures. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
Decision diagrams for linear arithmetic. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Krishnan Kailas, Viresh Paruthi, Brian Monwai |
Formal verification of correctness and performance of random priority-based arbiters. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Roderick Bloem, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann |
Synthesizing robust systems. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson |
Formal verification of analog designs using MetiTarski. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Orna Kupferman, Wenchao Li 0001, Sanjit A. Seshia |
A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Armin Biere, Robert Brummayer |
Consistency Checking of All Different Constraints over Bit-Vectors within a SAT Solver. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Chao Yan 0001, Mark R. Greenstreet |
Verifying an Arbiter Circuit. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Pieter H. Hartel, Theo C. Ruys, Marc C. W. Geilen |
Scheduling Optimisations for SPIN to Minimise Buffer Requirements in Synchronous Data Flow. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Jesse D. Bingham |
Automatic Non-Interference Lemmas for Parameterized Model Checking. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Roopsha Samanta, Jyotirmoy V. Deshmukh, E. Allen Emerson |
Automatic Generation of Local Repairs for Boolean Programs. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Eric Whitman Smith, David L. Dill |
Automatic Formal Verification of Block Cipher Implementations. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Murali Talupur, Mark R. Tuttle |
Going with the Flow: Parameterized Verification Using Message Flows. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Hana Chockler, Arie Gurfinkel, Ofer Strichman |
Beyond Vacuity: Towards the Strongest Passing Formula. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | David S. Hardin |
Invited Tutorial: Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Alessandro Cimatti, Robert B. Jones (eds.) |
Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17-20 November 2008 |
FMCAD |
2008 |
DBLP BibTeX RDF |
|
1 | Lei Bu, You Li, Linzhang Wang, Xuandong Li |
BACH : Bounded ReAchability CHecker for Linear Hybrid Automata. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Peter Böhm, Tom Melham |
A Refinement Approach to Design and Verification of On-Chip Communication Protocols. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young |
Mechanized Information Flow Analysis through Inductive Assertions. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Dan Goldwasser, Ofer Strichman, Shai Fine |
A Theory-Based Decision Heuristic for DPLL(T). |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Gianpiero Cabodi, Paolo Camurati, Luz Amanda Garcia, Marco Murciano, Sergio Nocco, Stefano Quer |
Trading-Off SAT Search and Variable Quantifications for Effective Unbounded Model Checking. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Per Bjesse |
Word-Level Sequential Memory Abstraction for Model Checking. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Cindy Eisner, Dana Fisman |
Augmenting a Regular Expression-Based Temporal Logic with Local Variables. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind |
Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Alan Mishchenko, Robert K. Brayton |
Recording Synthesis History for Sequential Verification. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | George Hagen, Cesare Tinelli |
Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, Harry C. Li |
Model Checking Nash Equilibria in MAD Distributed Systems. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Arie Gurfinkel, Sagar Chaki |
Combining Predicate and Numeric Abstraction for Software Model Checking. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Michael L. Case, Alan Mishchenko, Robert K. Brayton, Jason Baumgartner, Hari Mony |
Invariant-Strengthened Elimination of Dependent State Elements. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
A Write-Based Solver for SAT Modulo the Theory of Arrays. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Jason Baumgartner, Hari Mony, Adnan Aziz |
Optimal Constraint-Preserving Netlist Simplification. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Flavio M. de Paula, Marcel Gort, Alan J. Hu, Steven J. E. Wilton, Jin Yang 0006 |
BackSpace: Formal Analysis for Post-Silicon Debug. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Nishant Sinha 0001 |
Symbolic Program Analysis Using Term Rewriting and Generalization. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Deian Tabakov, Gila Kamhi, Moshe Y. Vardi, Eli Singerman |
A Temporal Language for SystemC. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Anna Slobodová |
Formal Verification of Hardware Support for Advanced Encryption Standard. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Michael L. Case, Alan Mishchenko, Robert K. Brayton |
Automated Extraction of Inductive Invariants to Aid Model Checking. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Daher Kaiss, Marcelo Skaba, Ziyad Hanna, Zurab Khasidashvili |
Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Aaron R. Bradley, Zohar Manna |
Checking Safety by Inductive Generalization of Counterexamples to Induction. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler |
Algorithmic Analysis of Piecewise FIFO Systems. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Yan Chen 0001, Yujing He, Fei Xie, Jin Yang 0006 |
Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Kathi Fisler |
Two-Dimensional Regular Expressions for Compositional Bus Protocols. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Chao Yan 0001, Mark R. Greenstreet |
Circuit Level Verification of a High-Speed Toggle. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Orna Kupferman, Yoad Lustig |
What Triggers a Behavior? |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Sean Safarpour, Hratch Mangassarian, Andreas G. Veneris, Mark H. Liffiton, Karem A. Sakallah |
Improved Design Debugging Using Maximum Satisfiability. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Chao Wang 0001, Aarti Gupta, Franjo Ivancic |
Induction in CEGAR for Detecting Counterexamples. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Hana Chockler, Eitan Farchi, Benny Godlin, Sergey Novikov |
Cross-Entropy Based Testing. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | |
Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, November 11-14, 2007, Proceedings |
FMCAD |
2007 |
DBLP BibTeX RDF |
|
1 | Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar |
Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Adrian E. Seigler, Gary A. Van Huben, Hari Mony |
Formal Verification of Partial Good Self-Test Fencing Structures. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
fencing, formal verification, self test |
1 | Julien Schmaltz |
A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Frank Hutter, Domagoj Babic, Holger H. Hoos, Alan J. Hu |
Boosting Verification by Automatic Tuning of Decision Procedures. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
Search Parameter Optimization, Decision Procedures, Boolean Satisfiability |
1 | Ariel Cohen 0002, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck |
Verifying Correctness of Transactional Memories. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
HTM, STM, TLC, model checking, Verification, transactional memory, TLA+ |
1 | Sara Adams, Magnus Björk, Thomas F. Melham, Carl-Johan H. Seger |
Automatic Abstraction in Symbolic Trajectory Evaluation. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Yogesh S. Mahajan, Sharad Malik |
Automating Hazard Checking in Transaction-Level Microarchitecture Models. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Fadi A. Zaraket, John Pape, Adnan Aziz, Margarida F. Jacome, Sarfraz Khurshid |
Global Optimization of Compositional Systems. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Jocelyn Simmonds, Jessica Davies 0001, Arie Gurfinkel, Marsha Chechik |
Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Kroening, Georg Weissenbacher |
Lifting Propositional Interpolants to the Word-Level. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Sandip Ray, Jayanta Bhadra |
A Mechanized Refinement Framework for Analysis of Custom Memories. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Alon Flaisher, Alon Gluska, Eli Singerman |
Case study: Integrating FV and DV in the Verification of the Intel CoreTM 2 Duo Microprocessor. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Koen Claessen |
A Coverage Analysis for Safety Property Lists. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Edward Smith |
A Logic for GSTE. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Mohamed H. Zaki, Ghiath Al Sammane, Sofiène Tahar, Guy Bois |
Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Martin Oberkönig, Martin Schickel, Hans Eveking |
A Quantitative Completeness Analysis for Property-Sets. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Xiaofang Chen, Steven M. German, Ganesh Gopalakrishnan |
Transaction Based Modeling and Verification of Hardware Protocols. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Neha Rungta, Hyrum Carroll, Eric G. Mercer, Randall J. Roper, Mark J. Clement, Quinn Snell |
Analyzing Gene Relationships for Down Syndrome with Labeled Transition Graphs. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
1 | Aaron P. Hurst, Alan Mishchenko, Robert K. Brayton |
Fast Minimum-Register Retiming via Binary Maximum-Flow. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
Sequential Verification, Retiming, Maximum Flow, State Minimization |
1 | Lee Pike |
Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|