Abstract
The impact of verification technologies would be much greater if they could not only verify existing information systems, but also synthesize or discover new ones. In our previous study, we tried to discover new algorithms that satisfy a given specification, by first defining a space of algorithms, and then checking each algorithm in the space against the specification, using an automatic verifier, i.e., model checker. Needless to say, the most serious problem of this approach is in search space explosion. In this paper, we describe case studies in which we employed symbolic model checking using BDD and searched for synchronization algorithms. By employing symbolic model checking, we could speed up enumeration and verification of algorithms. We also discuss the use of approximation for reducing the search space.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. E. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, Vol.C-35, No.8, pp.677–691, 1986.
Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model Checking, The MIT Press, 1999.
Edmund M. Clarke, Somesh Jha, Yuan Lu, and Dong Wang. Abstact BDDs: A Technique for Using Abstraction in Model Checking. Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science, Vol.1703, pp.172–186, 1999.
Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Conference Record of the 4th ACM Symposium on Principles of Programming Languages, pp.238–252, 1977.
Torbjörn Granlund and Richard Kenner. Eliminating Branches using a Superoptimizer and the GNU C Compiler. PLDI’92, Proceedings of the conference on Programming language design and implementation, pp.341–352, 1992.
Masami Hagiya. Discovering Algorithms by Verifiers. Programming Symposium, Information Processing Society of Japan, pp.9–19, 2000, in Japanese.
Masami Hagiya and Koichi Takahashi. Discovery and Deduction, Discovery Science, Third International Conference, DS 2000 (Setsuo Arikawa and Shinichi Morishita Eds.), Lecture Notes in Artificial Intelligence, Vol.1967, pp.17–37, 2000.
David E. Long. bdd-a binary decision diagram (BDD) package, 1993. http://www.cs.cmu.edu/~modelcheck/code.html
Henry Massalin. Superoptimizer: A Look at the Smallest Program. Proceedings of the Second International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS II, pp.122–126, 1987.
Adrian Perrig and Dawn Song. A First Step on Automatic Protocol Generation of Security Protocols. Proceedings of Network and Distributed System Security, 2000 Feb.
Dawn Xiaodong Song. Athena: a New Efficient Automatic Checker for Security Protocol Analysis, Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp.192–202, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Takahashi, K., Hagiya, M. (2002). Searching for Mutual Exclusion Algorithms Using BDDs. In: Arikawa, S., Shinohara, A. (eds) Progress in Discovery Science. Lecture Notes in Computer Science(), vol 2281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45884-0_1
Download citation
DOI: https://doi.org/10.1007/3-540-45884-0_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43338-5
Online ISBN: 978-3-540-45884-5
eBook Packages: Springer Book Archive