Efficient BDD Encodings for Partial Order Constraints with Application to Expert Systems in Software Verification

1. Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509–516 (1978)

   Article  Google Scholar 

2. Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. on Computers 45, 993–1002 (1996)

   Article  MATH  Google Scholar 

3. Bryant, R.E.: Graph-based algorithm for boolean function manipulation. IEEE Trans. Comput. C-35(5), 677–691 (1986)

   Article  Google Scholar 

4. Coudert, O., Madre, J.C.: Towards an interactive fault tree analyser. In: Proc. IASTED Int. Conf. on Reliability, Quality Control and Risk Assessment (1992)

   Google Scholar 

5. Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. North-Holland, Amsterdam (1990)

   Google Scholar 

6. Detlefs, D., Forgaad, R.: A procedure for automatically proving the termination of a set of rewrite rules. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 255–270. Springer, Heidelberg (1985)

   Google Scholar 

7. Fujita, M., Fujisawa, H., Matsunaga, Y.: Variable ordering algorithms for ordered binary decision diagrams and their evaluation. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 12, 6–12 (1993)

   Article  Google Scholar 

8. Kurihara, M., Kondo, H., et al.: Using ATMS to efficiently verify the termination of rewrite rule programs, Intern. Journal of Software Engineering and Knowledge Engineering 2(4), 547–565 (1992)

   Article  Google Scholar 

9. Madre, J.C., Coudert, O.: A logically complete reasoning maintenance system based on a logical constraint solver. In: Proc. Intern. Joint Conf. on Artificial Intelligence, pp. 294–299 (1991)

   Google Scholar 

10. Malik, S., et al.: Logic verification using binary decision diagrams in a logic synthesis environment. In: Proc. IEEE Int. Conf. on Computer-Aided Design, pp. 6–9 (1988)

    Google Scholar 

11. Minato, S., Ishiura, N., Yajima, S.: Shared binary decision diagram with attributed edges for efficient Boolean function manipulation. In: 27th DAC, pp. 52–57 (1990)

    Google Scholar 

12. Moore, J.S.: Introduction to the OBDD algorithm for the ATP community. Journal of Automated Reasoning 12, 33–45 (1994)

    Article  MATH  MathSciNet  Google Scholar 

13. Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M. (ed.) Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 274–364 (1993)

    Google Scholar 

14. Sieling, D.: On the existence of polynomial time approximation schemes for OBDD minimization. In: Meinel, C., Morvan, M. (eds.) STACS 1998. LNCS, vol. 1373, pp. 205–215. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

15. Steinbach, J.: Termination of rewriting: Ph.D thesis, Univ. Kaiserslautern, Germany (1994)

    Google Scholar 

16. Steinbach, J., Kühler, U.: Check your ordering: termination proofs and open problems, SEKI report SR-90-25(SFB), Univ. Kaiserslautern, Germany (1990)

    Google Scholar 

17. Tani, S., Hamaguchi, K., Yajima, S.: The complexity of the optimal variable ordering problem of a shared binary decision diagram. In: Ng, K.W., Balasubramanian, N.V., Raghavan, P., Chin, F.Y.L. (eds.) ISAAC 1993. LNCS, vol. 762, pp. 389–398. Springer, Heidelberg (1993)

    Google Scholar 

18. Wegener, I.: Branching Programs and Binary Decision Diagrams: Theory and Application. Society for Industrial and Applied Mathematics (2000)

    Google Scholar 

Download references