Search results for "BDD"

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