Symbolic Boolean manipulation with ordered binary-decision diagrams

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Symbolic Boolean manipulation with ordered binary-decision diagrams

Full text

Pdf (2.12 MB)

Source

ACM Computing Surveys (CSUR) archive
Volume 24 , Issue 3 (September 1992) table of contents

Pages: 293 - 318

Year of Publication: 1992

ISSN:0360-0300

Author

Randal E. Bryant

School of Computer Science, Carnegie-Mellon University, Pittsburgh, Pennsylvania

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 38, Downloads (12 Months): 298, Citation Count: 229

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/136035.136043 What is a DOI?

ABSTRACT

Ordered Binary-Decision Diagrams (OBDDs) represent Boolean functions as directed acyclic graphs. They form a canonical representation, making testing of functional properties such as satisfiability and equivalence straightforward. A number of operations on Boolean functions can be implemented as graph algorithms on OBDD data structures. Using OBDDs, a wide variety of problems can be solved through symbolic analysis. First, the possible variations in system parameters and operating conditions are encoded with Boolean variables. Then the system is evaluated for all variations by a sequence of OBDD operations. Researchers have thus solved a number of problems in digital-system design, finite-state system analysis, artificial intelligence, and mathematical logic. This paper describes the OBDD data structure and surveys a number of applications that have been solved by OBDD-based symbolic analysis.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	2	S. B. 1978. Binary decision diagrams. IEEE Trans. Comput. C-27, 6 (Aug.), 509 516.
	3	Pranav Ashar , Abhijit Ghosh , Srinivas Devadas, Boolean Satisfiability and Equivalence Checking Using General Binary Decision Diagrams, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.259-264, October 14-16, 1991
	4	Randal E. Bryant , Derek L. Beatty , Carl-Johan H. Seger, Formal hardware verification by symbolic ternary trajectory evaluation, Proceedings of the 28th conference on ACM/IEEE design automation, p.397-402, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127701]
	5	C. L. 1989. Ordered binary decision diagrams and circuit structure. In The International Conference on Computer Design (Cambridge, Mass., Oct.), IEEE, New York, pp. 392 395.
	6	M. W., AND CHANDRA, A.K. 1980. Equivalence of free Boolean graphs can be decided probabilistically in polynomial time. Inf. Process. Lett. 10, 2 (Mar.), 80-82.
	7	S., AND FISHER, A. L. 1989. Verifying pipelined hardware using symbolic logic simulation. In The International Conference on Computer Deszgn (Boston, Oct.). IEEE, New York, pp. 217 221.
	8	Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
	9	Robert King Brayton , Alberto L. Sangiovanni-Vincentelli , Curtis T. McMullen , Gary D. Hachtel, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Norwell, MA, 1984
	10	F., POWNALL, P., AND HUM, P. 1984. Apphcations of testability analysis: From ATPG to critical path tracing. In The International Test Conference (Philadelphia, Oct.). IEEE, New York, pp. 705-712.
	11	F.M. 1990. Boolean Reasoning. Kluwer Academic Publishers, Boston
	12	Randal E. Bryant, On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication, IEEE Transactions on Computers, v.40 n.2, p.205-213, February 1991 [doi>10.1109/12.73590]
	13	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	14	Jerry R. Burch, Using BDDs to verify multipliers, Proceedings of the 28th conference on ACM/IEEE design automation, p.408-412, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127703]
	15	J. R., CLARKE, E. M., AND McMmLAN, K. 1990a. Symbolic model checking: 102~ states and beyond In The 5th Annual IEEE Symposium on Logic in Computer Science (Philadelphia, June) IEEE, New York, pp. 428 439
	16	J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
	17	Wolfram Büttner , Helmut Simonis, Embedding Boolean expressions into logic programming, Journal of Symbolic Computation, v.4 n.2, p.191-205, Oct. 1987 [doi>10.1016/S0747-7171(87)80065-2]
	18	E., AND MAmN, M.A. 1977. An approach to unified methodology of combinational switching circuits. IEEE Trans. Comput. C-26, 8 (Aug.), 745 756.
	19	K. Cho , R. E. Bryant, Test pattern generation for sequential MOS circuits by symbolic fault simulation, Proceedings of the 26th ACM/IEEE conference on Design automation, p.418-423, June 25-28, 1989, Las Vegas, Nevada, United States [doi>10.1145/74382.74452]
	20	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	21	Olivier Coudert , Jean Christophe Madre , Christian Berthet, Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.23-32, June 18-21, 1990
	22	Yutaka Deguchi , Nagisa Ishiura , Shuzo Yajima, Probabilistic CTSS: analysis of timing error probability in asynchronous logic circuits, Proceedings of the 28th conference on ACM/IEEE design automation, p.650-655, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127745]
	23	Reinhard Enders , Thomas Filkorn , Dirk Taubner, Generating BDDs for Symbolic Model Checking in CCS, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.203-213, July 01-04, 1991
	24	, T. 1991. A method for symbolic verification of synchronous circuits. In Computer Hardware Description Languages and their Applications (Marseilles, Apr.). Proceedings of IFIP WG 10.2, Tenth International Symposium Amsterdam, North-Holland, D. Borrione and R. Waxman, Eds., pp. 229-239.
	25	Steven Fortune , John E. Hopcroft , Erik Meineche Schmidt, The Complexity of Equivalence and Containment for Free Single Variable Program Schemes, Proceedings of the Fifth Colloquium on Automata, Languages and Programming, p.227-240, July 17-21, 1978
	26	, M., FUJISAWA, H., AND KAWATO, N. 1988. Evaluations and improvements of a Boolean comparison program based on binary decision diagrams. In The International Conference on Computer-Aided Destgn (Santa Clara. Calif., Nov.). 1EEE, New York, pp. 2 5.
	27	M., KAK~TDA, T., AND MATSUNAGA, Y. 1991. Redesign and automatic error correction of combinational circuits. In Logic and Architecture Synthesis: Proceedings of the IFIP TCIO / WGIO. 5 Workshop on Logic and Architecture Synthesis (Paris, May 1990), P. Michel and G. Saucier, Eds. Elsevier, Amsterdam, pp. 35~ ~go.
	28	M. R., AND JOHNSON, D.S. 1979. Computers and Intractability. W. H. Freeman and Company, New York.
	29	J., AND MEINEL, C. 1992. Efficient analysis and manipulation of OBDDs can be extended to read-once-only branching programs. Tech. Rep. 92-10, Universit~it Trier, Fachbereich IV--Mathematik/ Informatik, Trier, Germany.
	30	John Giraldi , Michael L. Bushnell, EST: The new frontier in automatic test-pattern generation, Proceedings of the 27th ACM/IEEE conference on Design automation, p.667-672, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123434]
	31	EONG, S.-W., PLESSIER, B., HACHTEL, G. D., AND SOMENZL F. 1991. Variable ordering and selection for FSM traversal. In The International Conference on Computer-Aided Design (Santa Clara, Calif., Nov.). IEEE, New York, pp. 476-479.
	32	Kevin Karplus, Using if-then-else DAGs for multi-level logic minimization, Proceedings of the decennial Caltech conference on VLSI on Advanced research in VLSI, p.101-117, June 1989, Cambridge, Massachusetts, United States
	33	IMURA, S., AND CLARK, E. M. 1990. A parallel algorithm for constructing binary decision diagrams. In The International Conference on Computer Design (Boston, Oct.). IEEE, New York, pp. 220-223.
	34	E, C.Y. 1959. Representation of switching circuits by binary-decision programs. Bell System Tech. J. 38, 4(July), 985-999.
	35	LIN, B., TOUATI, H. J., AND NEWTON, A.R. 1990. Don't care minimization of multi-level sequential logic networks. In The Internatwnal Conference on Computer-Aided Destgn (Santa Clara, Calif., Nov.). IEEE, New York, pp. 4{4 417.
	36	Jean-Christophe Madre , Jean-Paul Billon, Proving circuit correctness using formal comparison between expected and extracted behaviour, Proceedings of the 25th ACM/IEEE conference on Design automation, p.205-210, June 12-15, 1988, Atlantic City, New Jersey, United States
	37	MADRE, J.-C., AND COUDERT, O. 1991. A logically complete reasoning maintenance system based on a logical constraint solver. In The 12th International Joint Conference on Artificial Intelligence (Sydney, Aug.), Morgan Kaufman, San Mateo, CA, pp. 294-299.
	38	MADRE, J.-C, COUDERT, O., AND BILLON, J.P. 1989. Automating the diagnosis and rectification of design errors with PRIAM. In The Internatwnal Conference on Computer-A~ded Design (Santa Clara, Calif., Nov.). IEEE, New York, pp. 30-33.
	39	MALIK, S., WANG, A., BRAYTON, R. K., AND SANGIOVANNI-VINCENTELLI, A. 1988. Logic verification using binary decision diagrams in a logic synthes~s environment. In The International Conference on Computer-Aided Design (Santa Clara, Calif., Nov.). IEEE, New York, pp. 6-9.
	40	MCMmLAN, K. L. 1992. Symbolic model checking: An approach to the state explosion problem. PhD thesis, School of Computer Science, Carnegie-Mellon Univ.
	41	Carver Mead , Lynn Conway, Introduction to VLSI Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1979
	42	Christoph Meinel, Modified branching programs and their computational power, Springer-Verlag New York, Inc., New York, NY, 1989
	43	Shin-ichi Minato , Nagisa Ishiura , Shuzo Yajima, Shared binary decision diagram with attributed edges for efficient Boolean function manipulation, Proceedings of the 27th ACM/IEEE conference on Design automation, p.52-57, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123225]
	44	Hiroyuki Ochi , Nagisa Ishiura , Shuzo Yajima, Breadth-first manipulation of SBDD of Boolean functions for vector processing, Proceedings of the 28th conference on ACM/IEEE design automation, p.413-416, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127704]
	45	REEVES, D. S., AND IRWIN, M.J. 1987. Fast methods for switch-level verification of MOS circuits. IEEE Trans. CAD / IC CAD-G, 5 (Sept.), 766-779.
	46	Hitomi Sato , Yoshihiro Yasue , Yusuke Matsunaga , Masahiro Fujita, Boolean resubstitution with permissible functions and binary decision diagrams, Proceedings of the 27th ACM/IEEE conference on Design automation, p.284-289, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123276]
	47	SELLERS, F. F., HSIAO, M. Y., AND BEARNSON, C. L. 1968. Analyzing errors with the Boolean difference. IEEE Trans. Comput. C-17, 7(July), 676 683.
	48	SRINIVASAN, A., KAM, T., MALIK, S., AND BRAYTON, R.K. 1990. Algorithms for discrete function manipulation. In The Internattonal Conference on Computer-Aided Design (Santa Clara, Calif., Nov.). IEEE, New York, pp. 92-95.
	49	Ingo Wegener, On the complexity of branching programs and decision trees for clique functions, Journal of the ACM (JACM), v.35 n.2, p.461-471, April 1988 [doi>10.1145/42282.46161]

