Abstract
VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code written in full-fledged programming languages such as C or C++. It can automatically detect coordination problems between concurrent processes. Specifically, VeriSoft searches the state space of the system for deadlocks, livelocks, divergences, and violations of user-specified assertions. An interactive graphical simulator/debugger is also available for following the execution of all the processes of the concurrent system.
Chapter PDF
References
B. Boigelot and P. Godefroid. Model checking in practice: An analysis of the ACCESS.bus protocol using SPIN. In Proceedings of Formal Methods Europe'96, volume 1051 of Lecture Notes in Computer Science, pages 465–478, Oxford, March 1996. Springer-Verlag.
E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ cache coherence protocol. In Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and Their Apllications. North-Holland, 1993.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 1(15):36–72, 1993.
D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522–525, Cambridge, MA, October 1992. IEEE Computer Society.
J.C. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis. A toolbox for the verification of LOTOS programs. In Proc. of the 14th International Conference on Software Engineering ICSE'14, Melbourne, Australia, May 1992. ACM.
A. R. Flora-Holmquist and M. Staskauskas. Formal validation of virtual finite state machines. In Proc. Workshop on Industrial-Strength Formal Specification Techniques (WIFT'95), pages 122–129, Boca Raton, April 1995.
Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems — An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, January 1996.
P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pages 174–186, Paris, January 1997.
Z. Har'El and R. P. Kurshan. Software for analytical development of communication protocols. AT&T Technical Journal, 1990.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125–143, 1977.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
H. Rudin. Protocol development success stories: Part I. In Proc. 12th IFIP WG 6.1 International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida, June 1992. North-Holland.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Godefroid, P. (1997). VeriSoft: A tool for the automatic analysis of concurrent reactive software. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_52
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive