Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
9 | Edmund M. Clarke, Daniel Kroening |
Tutorial: Software Model Checking. |
ICFEM |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Marta Z. Kwiatkowska, David Parker 0001, Yi Zhang, Rashid Mehmood |
Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking. |
MASCOTS |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Arijit Mondal, P. P. Chakrabarti 0001, Chittaranjan A. Mandal |
A New Approach to Timing Analysis Using Event Propagation and Temporal Logic. |
DATE |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Bin Li, Michael S. Hsiao, Shuo Sheng |
A Novel SAT All-Solutions Solver for Efficient Preimage Computation. |
DATE |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Erik D. Demaine, John Iacono, Stefan Langerman |
Grid Vertex-Unfolding Orthostacks. |
JCDCG |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Christophe Mues, Jan Vanthienen |
Improving the Scalability of Rule Base Verification Using Binary Decision Diagrams: An Empirical Study. |
KI |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Marc Solé, Enric Pastor |
Evaluating Symbolic Traversal Algorithms Applied to Asynchronous Concurrent Systems. |
ACSD |
2004 |
DBLP DOI BibTeX RDF |
|
9 | John Whaley, Monica S. Lam |
Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. |
PLDI |
2004 |
DBLP DOI BibTeX RDF |
inclusion-based, Java, scalable, logic programming, program analysis, Datalog, binary decision diagrams, cloning, pointer analysis, context-sensitive |
9 | HoonSang Jin, Fabio Somenzi |
CirCUs: A Hybrid Satisfiability Solver. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Malay K. Ganai, Aarti Gupta, Pranav Ashar |
Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. |
ICCAD |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Liang Zhang 0012, Mukul R. Prasad, Michael S. Hsiao |
Incremental deductive & inductive reasoning for SAT-based bounded model checking. |
ICCAD |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Jinbo Huang, Adnan Darwiche |
Toward Good Elimination Orders for Symbolic SAT Solving. |
ICTAI |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Yann Thierry-Mieg, Jean-Michel Ilié, Denis Poitrenaud |
A Symbolic Symbolic State Space Representation. |
FORTE |
2004 |
DBLP DOI BibTeX RDF |
Well-Formed Petri Nets, Symbolic Model-checking, Decision Diagrams, Symmetry Detection, Symbolic Reachability Graph |
9 | Yunja Choi, Mats Per Erik Heimdahl |
Combination Model Checking: Approach and a Case Study. |
ASE |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Christian Stangier, Thomas Sidle |
Invariant Checking Combining Forward and Backward Traversal. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Fang Yu 0001, Bow-Yaw Wang, Yao-Wen Huang |
Bounded Model Checking for Region Automata. |
FORMATS/FTRTFT |
2004 |
DBLP DOI BibTeX RDF |
|
9 | Mohammad Ghasemzadeh 0001, Volker Klotz, Christoph Meinel |
Embedding Memoization to the Semantic Tree Search for Deciding QBFs. |
Australian Conference on Artificial Intelligence |
2004 |
DBLP DOI BibTeX RDF |
Zero-Suppressed Binary Decision Diagram (ZDD), Quantified Boolean Formula (QBF), QSAT, Satisfiability, DPLL |
9 | Arindam Mukherjee 0001, Malgorzata Marek-Sadowska |
Wave steering to integrate logic and physical syntheses. |
IEEE Trans. Very Large Scale Integr. Syst. |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Jie-Hong Roland Jiang, Robert K. Brayton |
On the verification of sequential equivalence. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Shoham Ben-David, Orna Grumberg, Tamir Heyman, Assaf Schuster |
Scalable distributed on-the-fly symbolic model checking. |
Int. J. Softw. Tools Technol. Transf. |
2003 |
DBLP DOI BibTeX RDF |
Distributed, Memory, BDDs, Counterexample |
9 | Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard |
Satisfiability checking using Boolean Expression Diagrams. |
Int. J. Softw. Tools Technol. Transf. |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Juraj Hromkovic, Martin Sauerhoff |
The Power of Nondeterminism and Randomness for Oblivious Branching Programs. |
Theory Comput. Syst. |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Kenneth L. McMillan |
Interpolation and SAT-Based Model Checking. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Sanjit A. Seshia, Randal E. Bryant |
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Hasan Amjad |
Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. |
TPHOLs |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Sava Krstic, John Matthews |
Inductive Invariants for Nested Recursion. |
TPHOLs |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Shuo Sheng, Michael S. Hsiao |
Efficient Preimage Computation Using A Novel Success-Driven ATPG. |
DATE |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Zhihong Zeng, Qiushuang Zhang, Ian G. Harris, Maciej J. Ciesielski |
Fast Computation of Data Correlation Using BDDs. |
DATE |
2003 |
DBLP DOI BibTeX RDF |
|
9 | P. W. Chandana Prasad, M. Maria Dominic, Ashutosh Kumar Singh |
Variable Order Verification Use of Logic Representation. |
ICADL |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Zhan Xu, Xiaolang Yan, Yongjiang Lu, Haitong Ge |
Equivalence Checking Using Independent Cuts. |
Asian Test Symposium |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Ming Shao, Guanghui Li 0001, Xiaowei Li 0001 |
SAT-Based Algorithm of Verification for Port Order Fault. |
Asian Test Symposium |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Akihiko Tozawa, Masami Hagiya |
XML Schema Containment Checking Based on Semi-implicit Techniques. |
CIAA |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Enric Pastor, Marco A. Peña |
Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Aarti Gupta, Malay K. Ganai, Zijiang Yang 0006, Pranav Ashar |
Iterative Abstraction using SAT-based BMC with Proof Analysis. |
ICCAD |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Constantinos Bartzis, Tevfik Bultan |
Construction of Efficient BDDs for Bounded Arithmetic Constraints. |
TACAS |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Gianfranco Ciardo, Robert M. Marmorstein, Radu Siminiceanu |
Saturation Unbound. |
TACAS |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Rolf Drechsler, Junhao Shi, Görschwin Fey |
MuTaTe: an efficient design for testability technique for multiplexor based circuits. |
ACM Great Lakes Symposium on VLSI |
2003 |
DBLP DOI BibTeX RDF |
multiplexor based circuits, design for testability, logic synthesis, BDDs, decision diagrams |
9 | Jae-Seok Yang, Jeong-Yeol Kim, Joon-Ho Choi, Moon-Hyun Yoo, Jeong-Taek Kong |
Elimination of false aggressors using the functional relationship for full-chip crosstalk analysis. |
ISQED |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Peter Dybjer, Qiao Haiyan, Makoto Takeyama |
Verifying Haskell Programs by Combining Testing and Proving. |
QSIC |
2003 |
DBLP DOI BibTeX RDF |
BDDs and Haskell, program verification, random testing, type theory, proof-assistants |
9 | Hyeong-Ju Kang, In-Cheol Park |
SAT-based unbounded symbolic model checking. |
DAC |
2003 |
DBLP DOI BibTeX RDF |
boolean satisfiability checking, unbounded symbolic model checking, formal verification, symbolic model checking |
9 | Natasha Sharygina, James C. Browne |
Model Checking Software via Abstraction of Loop Transitions. |
FASE |
2003 |
DBLP DOI BibTeX RDF |
|
9 | Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella |
NuSMV 2: An OpenSource Tool for Symbolic Model Checking. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Gianpiero Cabodi, Paolo Camurati, Stefano Quer |
Dynamic Scheduling and Clustering in Symbolic Image Computation. |
DATE |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Roope Kaivola, Naren Narasimhan |
Formal Verification of the Pentium ® 4 Floating-Point Multiplier. |
DATE |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Saravanan Padmanaban, Spyros Tragoudas |
Exact Grading of Multiple Path Delay Faults. |
DATE |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Koichi Takahashi, Masami Hagiya |
Searching for Mutual Exclusion Algorithms Using BDDs. |
Progress in Discovery Science |
2002 |
DBLP DOI BibTeX RDF |
|
9 | D. Michael Miller, Rolf Drechsler |
On the Construction of Multiple-Valued Decision Diagrams. |
ISMVL |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Mikael Kerttu, Per Lindgren, Mitchell A. Thornton, Rolf Drechsler |
Switching activity estimation of finite state machines for low power synthesis. |
ISCAS (4) |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Ashraf Salem |
Semi-formal verification of VHDL-AMS descriptions. |
ISCAS (5) |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Farn Wang, Karsten Schmidt 0004 |
Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures. |
FORTE |
2002 |
DBLP DOI BibTeX RDF |
data-structures, Symmetry, symbolic model-checking, pointers |
9 | Vijay Ganesh, Sergey Berezin, David L. Dill |
Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods. |
FMCAD |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Chao Wang 0001, Gary D. Hachtel |
Sharp Disjunctive Decomposition for Language Emptiness Checking. |
FMCAD |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Marc Solé, Enric Pastor |
Traversal Techniques for Concurrent Systems. |
FMCAD |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Malay K. Ganai, Adnan Aziz |
Improved SAT-Based Bounded Reachability Analysis. |
ASP-DAC/VLSI Design |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Pallab Dasgupta, Arindam Chakrabarti, P. P. Chakrabarti 0001 |
Open Computation Tree Logic for Formal Verification of Modules. |
ASP-DAC/VLSI Design |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Ian Davies, William J. Knottenbelt, Pieter S. Kritzinger |
Symbolic Methods for the State Space Exploration of GSPN Models. |
Computer Performance Evaluation / TOOLS |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Sumio Morioka, Akashi Satoh |
An Optimized S-Box Circuit Architecture for Low Power AES Design. |
CHES |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah |
Satometer: how much have we searched? |
DAC |
2002 |
DBLP DOI BibTeX RDF |
conflict diagnosis, search progress, search space coverage, SAT, BDDs, CNF, backtrack search, ZBDDs |
9 | Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna |
A proof engine approach to solving combinational design automation problems. |
DAC |
2002 |
DBLP DOI BibTeX RDF |
|
9 | Enric Pastor, Jordi Cortadella, Oriol Roig |
Symbolic Analysis of Bounded Petri Nets. |
IEEE Trans. Computers |
2001 |
DBLP DOI BibTeX RDF |
Binary Decition Diagrams, Petri nets, formal verification, symbolic methods |
9 | Shi-Yu Huang, Kwang-Ting Cheng, Kuang-Chien Chen |
Verifying sequential equivalence using ATPG techniques. |
ACM Trans. Design Autom. Electr. Syst. |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Yoav Rodeh, Ofer Strichman |
Finite Instantiations in Equivalence Logic with Uninterpreted Functions. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Per Bjesse, Tim Leonard, Abdel Mokkedem |
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck |
Parameterized Verification with Automatically Computed Inductive Assertions. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Frank Schmiedle, Daniel Große, Rolf Drechsler, Bernd Becker 0001 |
Too Much Knowledge Hurts: Acceleration of Genetic Programs for Learning Heuristics. |
Fuzzy Days |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Dirk Beyer 0001 |
Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
Real-time systems, Formal verification, Timed Automata |
9 | Yunjian Jiang, Robert K. Brayton |
Logic optimization and code generation for embedded control applications. |
CODES |
2001 |
DBLP DOI BibTeX RDF |
code generation, MDD, Esterel, logic optimization, multiple-valued |
9 | Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan |
A Library for Composite Symbolic Representations. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Gianfranco Ciardo, Gerald Lüttgen, Radu Siminiceanu |
Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Xiang Fu 0001, Tevfik Bultan, Richard Hull 0001, Jianwen Su |
Verification of Vortex Workflows. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck |
Automatic Deductive Verification with Invisible Invariants. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Michael P. Fourman |
Propositional Reasoning. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard |
Satisfiability Checking Using Boolean Expression Diagrams. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Sherief Reda, Ayman Wahba, Ashraf Salem, Dominique Borrione, M. Ghonaimy |
On the use of don't cares during symbolic reachability analysis. |
ISCAS (5) |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Daniel Sheridan |
Comparing SAT Encodings for Model Checking. |
CP |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Maria K. Michael, Spyros Tragoudas |
ATPG for Path Delay Faults without Path Enumeration. |
ISQED |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Tevfik Bultan, Tuba Yavuz-Kahveci |
Action Language Verifier. |
ASE |
2001 |
DBLP DOI BibTeX RDF |
|
9 | Carsten Sinz, Wolfgang Küchlin, Thomas Lumpp |
Towards a Verification of the Rule-Based Expert System of the IBM SA for OS/390 Automation Manager. |
APAQS |
2001 |
DBLP DOI BibTeX RDF |
|
9 | R. Iris Bahar, Ernest T. Lampe, Enrico Macii |
Power optimization of technology-dependent circuits based on symbolic computation of logic implications. |
ACM Trans. Design Autom. Electr. Syst. |
2000 |
DBLP DOI BibTeX RDF |
design synthesis, logic design, automation, aids |
9 | Felice Balarin |
Automatic Abstraction for Worst-Case Analysis of Discrete Systems. |
DATE |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Jens Schönherr, Bernd Straube |
Automatic Equivalence Check of Circuit Descriptions at Clocked Algorithmic and Register Transfer Level. |
DATE |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Jacob M. Howe, Andy King |
Implementing Groundness Analysis with Definite Boolean Functions. |
ESOP |
2000 |
DBLP DOI BibTeX RDF |
definite Boolean functions, interpretation, groundness analysis, (constraint) logic programs |
9 | Nils Klarlund, Anders Møller, Michael I. Schwartzbach |
MONA Implementation Secrets. |
CIAA |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Dragan Jankovic, Wolfgang Günther 0001, Rolf Drechsler |
Lower Bound Sifting for MDDs. |
ISMVL |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Farn Wang |
Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. |
TACAS |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Ramesh Bharadwaj, Steve Sims |
Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking. |
TACAS |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Giorgio Delzanno, Jean-François Raskin |
Symbolic Representation of Upward-Closed Sets. |
TACAS |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Rolf Drechsler, Wolfgang Günther 0001, Bernd Becker 0001 |
Testability of Circuits Derived from Lattice Diagrams. |
EUROMICRO |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Fabrizio Ferrandi, Donatella Sciuto, Alessandro Fin, Franco Fummi |
An Application of Genetic Algorithms and BDDs to Functional Testing. |
ICCD |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Sandro Wefel, Paul Molitor |
Prove that a faulty multiplier is faulty!? |
ACM Great Lakes Symposium on VLSI |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Per Bjesse, Koen Claessen |
SAT-Based Verification without State Space Traversal. |
FMCAD |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Yuan Lu 0004, Jawahar Jain, Edmund M. Clarke, Masahiro Fujita |
Efficient variable ordering using aBDD based sampling. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
9 | João P. Marques Silva, Karem A. Sakallah |
Boolean satisfiability in electronic design automation. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Andreas Hett, Christoph Scholl 0001, Bernd Becker 0001 |
Distance driven finite state machine traversal. |
DAC |
2000 |
DBLP DOI BibTeX RDF |
|
9 | Luca Benini, Giovanni De Micheli, Enrico Macii, Massimo Poncino, Riccardo Scarsi |
Symbolic synthesis of clock-gating logic for power optimization of synchronous controllers. |
ACM Trans. Design Autom. Electr. Syst. |
1999 |
DBLP DOI BibTeX RDF |
|
9 | Bwolen Yang, Reid G. Simmons, Randal E. Bryant, David R. O'Hallaron |
Optimizing Symbolic Model Checking for Constraint-Rich Models. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
9 | David L. Dill |
Alternative Approaches to Hardware Verification (abstract). |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
9 | Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
Deciding Equality Formulas by Small Domains Instantiations. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
9 | Marius Bozga, Oded Maler |
On the Representation of Probabilities over Structured Domains. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
9 | Satyaki Das, David L. Dill, Seungjoon Park |
Experience with Predicate Abstraction. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|