CITED BY 229

	Li-C. Wang , Magdy S. Abadir, Experience in Validation of PowerPCTM Microprocessor Embedded Arrays, Journal of Electronic Testing: Theory and Applications, v.15 n.1-2, p.191-205, August-October 1999
	Jason Cong , Yuzheng Ding, Beyond the combinatorial limit in depth minimization for LUT-based FPGA designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.110-114, November 07-11, 1993, Santa Clara, California, United States
	Valeria Bertacco , Maurizio Damiani , Stefano Quer, Cycle-based symbolic simulation of gate-level synchronous circuits, Proceedings of the 36th ACM/IEEE conference on Design automation, p.391-396, June 21-25, 1999, New Orleans, Louisiana, United States
	Andreas Birkendorf , Andreas Böker , Hans Ulrich Simon, Learning deterministic finite automata from smallest counterexamples, Proceedings of the ninth annual ACM-SIAM symposium on Discrete algorithms, p.599-608, January 25-27, 1998, San Francisco, California, United States
	Jason Cong , Yuzheng Ding, Combinational logic synthesis for LUT based field programmable gate arrays, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.1 n.2, p.145-204, April 1996
	F. Corno , P. Prinetto , M. Sonza Reorda , M. Violante, Exploiting symbolic techniques for partial scan flip flop selection, Proceedings of the conference on Design, automation and test in Europe, p.670-679, February 23-26, 1998, Le Palais des Congrés de Paris, France
	P. Dasgupta , P. Chakrabarti , A. Nandi , S. Krishna , A. Chakrabarti, Abstraction of word-level linear arithmetic functions from bit-level component descriptions, Proceedings of the conference on Design, automation and test in Europe, p.4-8, March 2001, Munich, Germany
	Miroslav N. Velev , Randal E. Bryant, Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction, Proceedings of the 37th conference on Design automation, p.112-117, June 05-09, 2000, Los Angeles, California, United States
	Martin Keim , Rolf Drechsler , Bernd Becker , Michael Martin , Paul Molitor, Polynomial Formal Verification of Multipliers, Formal Methods in System Design, v.22 n.1, p.39-58, January 2003
	Ming-Chuan Wu, Query optimization for selections using bitmaps, ACM SIGMOD Record, v.28 n.2, p.227-238, June 1999
	Randal E. Bryant, Bit-level analysis of an SRT divider circuit, Proceedings of the 33rd annual conference on Design automation, p.661-665, June 03-07, 1996, Las Vegas, Nevada, United States
	Lance Obermeyer , Daniel P. Miranker, Evaluating triggers using decision trees, Proceedings of the sixth international conference on Information and knowledge management, p.144-150, November 10-14, 1997, Las Vegas, Nevada, United States
	Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Li-C. Wang , Magdy S. Abadir , Nari Krishnamurthy, Automatic generation of assertions for formal verification of PowerPC microprocessor arrays using symbolic trajectory evaluation, Proceedings of the 35th annual conference on Design automation, p.534-537, June 15-19, 1998, San Francisco, California, United States
	Olivier Coudert , Tsutomu Sasao, Two-level logic minimization, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Michael Codish , Harald Søndergaard , Peter J. Stuckey, Sharing and groundness dependencies in logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.5, p.948-976, Sept. 1999
	Steven Dawson , C. R. Ramakrishnan , David S. Warren, Practical program analysis using general purpose logic programming systems—a case study, ACM SIGPLAN Notices, v.31 n.5, p.117-126, May 1996
	Michael Kishinevsky , Jordi Cortadella , Alex Kondratyev, Asynchronous interface specification, analysis and synthesis, Proceedings of the 35th annual conference on Design automation, p.2-7, June 15-19, 1998, San Francisco, California, United States
	Aarti Gupta , Allan L. Fisher, Representation and symbolic manipulation of linearly inductive Boolean functions, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.192-199, November 07-11, 1993, Santa Clara, California, United States
	Cordula Hansen , Francisco Nascimento , Wolfgang Rosenstiel, An approach for extracting RT timing information to annotate algorithmic VHDL specifications, Proceedings of the 36th ACM/IEEE conference on Design automation, p.678-683, June 21-25, 1999, New Orleans, Louisiana, United States
	Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW, Proceedings of the 38th conference on Design automation, p.226-231, June 2001, Las Vegas, Nevada, United States
	Christoph Scholl , Bernd Becker , Andreas Brogle, The multiple variable order problem for binary decision diagrams: theory and practical application, Proceedings of the 2001 conference on Asia South Pacific design automation, p.85-90, January 2001, Yokohama, Japan
	Kazuhiro Nakamura , Kazuyoshi Takagi , Shinji Kimura , Katsumasa Watanabe, Waiting false path analysis of sequential logic circuits for performance optimization, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.392-395, November 08-12, 1998, San Jose, California, United States
	M. A. Thornton , V. S. S. Nair, Behavioral synthesis of combinational logic using spectral-based heuristics, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.219-230, April 1999
	Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France
	Andrew S. Miner , Gianfranco Ciardo , Susanna Donatelli, Using the exact state space of a Markov model to compute approximate stationary measures, ACM SIGMETRICS Performance Evaluation Review, v.28 n.1, p.207-216, June 2000
	Tao Feng , Li-C. Wang , Kwang-Ting Cheng , Manish Pandey , Magdy S. Abadir, Enhanced symbolic simulation for efficient verification of embedded array systems, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
	Kazuhiro Nakamura , Shinji Maruoka , Shinji Kimura , Katsumasa Watanabe, Multi-clock path analysis using propositional satisfiability, Proceedings of the 2000 conference on Asia South Pacific design automation, p.81-86, January 2000, Yokohama, Japan
	R. Drechsler , A. Sarabi , M. Theobald , B. Becker , M. A. Perkowski, Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams, Proceedings of the 31st annual conference on Design automation, p.415-419, June 06-10, 1994, San Diego, California, United States
	Randal E. Bryant, Binary decision diagrams and beyond: enabling technologies for formal verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.236-243, November 05-09, 1995, San Jose, California, United States
	S. Höreth, Compilation of optimized OBDD-algorithms, Proceedings of the conference on European design automation, p.152-157, September 1996, Geneva, Switzerland
	Jochen Bern , Christoph Meinel , Anna Slobodová, Efficient OBDD-based boolean manipulation in CAD beyond current limits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.408-413, June 12-16, 1995, San Francisco, California, United States
	Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, Journal of Symbolic Computation, v.35 n.2, p.73-106, February 2003
	Craig A. Damon , Daniel Jackson , Somesh Jha, Checking relational specifications with binary decision diagrams, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.70-80, Nov. 1996
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	James C. Corbett, An empirical evaluation of three methods for deadlock analysis of Ada tasking programs, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.204-215, August 17-19, 1994, Seattle, Washington, United States
	Radu Marculescu , Diana Marculescu , Massoud Pedram, Switching activity analysis considering spatiotemporal correlations, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.294-299, November 06-10, 1994, San Jose, California, United States
	Vitaly Lagoon , Peter J. Stuckey, Precise pair-sharing analysis of logic programs, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.99-108, October 06-08, 2002, Pittsburgh, PA, USA
	C. R. Ramakrishnan , I. V. Ramakrishnan , R. C. Sekar, A symbolic constraint solving framework for analysis of logic programs, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.12-23, June 21-23, 1995, La Jolla, California, United States
	Gianfranco Ciardo, Distributed and structured analysis approaches to study large and complex systems, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag New York, Inc., New York, NY, 2002
	Szilvia Gyapay , András Pataricza, Optimal trajectory generation for petri nets, Acta Cybernetica, v.17 n.2, p.225-245, January 2005
	Adnan Darwiche, Decomposable negation normal form, Journal of the ACM (JACM), v.48 n.4, p.608-647, July 2001
	Stephan W. Gehring , Stefan H.-M. Ludwig, Fast integrated tools for circuit design with FPGAs, Proceedings of the 1998 ACM/SIGDA sixth international symposium on Field programmable gate arrays, p.133-139, February 22-25, 1998, Monterey, California, United States
	Simon N. Foley, Conduit cascades and secure synchronization, Proceedings of the 2000 workshop on New security paradigms, p.141-150, September 18-21, 2000, Ballycotton, County Cork, Ireland
	R. Glenn Wood , Rob A. Rutenbar, FPGA routing and routability estimation via Boolean satisfiability, Proceedings of the 1997 ACM fifth international symposium on Field-programmable gate arrays, p.119-125, February 09-11, 1997, Monterey, California, United States
	Paul Tafertshofer , Massoud Pedram, Factored Edge-Valued Binary Decision Diagrams, Formal Methods in System Design, v.10 n.2-3, p.243-270, April -May 1997
	Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997
	Daniel Mange , Eduardo Sanchez , André Stauffer , Gianluca Tempesti , Pierre Marchal , Christian Piguet, Embryonics: a new methodology for designing field-programmable gate arrays with self-repair and self-replicating properties, Readings in hardware/software co-design, Kluwer Academic Publishers, Norwell, MA, 2001
	Shinji Kimura, Residue BDD and its application to the verification of arithmetic circuits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.542-545, June 12-16, 1995, San Francisco, California, United States
	Chung-Hung Lai , Tien-Fu Chen, Compressing inverted files in scalable information systems by binary decision diagram encoding, Proceedings of the 2001 ACM/IEEE conference on Supercomputing (CDROM), p.60-60, November 10-16, 2001, Denver, Colorado
	David E. Long, The design of a cache-friendly BDD library, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.639-645, November 08-12, 1998, San Jose, California, United States
	Stephen Ponzio, A lower bound for integer multiplication with read-once branching programs, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.130-139, May 29-June 01, 1995, Las Vegas, Nevada, United States
	H. Eikerling , W. Rosenstiel, Automatic structuring and optimization of hierarchical designs, Proceedings of the conference on European design automation, p.134-139, September 1996, Geneva, Switzerland
	Christoph Scholl , Bernd Becker, Checking equivalence for partial implementations, Proceedings of the 38th conference on Design automation, p.238-243, June 2001, Las Vegas, Nevada, United States
	Carl Johan Lillieroth , Satnam Singh, Formal verification of the FPGA cores, Nordic Journal of Computing, v.6 n.3, p.299-319, Fall 1999
	Farid Ablayev , Marek Karpinski , Rustam Mubarakzjanov, On BPP versus NP (semi-circle up) coNP for ordered read-once branching programs, Theoretical Computer Science, v.264 n.1, p.127-137, 08/06/2001
	Vijay Raghavan , Dawn Wilkins, Learning &mgr;-branching programs with queries, Proceedings of the sixth annual conference on Computational learning theory, p.27-36, July 26-28, 1993, Santa Cruz, California, United States
	Sándor Palugyai , Máté J. Csorba , Sarolta Dibuz , Gyula Csopaki, Measurement and optimization of access control lists, Acta Cybernetica, v.17 n.2, p.185-198, January 2005
	Randal E. Bryant , Christoph Meinel, Ordered binary decision diagrams, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
	Li-C. Wang , Magdy S. Abadir , Jing Zeng, On measuring the effectiveness of various design validation approaches for PowerPC microprocessor embedded arrays, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.3 n.4, p.524-532, Oct. 1998
	Kim Marriott , Harald Søndergaard , Neil D. Jones, Denotational abstract interpretation of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.607-648, May 1994
	L.-C. Wang , M. S. Abadir , J. Zeng, Measuring the effectiveness of various design validation approaches for PowerPCTM microprocessor arrays, Proceedings of the conference on Design, automation and test in Europe, p.273-277, February 23-26, 1998, Le Palais des Congrés de Paris, France
	Gi-Joon Nam , Karem A. Sakallah , Rob A. Rutenbar, Satisfiability-based layout revisited: detailed routing of complex FPGAs via search-based Boolean SAT, Proceedings of the 1999 ACM/SIGDA seventh international symposium on Field programmable gate arrays, p.167-175, February 21-23, 1999, Monterey, California, United States
	Yung-Te Lai , Massoud Pedram , Sarma B. K. Vrudhula, Formal Verification Using Edge-Valued Binary Decision Diagrams, IEEE Transactions on Computers, v.45 n.2, p.247-255, February 1996
	Maria Garcia de la Banda , Peter J. Stuckey , Jeremy Wazny, Finding all minimal unsatisfiable subsets, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.32-43, August 27-29, 2003, Uppsala, Sweden
	Michael Baldamus , Klaus Schneider, The BDD space complexity of different forms of concurrency, Fundamenta Informaticae, v.50 n.2, p.111-133, April 2002
	Marc Berndl , Ondrej Lhoták , Feng Qian , Laurie Hendren , Navindra Umanee, Points-to analysis using BDDs, ACM SIGPLAN Notices, v.38 n.5, May 2003
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Christoph Meinel , Christian Stangier, Algorithms and heuristics in VLSI design, Experimental algorithmics: from algorithm design to robust and efficient software, Springer-Verlag New York, Inc., New York, NY, 2002
	J. Gergov , C. Meinel, Efficient Boolean Manipulation with OBDD's Can be Extended to FBDD's, IEEE Transactions on Computers, v.43 n.10, p.1197-1209, October 1994
	Atsuyoshi Nakamura, An efficient query learning algorithm for ordered binary decision diagrams, Information and Computation, v.201 n.2, p.178-198, September 15, 2005
	Laurent Mauborgne, Infinitary relations and their representation, Science of Computer Programming, v.47 n.2-3, p.121-144, May 2003
	Claudio Castellini , Enrico Giunchiglia , Armando Tacchella, SAT-based planning in complex domains: concurrency, constraints and nondeterminism, Artificial Intelligence, v.147 n.1-2, p.85-117, July 2003
	Patrice Godefroid , David E. Long, Symbolic Protocol Verification with Queue BDDs, Formal Methods in System Design, v.14 n.3, p.257-271, May 1999
	Detlef Sieling, The nonapproximability of OBDD minimization, Information and Computation, v.172 n.2, p.103-138, January 29, 2002
	Sanjukta Bhanja , N. Ranganathan, Swtiching activity estimation of VLSI circuits using Bayesian networks, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.11 n.4, p.558-567, August 2003
	Roberto Bagnara , Roberta Gori , Patricia M. Hill , Enea Zaffanella, Finite-tree analysis for constraint logic-based languages, Information and Computation, v.193 n.2, p.84-116, 15 September 2004
	Tao Feng , Li-C. Wang , Kwang-Ting Cheng, Improved symbolic simulation by functional-space decomposition, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.634-639, January 27-30, 2004, Yokohama, Japan
	Ashok K. Murugavel , Nagarajan Ranganathan, Petri net modeling of gate and interconnect delays for power estimation, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.11 n.5, p.921-927, October 2003
	A. Srivastava , H. N. Venkata, Quaternary to binary bit conversion CMOS integrated circuit design using multiple-input floating gate MOSFETS, Integration, the VLSI Journal, v.36 n.3, p.87-101, October 2003
	J. Jain , K. Mohanram , D. Moundanos , I. Wegener , Y. Lu, Analysis of composition complexity and how to obtain smaller canonical graphs, Proceedings of the 37th conference on Design automation, p.681-686, June 05-09, 2000, Los Angeles, California, United States
	Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Auxiliary variables for BDD-based representation and manipulation of Boolean functions, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.3 n.3, p.309-340, July 1998
	John Launchbury , Jeffrey R. Lewis , Byron Cook, On embedding a microarchitectural design language within Haskell, ACM SIGPLAN Notices, v.34 n.9, p.60-69, Sept. 1999
	Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, ACM SIGPLAN Notices, v.36 n.3, p.27-40, March 2001
	Miroslav N. Velev , Randal E. Bryant, Exploiting positive equality and partial non-consistency in the formal verification of pipelined microprocessors, Proceedings of the 36th ACM/IEEE conference on Design automation, p.397-401, June 21-25, 1999, New Orleans, Louisiana, United States
	Daniel Jackson , Somesh Jha , Craig A. Damon, Isomorph-free model enumeration: a new method for checking relational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.2, p.302-343, March 1998
	A. Hett , B. Becker , R. Drechsler, MORE: an alternative implementation of BDD packages by multi-operand synthesis, Proceedings of the conference on European design automation, p.164-169, September 1996, Geneva, Switzerland
	Kim Marriott , Harald Søndergaard, Precise and efficient groundness analysis for logic programs, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.181-196, March–Dec. 1993
	Sanjukta Bhanja , N. Ranganathan, Dependency preserving probabilistic modeling of switching activity using bayesian networks, Proceedings of the 38th conference on Design automation, p.209-214, June 2001, Las Vegas, Nevada, United States
	F. Corno , P. Prinetto , M. Rebaudengo , M. Sonza Reorda , G. Squillero, Initializability analysis of synchronous sequential circuits, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.7 n.2, p.249-264, April 2002
	Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002
	Sally A. Goldman , Stephen S. Kwek , Stephen D. Scott, Learning from examples with unspecified attribute values, Information and Computation, v.180 n.2, p.82-100, 29 January 2003
	Karen Panetta Lentz , Jamie Heller , Pier Luca Montessoro, System Verification Using Multilevel Concurrent Simulation, IEEE Micro, v.19 n.1, p.60-67, January 1999
	Beate Bollig , Ingo Wegener, Improving the Variable Ordering of OBDDs Is NP-Complete, IEEE Transactions on Computers, v.45 n.9, p.993-1002, September 1996
	Hui Xu , Rob A. Rutenbar , Karem Sakallah, sub-SAT: a formulation for relaxed boolean satisfiability with applications in routing, Proceedings of the 2002 international symposium on Physical design, April 07-10, 2002, San Diego, CA, USA
	Takenobu Aoshima , Kenji Sakuma , Naoki Yonezaki, An efficient verification procedure supporting evolution of reactive system specifications, Proceedings of the 4th International Workshop on Principles of Software Evolution, September 10-11, 2001, Vienna, Austria
	Fulvio Corno , Paolo Prinetto , Matteo Sonza Reorda, Circular Self-Test Path for FSMs, IEEE Design & Test, v.13 n.4, p.50-60, December 1996
	Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Ch. Choffrut , Y. Haddad, String-matching with OBDDs, Theoretical Computer Science, v.320 n.2-3, p.187-198, June 14, 2004
	Shiva Shankar Ramani , Sanjukta Bhanja, Any-time probabilistic switching model using bayesian networks, Proceedings of the 2004 international symposium on Low power electronics and design, August 09-11, 2004, Newport Beach, California, USA
	Sachin Kogekar , Sandeep Neema , Brandon Eames , Xenofon Koutsoukos , Akos Ledeczi , Miklos Maroti, Constraint-guided dynamic reconfiguration in sensor networks, Proceedings of the third international symposium on Information processing in sensor networks, April 26-27, 2004, Berkeley, California, USA
	Enric Pastor , Jordi Cortadella , Oriol Roig, Symbolic Analysis of Bounded Petri Nets, IEEE Transactions on Computers, v.50 n.5, p.432-448, May 2001
	Michael Wooldridge , Paul E. Dunne, On the computational complexity of qualitative coalitional games, Artificial Intelligence, v.158 n.1, p.27-73, September 2004
	A. Cimatti , M. Roveri , P. Bertoli, Conformant planning via symbolic model checking and heuristic search, Artificial Intelligence, v.159 n.1-2, p.127-206, November 2004
	Valeria Bertacco , Kunle Olukotun, Efficient state representation for symbolic simulation, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004
	Erik R. van der Meer , Ioanna Stavrinidou Henriksen , Henrik Reif Andersen, Using configuration technology as the core of a legal decision support system, Proceedings of the 9th international conference on Artificial intelligence and law, June 24-28, 2003, Scotland, United Kingdom
	Fabrizio Luccio , Linda Pagli, On a New Boolean Function with Applications, IEEE Transactions on Computers, v.48 n.3, p.296-310, March 1999
	John Lafferty , Alexander Vardy, Ordered Binary Decision Diagrams and Minimal Trellises, IEEE Transactions on Computers, v.48 n.9, p.971-986, September 1999
	J. Strother Moore , Thomas W. Lynch , Matt Kaufmann, A Mechanically Checked Proof of the AMD5K86TM Floating-Point Division Program, IEEE Transactions on Computers, v.47 n.9, p.913-926, September 1998
	Jordi Cortadella , Michael Kishinevsky , Luciano Lavagno , Alexandre Yakovlev, Deriving Petri Nets from Finite Transition Systems, IEEE Transactions on Computers, v.47 n.8, p.859-882, August 1998
	L. Benini , G. De Micheli , A. Lioy , E. Macii , G. Odasso , M. Poncino, Automatic Synthesis of Large Telescopic Units Based on Near-Minimum Timed Supersetting, IEEE Transactions on Computers, v.48 n.8, p.769-779, August 1999
	Laura Heinrich-Litan , Paul Molitor, Least Upper Bounds for the Size of OBDDs Using Symmetry Properties, IEEE Transactions on Computers, v.49 n.4, p.360-368, April 2000
	Dirk Beyer , Andreas Noack , Claus Lewerentz, Efficient Relational Calculation for Software Analysis, IEEE Transactions on Software Engineering, v.31 n.2, p.137-149, February 2005
	Anne Benoit , Paulo Fernandes , Brigitte Plateau , William J. Stewart, On the benefits of using functional transitions and Kronecker algebra, Performance Evaluation, v.58 n.4, p.367-390, December 2004
	James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996
	Farid Ablayev , Marek Karpinski, A lower bound for integer multiplication on randomized ordered read-once branching programs, Information and Computation, v.186 n.1, p.78-89, 10 October 2003
	Bernd Becker , Rolf Drechsler , Michael Theobald, On the Expressive Power of OKFDDs, Formal Methods in System Design, v.11 n.1, p.5-21, July 1997
	Nils Klarlund, Relativizations for the Logic-Automata Connection, Higher-Order and Symbolic Computation, v.18 n.1-2, p.79-120, June 2005
	Niklas Pettersson, Measuring precision for static and dynamic design pattern recognition as a function of coverage, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005
	Meir Kalech , Gal A. Kaminka, Diagnosing a team of agents: scaling-up, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
	Raymond Boute, Functional declarative language design and predicate calculus: a practical approach, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.5, p.988-1047, September 2005
	Matthias Krause , Petr Savický , Ingo Wegener, On the influence of the variable ordering for algorithmic learning using OBDDs, Information and Computation, v.201 n.2, p.160-177, September 15, 2005
	Stephen Plaza , Valeria Bertacco, STACCATO: disjoint support decompositions from BDDs through symbolic kernels, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
	Tao Feng , Li-C Wang , Kwang-Ting (Tim) Cheng , Chih-Chang (Andy) Lin, Using 2-domain partitioned OBDD data structure in an enhanced symbolic simulator, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.10 n.4, p.627-650, October 2005
	Pejman Lotfi-Kamran , Mohammad Hosseinabady , Hamid Shojaei , Mehran Massoumi , Zainalabedin Navabi, TED+: a data structure for microprocessor verification, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
	Jianbin Tan , George S. Avrunin , Lori A. Clarke, Managing space for finite-state verification, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Rolf Drechsler , Bernd Becker , Andrea Jahnke, On Variable Ordering and Decomposition Type Choice in OKFDDs, IEEE Transactions on Computers, v.47 n.12, p.1398-1403, December 1998
	Sanjukta Bhanja , Karthikeyan Lingasubramanian , N. Ranganathan, A stimulus-free graphical probabilistic switching model for sequential circuits using dynamic bayesian networks, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.11 n.3, p.773-796, July 2006
	Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005
	Prakash M. Peranandam , Pradeep K. Nalla , Jürgen Ruf , Roland J. Weiss , Thomas Kropf , Wolfgang Rosenstiel, Fast falsification based on symbolic bounded property checking, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
	Yuke Wang , Carl McCrosky, Solving Boolean Equations Using ROSOP Forms, IEEE Transactions on Computers, v.47 n.2, p.171-177, February 1998
	Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso, Strong planning under partial observability, Artificial Intelligence, v.170 n.4, p.337-384, April 2006
	G. Ciardo , R. L. Jones, III , A. S. Miner , R. I. Siminiceanu, Logic and stochastic modeling with SMART, Performance Evaluation, v.63 n.6, p.578-608, June 2006
	Felix Sheng-Ho Chang , Daniel Jackson, Symbolic model checking of declarative relational models, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Ingo Wegener, The Size of Reduced OBDD's and Optimal Read-Once Branching Programs for Almost all Boolean Functions, IEEE Transactions on Computers, v.43 n.11, p.1262-1269, November 1994
	Bernard Boigelot , Patrice Godefroid, Symbolic Verification of Communication Protocols with Infinite StateSpaces using QDDs, Formal Methods in System Design, v.14 n.3, p.237-255, May 1999
	Eugenio Di Sciascio , Francesco M. Donini , Marina Mongiello , Giacomo Piscitelli, AnWeb: a system for automatic support to web application verification, Proceedings of the 14th international conference on Software engineering and knowledge engineering, July 15-19, 2002, Ischia, Italy
	Christoph Meinel , Christian Stangier, Data structures for Boolean functions, Computational Discrete Mathematics: advanced lectures, Springer-Verlag New York, Inc., New York, NY, 2001
	Brian Herlihy , Peter Schachte , Harald Søndergaard, Boolean equation solving as graph traversal, Proceedings of the 12th Computing: The Australasian Theroy Symposium, p.123-132, January 16-19, 2006, Hobart, Australia
	Michael Eichberg , Sven Kloppenburg , Karl Klose , Mira Mezini, Defining and continuous checking of structural program dependencies, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Odile Papini, Knowledge-base revision, The Knowledge Engineering Review, v.15 n.4, p.339-370, December 2000
	Gabor Madl , Sudeep Pasricha , Luis Angel D. Bathen , Nikil Dutt , Qiang Zhu, Formal performance evaluation of AMBA-based system-on-chip designs, Proceedings of the 6th ACM & IEEE International conference on Embedded software, October 22-25, 2006, Seoul, Korea
	Nathan Clark , Amir Hormati , Scott Mahlke , Sami Yehia, Scalable subgraph mapping for acyclic computation accelerators, Proceedings of the 2006 international conference on Compilers, architecture and synthesis for embedded systems, October 22-25, 2006, Seoul, Korea
	Markus Lohrey , Sebastian Maneth, The complexity of tree automata and XPath on grammar-compressed trees, Theoretical Computer Science, v.363 n.2, p.196-210, 28 October 2006
	Ingo Brückner , Björn Metzler , Heike Wehrheim, Optimizing slicing of formal specifications by deductive verification, Nordic Journal of Computing, v.13 n.1, p.22-45, June 2006
	Roberto Micalizio , Pietro Torasso , Gianluca Torta, Synthesizing diagnostic explanations from monitoring data in multi-robot systems, Proceedings of the 24th IASTED international conference on Artificial intelligence and applications, p.279-286, February 13-16, 2006, Innsbruck, Austria
	Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of data structure properties, ACM SIGPLAN Notices, v.41 n.10, October 2006
	Alice Miller , Alastair Donaldson , Muffy Calder, Symmetry in temporal logic model checking, ACM Computing Surveys (CSUR), v.38 n.3, p.8-es, 2006
	B. Besharati , S. Azarm , P. K. Kannan, A decision support system for product design selection: a generalized purchase modeling approach, Decision Support Systems, v.42 n.1, p.333-350, October 2006
	Petr Savický , Detlef Sieling, A hierarchy result for read-once branching programs with restricted parity nondeterminism, Theoretical Computer Science, v.340 n.3, p.594-605, 31 August 2005
	Marsha Chechik , Arie Gurfinkel , Benet Devereux , Albert Lai , Steve Easterbrook, Data structures for symbolic multi-valued model-checking, Formal Methods in System Design, v.29 n.3, p.295-344, November 2006
	Mark G. J. van den Brand , Paul Klint, ATerms for manipulation and exchange of structured data: It's all about sharing, Information and Software Technology, v.49 n.1, p.55-64, January, 2007
	Rabeb Mizouni , Sofiène Tahar , Paul Curzon, Hybrid verification integrating HOL theorem proving with MDG model checking, Microelectronics Journal, v.37 n.11, p.1200-1207, November, 2006
	William C. Benton , Charles N. Fischer, Interactive, scalable, declarative program analysis: from prototype to implementation, Proceedings of the 9th ACM SIGPLAN international symposium on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland
	Haiyan Xiong , Paul Curzon , Sofiène Tahar , Ann Blandford, Providing a formal linkage between MDG and HOL, Formal Methods in System Design, v.30 n.2, p.83-116, April 2007
	Meenakshi Balasubramanian , Abhishek Bhatnagar , Namit Chaturvedi , Atish Datta Chowdhury , Arul Ganesh, A framework for decentralized access control, Proceedings of the 2nd ACM symposium on Information, computer and communications security, March 20-22, 2007, Singapore
	Julian R. Ullmann, Partition search for non-binary constraint satisfaction, Information Sciences: an International Journal, v.177 n.18, p.3639-3678, September, 2007
	Tsung-Hsi Chiang , Lan-Rong Dung, Verification method of dataflow algorithms in high-level synthesis, Journal of Systems and Software, v.80 n.8, p.1256-1270, August, 2007
	Josep Carmona , Jordi Cortadella , Yousuke Takada , Ferdinand Peper, From molecular interactions to gates: a systematic approach, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
	Quocnam Tran , Moshe Y. Vardi, Groebner bases computation in Boolean rings for symbolic model checking, Proceedings of the 18th conference on Proceedings of the 18th IASTED International Conference: modelling and simulation, p.440-445, May 30-June 01, 2007, Montreal, Canada
	Marcelo d'Amorim , Steven Lauterburg , Darko Marinov, Delta execution for efficient state-space exploration of object-oriented programs, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom
	Benoit Gaudin , Hervé Merchand, An Efficient Modular Method for the Control of Concurrent Discrete Event Systems: A Language-based Approach, Discrete Event Dynamic Systems, v.17 n.2, p.179-209, June 2007
	Nicolas Peltier, Extended resolution simulates binary decision diagrams, Discrete Applied Mathematics, v.156 n.6, p.825-837, March, 2008
	Gabor Madl , Nikil Dutt , Sherif Abdelwahed, Performance estimation of distributed real-time embedded systems by discrete event simulations, Proceedings of the 7th ACM & IEEE international conference on Embedded software, September 30-October 03, 2007, Salzburg, Austria
	Ramesh Bharadwaj , Constance L. Heitmeyer, Model Checking Complete Requirements Specifications Using Abstraction, Automated Software Engineering, v.6 n.1, p.37-68, January 1999
	U. Buy , R. H. Sloan, Automatic Real-Time Analysis of Reactive Systems with the PARTS Toolset, Automated Software Engineering, v.8 n.3-4, p.227-273, August 2001
	Li-C. Wang , Magdy S. Abadir, Test Generation Based on High-Level Assertion Specification for PowerPCTM Microprocessor Embedded Arrays, Journal of Electronic Testing: Theory and Applications, v.13 n.2, p.121-135, Oct. 1998
	Karen Panetta Lentz , Elias S. Manolakos , Edward Czeck , Jamie Heller, Multiple Experiment Environments for Testing, Journal of Electronic Testing: Theory and Applications, v.11 n.3, p.247-262, Dec. 1997
	Christoph Meinel , Anna Slobodová, A Unifying Theoretical Background for Some Bdd-based Data Structures, Formal Methods in System Design, v.11 n.3, p.223-237, Oct. 1997
	Enrique San Millán , Luis Entrena , José A. Espejo , Silvia Chiusano , Fulvio Corno, Integrating symbolic techniques in ATPG-based sequential logic optimization, Proceedings of the conference on Design, automation and test in Europe, p.105-es, January 1999, Munich, Germany
	C. Cayrol , M.-C. Lagasquie-Schiex , T. Schiex, Nonmonotonic reasoning: from complexity to algorithms, Annals of Mathematics and Artificial Intelligence, v.22 n.3-4, p.207-236, 1998
	Andreas Birkendorf , Hans Ulrich Simon, Using computational learning strategies as a tool for combinatorial optimization, Annals of Mathematics and Artificial Intelligence, v.22 n.3-4, p.237-257, 1998
	Roberto Micalizio , Pietro Torasso , Gianluca Torta, On-line monitoring and diagnosis of a team of service robots: A model-based approach, AI Communications, v.19 n.4, p.313-340, December 2006
	A. Kondratyev , J. Cortadella , M. Kishinevsky , E. Pastor , O. Roig , A. Yakovlev, Checking signal transition graph implementability by symbolic BDD traversal, Proceedings of the 1995 European conference on Design and Test, p.325, March 06-09, 1995
	I. Radivojevic , F. Brewer, On applicability of symbolic techniques to larger scheduling problems, Proceedings of the 1995 European conference on Design and Test, p.48, March 06-09, 1995
	B. Becker , R. Drechsler, How many decomposition types do we need? [decision diagrams], Proceedings of the 1995 European conference on Design and Test, p.438, March 06-09, 1995
	S. Chiusano , F. Corno , P. Prinetto , M. Sonza Reorda, Hybrid symbolic-explicit techniques for the graph coloring problem, Proceedings of the 1997 European conference on Design and Test, p.422, March 17-20, 1997
	A. Hett , R. Drechsler , B. Becker, Fast and Efficient Construction of BDDs by Reordering Based Synthesis, Proceedings of the 1997 European conference on Design and Test, p.168, March 17-20, 1997
	C. Scholl , S. Melchior , G. Hotz , P. Molitor, Minimizing ROBDD Sizes of Incompletely Specified Boolean Functions by Exploiting Strong Symmetries, Proceedings of the 1997 European conference on Design and Test, p.229, March 17-20, 1997
	Rolf Drechsler , Bernd Becker , Stefan Ruppertz, K*BMDs: A New Data Structure for Verification, Proceedings of the 1996 European conference on Design and Test, p.2, March 11-14, 1996
	Sanjukta Bhanja , N. Ranganathan, Switching Activity Estimation of Large Circuits using Multiple Bayesian Networks, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.187, January 07-11, 2002
	Shan-Tai Chen , Shun-Shii Lin , Li-Te Huang , Chun-Jen Wei, Towards the Exact Minimization of BDDs—An Elitism-Based Distributed Evolutionary Algorithm, Journal of Heuristics, v.10 n.3, p.337-355, May 2004
	Samir Genaim , Michael Codish , Jacob M. Howe, Worst-case groundness analysis using definite Boolean functions, Theory and Practice of Logic Programming, v.1 n.5, p.611-615, September 2001
	Tao Feng , Li-C. Wang , Kwang-Ting Cheng , Andy C-C. Lin, Improved Symoblic Simulation by Dynamic Funtional Space Partitioning, Proceedings of the conference on Design, automation and test in Europe, p.10042, February 16-20, 2004
	Marc-Michel Corsini , Antoine Rauzy, Toupie: The µ-calculus over Finite Domains as a Constraint Language, Journal of Automated Reasoning, v.19 n.2, p.143-171, October 1997
	Tianlong Gu , Huadong Liu, The symbolic OBDD scheme for generating mechanical assembly sequences, Formal Methods in System Design, v.33 n.1-3, p.29-44, December 2008
	Jens D. Nielsen , Rafael Rumí , Antonio Salmerón, Supervised classification using probabilistic decision graphs, Computational Statistics & Data Analysis, v.53 n.4, p.1299-1311, February, 2009
	Tianlong Gu , Zhoubo Xu , Zhifei Yang, Symbolic OBDD representations for mechanical assembly sequences, Computer-Aided Design, v.40 n.4, p.411-421, April, 2008
	Watis Leelapatra , Kanchana Kanchanasut , Chidchanok Lursinsap, Displacement BDD and geometric transformations of binary decision diagram encoded images, Pattern Recognition Letters, v.29 n.4, p.438-456, March, 2008
	Sophie Laplante , Richard Lassaigne , Frédéric Magniez , Sylvain Peyronnet , Michel de Rougemont, Probabilistic abstraction for model checking: An approach based on property testing, ACM Transactions on Computational Logic (TOCL), v.8 n.4, p.20-es, August 2007
	Silvio Lago Pereira , Leliane Nunes Barros, A logic-based agent that plans for extended reachability goals, Autonomous Agents and Multi-Agent Systems, v.16 n.3, p.327-344, June 2008
	Sandor Palugyai , Mate J. Csorba, State-space reduction in the model of Access Control Lists in IP routers, International Journal of Internet Protocol Technology, v.2 n.2, p.131-140, February 2007
	Gianluca Torta , Pietro Torasso, On the role of modeling causal independence for system model compilation with OBDDs, AI Communications, v.20 n.1, p.17-26, January 2007
	Maik Friedel , Swetlana Nikolajewa , Thomas Wilhelm, The decomposition tree for analyses of boolean functions, Mathematical Structures in Computer Science, v.18 n.2, p.411-426, April 2008
	Gianluca Torta , Pietro Torasso, An on-line approach to the computation and presentation of preferred diagnoses for dynamic systems, AI Communications, v.20 n.2, p.93-116, April 2007
	Tertia Hörne , John A. van der Poll, Planning as model checking: the performance of ProB vs NuSMV, Proceedings of the 2008 annual research conference of the South African Institute of Computer Scientists and Information Technologists on IT research in developing countries: riding the wave of technology, p.114-123, October 06-08, 2008, Wilderness, South Africa
	Ondřej Lhoták , Laurie Hendren, Relations as an abstraction for BDD-based program analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-63, July 2008
	Michael Roberson , Melanie Harries , Paul T. Darga , Chandrasekhar Boyapati, Efficient software model checking of soundness of type systems, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Andrew S. Miner, Saturation for a General Class of Models, IEEE Transactions on Software Engineering, v.32 n.8, p.559-570, August 2006
	Michele Sama , David S. Rosenblum , Zhimin Wang , Sebastian Elbaum, Model-based fault detection in context-aware adaptive applications, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	Ondřej Lhoták , Laurie Hendren, Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.18 n.1, p.1-53, September 2008
	Hamid Shojaei , Twan Basten , Marc Geilen , Phillip Stanley-Marbell, SPaC: a symbolic pareto calculator, Proceedings of the 6th IEEE/ACM/IFIP international conference on Hardware/Software codesign and system synthesis, October 19-24, 2008, Atlanta, GA, USA
	Yuqing Tang , Timothy J. Norman , Simon Parsons, A model for integrating dialogue and the execution of joint plans, Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, May 10-15, 2009, Budapest, Hungary
	K. L. McMillan, Model checking, Encyclopedia of Computer Science, 4th edition, John Wiley and Sons Ltd., Chichester, 2003
	Neil Kettle , Andy King, Bit-precise reasoning with affine functions, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, July 07-14, 2008, Princeton, New Jersey
	Bernard Boigelot , Julien Brusten, A generalization of Cobham's theorem to automata over real numbers, Theoretical Computer Science, v.410 n.18, p.1694-1703, April, 2009
	Ugur Kuter , Dana Nau , Marco Pistore , Paolo Traverso, Task decomposition on abstract states, for planning under nondeterminism, Artificial Intelligence, v.173 n.5-6, p.669-695, April, 2009
	Marco Beccuti , Daniele Codetta-Raiteri , Giuliana Franceschinis , Serge Haddad, Non deterministic repairable fault trees for computing optimal repair strategy, Proceedings of the 3rd International Conference on Performance Evaluation Methodologies and Tools, October 20-24, 2008, Athens, Greece
	Barry O'Sullivan , Gregory M. Provan, Approximate compilation for embedded model-based reasoning, Proceedings of the 21st national conference on Artificial intelligence, p.894-899, July 16-20, 2006, Boston, Massachusetts
	Yolifé Arvelo , Blai Bonet , María Esther Vidal, Compilation of query-rewriting problems into tractable fragments of propositional logic, Proceedings of the 21st national conference on Artificial intelligence, p.225-230, July 16-20, 2006, Boston, Massachusetts
	Ugur Kuter , Dana Nau, Controlled search over compact state representations, in nondeterministic planning domains and beyond, proceedings of the 21st national conference on Artificial intelligence, p.1638-1641, July 16-20, 2006, Boston, Massachusetts
	Gianluca Torta , Pietro Torasso, Parametric abstraction of behavioral modes for model-based diagnosis, AI Communications, v.22 n.2, p.73-96, April 2009
	Peter Hawkins , Vitaly Lagoon , Peter J. Stuckey, Solving set constraint satisfaction problems using ROBDDs, Journal of Artificial Intelligence Research, v.24 n.1, p.109-156, July 2005
	Stefan Edelkamp, Taming numbers and durations in the model checking integrated planning system, Journal of Artificial Intelligence Research, v.20 n.1, p.195-238, December 2003
	Alessandro Cimatti , Marco Roveri, Conformant planning via symbolic model checking, Journal of Artificial Intelligence Research, v.13 n.1, p.305-338, August 2000
	Ariel Felner , Richard E. Korf , Ram Meshulam , Robert Holte, Compressed pattern databases, Journal of Artificial Intelligence Research, v.30 n.1, p.213-247, September 2007
	Heidi E. Dixon , Matthew L. Ginsberg , Andrew J. Parkes, Generalizing Boolean satisfiability I: background and survey of existing work, Journal of Artificial Intelligence Research, v.21 n.1, p.193-243, January 2004
	Sébastien Jodogne , Justus H. Piater, Closed-loop learning of visual control policies, Journal of Artificial Intelligence Research, v.28 n.1, p.349-391, January 2007
	Chenggang Wang , Saket Joshi , Roni Khardon, First order decision diagrams for relational MDPs, Journal of Artificial Intelligence Research, v.31 n.1, p.431-472, January 2008
	Adnan Darwiche , Pierre Marquis, A knowledge compilation map, Journal of Artificial Intelligence Research, v.17 n.1, p.229-264, July 2002
	Jussi Rintanen, Constructing conditional plans by a theorem-prover, Journal of Artificial Intelligence Research, v.10 n.1, p.323-352, January 1999
	Alberto Venturini , Gregory Provan, Incremental algorithms for approximate compilation, Proceedings of the 23rd national conference on Artificial intelligence, p.1495-1498, July 13-17, 2008, Chicago, Illinois
	Jussi Rintanen , Alban Grastien, Diagnosability testing with satisfiability algorithms, Proceedings of the 20th international joint conference on Artifical intelligence, p.532-537, January 06-12, 2007, Hyderabad, India
	Dafna Shahaf , Eyal Amir, Logical circuit filtering, Proceedings of the 20th international joint conference on Artifical intelligence, p.2611-2618, January 06-12, 2007, Hyderabad, India
	Meir Kalech , Gal A. Kaminka, Towards model-based diagnosis of coordination failures, Proceedings of the 20th national conference on Artificial intelligence, p.102-107, July 09-13, 2005, Pittsburgh, Pennsylvania
	Laurent Simon, Efficient consequence finding, Proceedings of the 17th international joint conference on Artificial intelligence, p.359-365, August 04-10, 2001, Seattle, WA, USA
	Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri, Heuristic search + symbolic model checking = efficient conformant planning, Proceedings of the 17th international joint conference on Artificial intelligence, p.467-472, August 04-10, 2001, Seattle, WA, USA
	Piergiorgio Bertoli , Alessandro Cimatti , Marco Roveri , Paolo Traverso, Planning in nondeterministic domains under partial observability via symbolic model checking, Proceedings of the 17th international joint conference on Artificial intelligence, p.473-478, August 04-10, 2001, Seattle, WA, USA