Cited By
View all- Staskauskas M(1993)Formal Derivation of Concurrent ProgramsIEEE Transactions on Software Engineering10.1109/32.23201519:5(503-528)Online publication date: 1-May-1993
An experience in the formal verification of industrial software
References
[1]
Brooks F.R No silver bullet: Essence and accidents of software engineering. IEEE Comput. 20, (4) (1987).
[2]
Chandy K.M. and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
[3]
Goldschlag, D.M. Mechanically verifying concurrent programs with the Boyer-Moore prover. IEEE Trans. Soft. Eng. 16, 9 (1990).
[4]
DeMillo R.A., R.J. Lipton, and A.J. Perlis. Social processes and proofs of theorems and programs. Comm. ACM22, 5 (1979).
[5]
Dijkstra E.W. On the cruelty of really teaching computing science. Comm. ACM 32, 12 (1989).
[6]
Fetzer J.R Program verification: The very idea. Comm. ACM 31, 9 (1988).
[7]
Gries D., M. Ardis, J.R Fetzer and R.J. Lipton. Debate on formal program verification. ACM Computer Science Conference, 1990.
[8]
Hayes I. Ed. Specification Case Studies. Prentice Hall (1987).
[9]
IEEE Transactions on Software Engineering, 16, 9. September 1990 (Special issue on formal methods in software engineering).
[10]
IEEE Software, 7, 5, September 1990 (Special section on formal methods).
[11]
Lamport L. Solved problems, unsolved problems and nonproblems in concurrency. In Proceedings of the ACM Conference on Principles of Distributed Computing. 1984.
[12]
Staskauskas M.G. The formal specification and design of a distributed electronic funds transfer system. IEEE Trans. Computers, 37, 12. (1988).
[13]
Staskauskas M.G. An exercise in verifying concurrent programs in industry: The I/O subsystem. In Proceedings of the 10th International Phoenix Conference on Computers and Communications (March 1991).
[14]
Staskauskas M.G. Specification and Verification of Large-Scale Reactive Programs. Technical Report TR-92- 34, Department of Computer Sciences, The University of Texas at Austin, August 1992. Available by anonymous FTP at site ftp.cs.utexas.edu, file pub/techreports/TR92-34.ps.Z.
[15]
Staskauskas M.G. Formal derivation of concurrent programs: An example from industry. IEEE Trans. Soft. Eng. 19, 5 (1993).
[16]
Wing J.M. A specifier's introduction to formal methods. IEEE Computer 23, 9 (1990).
Index Terms
- An experience in the formal verification of industrial software
Recommendations
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
A candid industrial evaluation of formal software verification using model checking
ICSE Companion 2014: Companion Proceedings of the 36th International Conference on Software EngineeringModel checking is a powerful formal analytical approach to verifying software and hardware systems. However, general industrial adoption is far from widespread. Some difficulties include the inaccessibility of techniques and tools and the need for ...
Industrial Strength Formal Verification Techniques for Hardware Designs
VLSID '97: Proceedings of the Tenth International Conference on VLSI Design: VLSI in Multimedia ApplicationsThe past decade has seen tremendous progress in the application of formal methods for hardware design and verification. While a number of different techniques based on BDDs, symbolic simulation, special-purpose decision procedures, model checking, and ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Dec. 1996
149 pages
Copyright © 1996 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 December 1996
Published in CACM Volume 39, Issue 12es
Check for updates
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 599Total Downloads
- Downloads (Last 12 months)70
- Downloads (Last 6 weeks)10
Reflects downloads up to 02 Mar 2025
Other Metrics
Citations
Cited By
View all- Staskauskas M(1993)Formal Derivation of Concurrent ProgramsIEEE Transactions on Software Engineering10.1109/32.23201519:5(503-528)Online publication date: 1-May-1993
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in