Roadmap for enhanced languages and methods to aid verification

ABSTRACT

This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

References

1. M. Abadi and L. Lamport. The existence of refinement mappings. Technical Report 29, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, Aug. 1988. A shorter version appeared in Proceedings of the LICS Conference, Edinburgh, Scotland, July 1988.]]
2. M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73--132, Jan. 1993.]]
3. J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, Aug. 1996.]]
4. J.-R. Abrial, E. Börger, and H. Langmaack, editors. Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control, volume 1165 of Lecture Notes in Computer Science. Springer-Verlag, 1996.]]
5. J.-R. Abrial and S. Hallerstede. Refinement, decomposition, and instantiation of discrete models: Application to Event-B. Fundamenta Informaticae, XXI, 2006.]]
6. Ádám Darvas and P. Müller. Reasoning about method calls in interface specifications. Journal of Object Technology, 5(5):59--85, June 2006.]]
7. A. L. Ambler, D. I. Good, J. C. Browne, W. F. Burger, R. M. Choen, C. G. Hoch, and R. E. Wells. Gypsy: a language for specification and implementation of verifiable programs. ACM SIGPLAN Notices, 12(3):1--10, Mar. 1977. Proceedings of the ACM Conference on Language Design for Reliable Software.]]
8. K. Araki, S. Gnesi, and D. Mandrioli, editors. FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings, volume 2805 of Lecture Notes in Computer Science. Springer-Verlag, 2003.]]
9. AspectJ Team. The AspectJ programming guide. Available from http://eclipse.org/aspectj, Oct. 2004.]]
10. E. Astesiano. Inductive and operational semantics. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Reports, pages 51--136. Springer-Verlag, New York, NY, 1991.]]
11. L. Augustsson. Cayenne --- a language with dependent types. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP '98), volume 34(1) of ACM SIGPLAN Notices, pages 239--250. ACM, June 1999.]]
12. B. E. Aydemier, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. In Theorem Proving in Higher Order Logics: 18th International Conference, Lecture Notes in Computer Science. Springer-Verlag, June 2005.]]
13. B-Core (UK) Limited. B-toolkit manuals. http://www.b-core.com, 1999.]]
14. R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer-Verlag, 1998.]]
15. R. J. R. Back. Refinement calculus, part II: Parallel and reactive programs. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, LNCS 430. Springer-Verlag, 1990.]]
16. R. J. R. Back and K. Sere. Stepwise refinement of parallel algorithms. Science of Computer Programming, 13(2-3):133--180, 1990.]]
17. R. J. R. Back and K. Sere. Stepwise refinement of parallel algorithms. Science of Computer Programming, 13(2-3):133--180, 1990.]]
18. J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison Wesley, New York, NY, 2003.]]
19. M. Barnett, R. DeLine, M. Fähndrich, K. R. M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27--56, 2004.]]
20. M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart devices (CASSIS 2004), volume 3362 of Lecture Notes in Computer Science, pages 49--69. Springer-Verlag, 2005.]]
21. D. Batory. Multi-level models in model driven development, product-lines, and metaprogramming. IBM Syst. J., 3, 2006.]]
22. D. S. Batory, J. N. Sarvela, and A. Rauschmayer. Scaling step-wise refinement. IEEE Transactions on Software Engineering, 30(6):355--371, June 2004.]]
23. M. Becker, L. Gilham, and D. R. Smith. Planware II: Synthesis of schedulers for complex resource systems. Technical report, Kestrel Technology, 2003.]]
24. M. Bidoit and P. D. Mosses. Casl User Manual. LNCS 2900 (IFIP Series). Springer-Verlag, 2004.]]
25. H.-J. Boehm. Side effects and aliasing can have simple axiomatic descriptions. ACM Trans. Prog. Lang. Syst., 7(4):637--655, Oct. 1985.]]
26. G. Booch. Growing the uml. Software and Systems Modeling, 1(2):157--160, Dec. 2002.]]
27. L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3):212--232, June 2005.]]
28. R. M. Burstall and J. A. Goguen. Putting theories together to make specifications. In Fifth International Joint Conference on Artifical Intelligence, MIT, Cambridge, Mass., volume 2, pages 1045--1058. IJCAI-77, Department of Computer Science, Carnegie Mellon, Pittsburgh, Aug. 1977.]]
29. R. M. Burstall and J. A. Goguen. The semantics of CLEAR, a specification language. In Abstract Software Specification, Copenhagen Winter School, volume 86 of Lecture Notes in Computer Science, pages 292--332. Springer-Verlag, New York, NY, 1980. Also University of Edinburgh, Department of Computer Science, Internal Report, CSR-65-80, Feb, 1980.]]
30. M. J. Butler. Stepwise refinement of communicating systems. Sci. Comput. Programming, 27(2):139--173, 1996.]]
31. M. J. Butler. On the use of data refinement in the development of secure communications systems. Formal Aspects of Computing, 14(1):2--34, 2002.]]
32. M. J. Butler, E. Sekerinski, and K. Sere. An action system approach to the steam boiler problem. In Abrial et al. {4} FMIA95, pages 129--148.]]
33. J. Charles. Adding native specifications to JML. In Workshop on Formal Techniques for Java-like Programs (FTfJP), July 2006.]]
34. C. Chen and H. Xi. Combining programming with theorem proving. In Proceedings of the 10th International Conference on Functional Programming (ICFP05), Sept. 2005.]]
35. ClearSy. Atelier B, user and reference manuals. http://tinyurl.com/lkj72, 1996.]]
36. A. Coglio and C. Green. A constructive approach to correctness, exemplified by a generator for certified Java Card appplets. In Proc. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments, Oct. 2005.]]
37. C. Colby, P. Lee, G. C. Necula, F. Blau, M. Plesko, and K. Cline. A certifying compiler for Java. In PLDI '00: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, pages 95--107, New York, NY, USA, 2000. ACM Press.]]
38. R. L. Constable. Assigning meaning to proofs: a semantic basis for problem solving environments. In M. Broy, editor, Constructive Methods in Computing Science, volume F55 of NATO ASI Series, pages 63--91. Springer-Verlag, New York, NY, 1989.]]
39. J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of the 22nd International Conference on Software Engineering, pages 439--448, New York, NY, June 2000. ACM Press.]]
40. K. Czarnecki and U. W. Eisenecker. Generative Programming: Methods, Tools, and Applications. Addison-Wesley, 2000.]]
41. CZT Partners. Community Z tools. http://czt.sourceforge.net/, 2006.]]
42. W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison, volume 47 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, NY, 1998.]]
43. W. P. de Roever, H. Langmaack, and A. Pnueli, editors. Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures, volume 1536 of Lecture Notes in Computer Science. Springer-Verlag, 1998.]]
44. D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Palo Alto, Dec 1998.]]
45. S. H. Edwards, W. D. Heym, T. J. Long, M. Sitaraman, and B. W. Weide. Part II: Specifying components in RESOLVE. ACM SIGSOFT Software Engineering Notes, 19(4):29--39, Oct 1994.]]
46. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, New York, NY, 1985.]]
47. D. R. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proc. 4th Symp. OS Design and Int'l (OSDI 2000), pages 1--16. ACM, 2000.]]
48. M. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):99--123, Feb. 2001.]]
49. D. Evans. Static detection of dynamic memory errors. ACM SIGPLAN Notices, 31(5):44--53, May 1996. Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).]]
50. M. Fähndrich and K. R. M. Leino. Declaring and checking non-null types in an object-oriented langauge. In OOPSLA '03: Proceedings of the 18th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, volume 38(11) of ACM SIGPLAN Notices, pages 302--312, New York, NY, Nov. 2003. ACM.]]
51. K. Finney. Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering, 22(2):158--159, Feb. 1996.]]
52. B. Fischer and J. Schumann. Generating data analysis programs from statistical models. Journal of Functional Programming, 13(3):483--508, 2003.]]
53. C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. In J. N. Oliveira and P. Zave, editors, FME 2001: Formal Methods for Increasing Software Productivity, volume 2021 of Lecture Notes in Computer Science, pages 500--517. Springer, Mar. 2001.]]
54. K. Futatsugi, J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 52--66. ACM, Jan. 1985.]]
55. J. A. Goguen and G. Malcolm. Algebraic Semantics of Imperative Programs. MIT Press, Cambridge, MA, 1996.]]
56. J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In R. T. Yeh, editor, Current Trends in Programming Methodology, volume 4, pages 80--149. Prentice-Hall, Inc., Englewood Cliffs, N.J., 1978.]]
57. J. Guttag and J. J. Horning. The algebraic specification of abstract data types. Acta Informatica, 10(1):27--52, 1978.]]
58. J. V. Guttag, J. J. Horning, S. Garland, K. Jones, A. Modet, and J. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, New York, NY, 1993.]]
59. K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4), Apr. 2000.]]
60. I. J. Hayes, M. Jackson, and C. B. Jones. Determining the specification of a control system from that of its environment. In Araki et al. \citeFME03, pages 154--169.]]
61. E. C. R. Hehner. A Practical Theory of Programming. Texts and Monographs in Computer Science. Springer-Verlag, 1993. Available from http://www.cs.utoronto.ca/~hehner/aPToP.]]
62. E. C. R. Hehner. Formalization of time and space. Formal Aspects of Computing, 10:290--306, 1998.]]
63. M. V. Hermenegildo, G. Puebla, F. Bueno, and P. López-García. Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Sci. Comput. Program., 58(1-2):115--140, 2005.]]
64. P. Hilfinger, G. Feldman, I. K. Robert Fitzgerald, R. L. London, K. V. S. Prasad, V. R. Prasad, J. Rosenberg, M. Shaw, and W. A. W. (editor). (preliminary) an informal definition of Alphard. Technical Report CMU-CS-78-105, School of Computer Science, Carnegie Mellon University, 1978.]]
65. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576--580,583, Oct. 1969.]]
66. C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972.]]
67. C. A. R. Hoare, I. J. Hayes, H. Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sorensen, J. M. Spivey, and B. A. Sufrin. Laws of programming. Commun. ACM, 30(8):672--686, Aug. 1987. See corrections in the September 1987 CACM.]]
68. C. A. R. Hoare, N. Shankar, and J. Misra, editors. Proc. IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments, Zürich, Switzerland, Oct. 2005.]]
69. T. Hoare. The verifying compiler: A grand challenge for computing research. J. ACM, 50(1):63--69, Jan. 2003.]]
70. T. Hoare, J. Misra, and N. Shankar. The IFIP working conference on verified software: Theories, tools, experiments. http://tinyurl.com/nrhdl, Oct. 2005.]]
71. D. Hovemeyer. Simple and Effective Static Analysis to Find Bugs. PhD thesis, University of Maryland, July 2005.]]
72. W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, Inc., New York, NY, 1980.]]
73. R. Inc. Software Refinery, Mar. 2006. http://www.reasoning.com/.]]
74. International Organization for Standardization. Ada 95 Reference Manual. The Language. The Standard Libraries, Jan. 1995. ANSI/ISO/IEC-8652:1995.]]
75. B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java classes (preliminary report). In OOPSLA '98 Conference Proceedings, volume 33(10) of ACM SIGPLAN Notices, pages 329--340. ACM, Oct. 1998.]]
76. K. Jensen and N. Wirth. PASCAL User Manual and Report (third edition). Springer-Verlag, New York, NY, 1985. Revised to the ISO Standard by Andrew B. Mickel and James F. Miner.]]
77. C. B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition, 1990.]]
78. I. T. Kassios. A Theory of Object-Oriented Refinement. PhD thesis, University of Toronto, 2006. To appear.]]
79. Kestrel Development Corporation. Specware System and documentation, 2004. http://www.specware.org/.]]
80. G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. G. Griswold. An overview of AspectJ. In J. L. Knudsen, editor, ECOOP 2001 --- Object-Oriented Programming 15th European Conference, Budapest Hungary, volume 2072 of Lecture Notes in Computer Science, pages 327--353. Springer-Verlag, Berlin, June 2001.]]
81. J. Krone, W. F. Ogden, and M. Sitaraman. Modular verification of performance constraints. In ACM OOPSLA Workshop on Specification and Verification of Component-Based Systems (SAVCBS), pages 60--67, 2001.]]
82. L. Lamport. A simple approach to specifying concurrent systems. Commun. ACM, 32(1):32--45, Jan. 1989.]]
83. L. Lamport. The temporal logic of actions. ACM Trans. Prog. Lang. Syst., 16(3):872--923, May 1994.]]
84. B. W. Lampson, J. L. Horning, R. L. London, J. G. Mitchell, and G. J. Popek. Report on the programming language Euclid. Technical Report CSL-81-12, Xerox Palo Alto Research Centers, Oct. 1981. Also SIGPLAN Notices, 12(2), February, 1977.]]
85. J. R. Larus, T. Ball, M. Das, R. DeLine, M. Fähndrich, J. Pincus, S. K. Rajamani, and R. Venkatapathy. Righting software. IEEE Software, 21:92--100, 2004.]]
86. G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, 55(1-3):185--208, Mar. 2005.]]
87. K. R. M. Leino and P. Müller. Object invariants in dynamic contexts. In M. Odersky, editor, European Conference on Object-Oriented Programming (ECOOP), volume 3086 of Lecture Notes in Computer Science, pages 491--516. Springer-Verlag, June 2004.]]
88. T. Lev-Ami and S. Sagiv. TVLA: A system for implementing static analyses. In J. Palsberg, editor, Static Analysis, 7th International Symposium, SAS 2000, Proceedings, volume 1824 of Lecture Notes in Computer Science, pages 280--301. Springer, 2000.]]
89. B. Liskov and J. Guttag. Abstraction and Specification in Program Development. The MIT Press, Cambridge, Mass., 1986.]]
90. B. Liskov, A. Snyder, R. Atkinson, and C. Schaffert. Abstraction mechanisms in CLU. Commun. ACM, 20(8):564--576, Aug. 1977.]]
91. B. Liskov and W. Weihl. Specifications of distributed programs. Distributed Computing, 1:102--118, 1986.]]
92. R. L. London, J. V. Guttag, J. J. Horning, B. W. Lampson, J. G. Mitchell, and G. J. Popek. Proof rules for the programming language Euclid. Acta Informatica, 10(1):1--26, 1978.]]
93. R. L. London, M. Shaw, and W. A. Wulf. Abstraction and verification in Alphard: a symbol table example. Technical report, Information Sciences Institute, USC, Dec. 1976.]]
94. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, New York, NY, 1992.]]
95. Matisse Partners. Matisse: Methodologies and technologies for industrial strength systems engineering. http://www.matisse.qinetiq.com/, 2003.]]
96. C. McBride and J. McKinna. The view from the left. Journal of Functional Programming, 14(1), 2004.]]
97. B. McCloskey, F. Zhou, D. Gay, and E. Brewer. Autolocker: synchronization inference for atomic sections. In Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 06), volume 41, 1 of ACM SIGPLAN Notices, pages 346--358, New York, Jan. 2006. ACM Press.]]
98. B. Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, NY, 1992.]]
99. B. Meyer. Object-oriented Software Construction. Prentice Hall, New York, NY, second edition, 1997.]]
100. C. Morgan. Programming from Specifications: Second Edition. Prentice Hall International, Hempstead, UK, 1994.]]
101. C. Morgan and T. Vickers, editors. On the refinement calculus. Formal approaches of computing and information technology series. Springer-Verlag, New York, NY, 1994.]]
102. J. B. Morris. Programming by successive refinement of data abstractions. Software---Practice & Experience, 10(4):249--263, Apr. 1980.]]
103. G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. ACM Trans. Prog. Lang. Syst., 21(3):527--568, May 1999.]]
104. P. Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of Lecture Notes in Computer Science. Springer-Verlag, 2002.]]
105. P. Müller, A. Poetzsch-Heffter, and G. T. Leavens. Modular specification of frame properties in JML. Concurrency and Computation: Practice and Experience, 15(2):117--154, Feb. 2003.]]
106. P. Müller, A. Poetzsch-Heffter, and G. T. Leavens. Modular invariants for layered object structures. Technical Report 424, ETH Zurich, Mar. 2005.]]
107. A. Narayanan and G. Karsai. Towards verifying model transformations. In R. Bruni and D. Varró, editors, 5th International Workshop on Graph Transformation and Visual Modeling Techniques, Vienna, pages 185--194, Apr 2006.]]
108. G. C. Necula. Proof-carrying code. In Conference Record of POPL 97: The 24TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, pages 106--119, New York, NY, Jan. 1997. ACM.]]
109. F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.]]
110. J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. In Proceedings of RV'01, First Workshop on Runtime Verification. Elsevier, July 2001.]]
111. T. Nipkow, L. Paulson, and M. Menzel. Isabelle/HOL --- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002.]]
112. T. Nipkow, D. von Oheimb, and C. Pusch. μJava: Embedding a programming language in a theorem prover. In F. L. Bauer and R. Steinbrüggen, editors, Foundations of Secure Computation, volume 175 of NATO Science Series F: Computer and Systems Sciences, pages 117--144. IOS Press, 2000.]]
113. J. Noble, J. Vitek, and J. Potter. Flexible alias protection. In E. Jul, editor, ECOOP '98 -- Object-Oriented Programming, 12th European Conference, Brussels, Belgium, volume 1445 of Lecture Notes in Computer Science, pages 158--185. Springer-Verlag, July 1998.]]
114. B. Nordström and K. Peterson. Types and specifications. In R. E. A. Mason, editor, Information Processing 83, pages 915--920. Elsevier Science Publishers B.V. (North-Holland), Sept. 1983. Proceedings of the IFIP 9th World Computer Congress, Paris, France.]]
115. B. Nordström, K. Peterson, and J. M. Smith. Programming in Martin-Lof's Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, New York, NY, 1990.]]
116. W. F. Ogden, M. Sitaraman, B. W. Weide, and S. H. Zweben. Part I: The RESOLVE framework and discipline --- a research synopsis. ACM SIGSOFT Software Engineering Notes, 19(4):23--28, Oct. 1994.]]
117. S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107--125, Feb. 1995.]]
118. Rodin Partners. Rodin: Rigorous open development environment for complex systems. http://rodin.cs.ncl.ac.uk/, 2006.]]
119. E. Rodríguez, M. B. Dwyer, C. Flanagan, J. Hatcliff, G. T. Leavens, and Robby. Extending JML for modular specification and verification of multi-threaded programs. In A. P. Black, editor, ECOOP 2005 --- Object-Oriented Programming 19th European Conference, Glasgow, UK, volume 3586 of Lecture Notes in Computer Science, pages 551--576. Springer-Verlag, Berlin, July 2005.]]
120. G. Rose. Object-Z. In S. Stepney, R. Barden, and D. Cooper, editors, Object Orientation in Z, Workshops in Computing, pages 59--77. Springer-Verlag, Cambridge CB2 1LQ, UK, 1992.]]
121. M. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Syst., 24(3):217--298, May 2002.]]
122. D. A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Inc., Boston, Mass., 1986.]]
123. P. G. Selinger, M. M. Astrahan, D. D. Chamberlin, R. A. Lorie, and T. G. Price. Access path selection in a relational database management system. In Proceedings of the ACM SIGMOD International Conference on Management of Data, pages 23--34, 1979.]]
124. M. Shaw. ALPHARD: Form and Content. Springer-Verlag, New York, NY, 1981.]]
125. T. Sheard. Languages of the future. In D. Schmidt, editor, OOPSLA '04: Proceedings of the 19th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, volume 39(11) of ACM SIGPLAN Notices, New York, NY, Oct. 2004. ACM.]]
126. M. Sitaraman, G. Kulczycki, J. Krone, W. F. Ogden, and A. L. N. Reddy. Performance specifications of software components. In Proceedings of the 2001 Symposium on Software Reusability (SSR-01), volume 26, 3 of SSR Record, pages 3--10, New York, May 18--20 2001. ACM Press.]]
127. M. Sitaraman, T. J. Long, B. W. Weide, E. J. Harner, and L. Wang. A formal approach to component-based software engineering: Education and evaluation. In Twenty Third International Conference on Software Engineering, pages 601--609. IEEE, 2001.]]
128. M. Sitaraman, B. W. Weide, and W. F. Ogden. On the practical need for abstraction relations to verify abstract data type representations. IEEE Transactions on Software Engineering, 23(3):157--170, Mar. 1997.]]
129. D. R. Smith. KIDS -- a semi-automatic program development system. IEEE Transactions on Software Engineering, 16(9):1024--1043, 1990.]]
130. D. R. Smith. Mechanizing the development of software. In M. Broy and R. Steinbrueggen, editors, Calculational System Design, Proceedings of the NATO Advanced Study Institute, pages 251--292. IOS Press, Amsterdam, 1999.]]
131. J. M. Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York, NY, second edition, 1992.]]
132. S. Stepney, D. Cooper, and J. Woodcock. An electronic purse: Specification, refinement, and proof. Technical monograph PRG-126, Oxford University Computing Laboratory, July 2000.]]
133. M. E. Stickel, R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood. Deductive composition of astronomical software from subroutine libraries. In A. Bundy, editor, 12th Conference on Automated Deduction, volume 814 of Lecture Notes in Computer Science. Springer-Verlag, 1994.]]
134. Stratego documentation. http://tinyurl.com/nr2c5, Mar. 2006.]]
135. F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121--189, 1995.]]
136. D. E. Turk, R. B. France, B. Rumpe, and G. Georg. Model-driven approaches to software development. In OOIS Workshops, pages 229--230, 2002.]]
137. J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Software (TACAS), volume 2031 of Lecture Notes in Computer Science, pages 299--312. Springer-Verlag, 2001.]]
138. A. van Lamsweerde. Requirements engineering in the year 00: A research perspective. In Proceedings of the 22nd International Conference on Software Engineering, pages 5--19, New York, NY, June 2000. ACM Press.]]
139. P. Voda. What can we gain by integrating a language processor with a theorem prover. unpublished; available from the author's web site, 2003.]]
140. J. Warmer and A. Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison Wesley Longman, Reading, Mass., 1999.]]
141. M. Weiser. Program slicing. IEEE Transactions on Software Engineering, SE-10(4):352--357, July 1984.]]
142. E. Westbrook, A. Stump, and I. Wehrman. A language-based approach to functionally correct imperative programming. In Proceedings of the 10th International Conference on Functional Programming (ICFP05), 2005.]]
143. J. M. Wing. Writing Larch interface language specifications. ACM Trans. Prog. Lang. Syst., 9(1):1--24, Jan. 1987.]]
144. J. M. Wing. A specifier's introduction to formal methods. Computer, 23(9):8--24, Sept. 1990.]]
145. N. Wirth. The programming language pascal. Acta Informatica, 1(1):35--63, 1971.]]
146. H. Xi. Facilitating program verification with dependent types. In Proceedings of the International Conference on Software Engineering and Formal Methods, pages 72--81, 2003.]]
147. P. Zave and M. Jackson. Four dark corners of requirements engineering. ACM Transactions on Software Engineering and Methodology, 6(1):1--30, Jan. 1997.]]

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Reliability

    • Validation

• Hardware

  • Hardware validation

    • Functional verification

      • Assertion checking

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • Compilers

      • Translator writing systems and compiler generators

    • Context specific languages

      • Specialized application languages

    • Formal language definitions

      • Semantics

    • General programming languages

      • Language features

        • Abstract data types

        • Classes and objects

      • Language types

        • Extensible languages

        • Very high level languages

    • Software libraries and repositories

    • System description languages

      • Specification languages

  • Software organization and properties

    • Software functional properties

      • Correctness

      • Formal methods

        • Model checking

    • Software system structures

      • Abstraction, modeling and modularity

      • Software architectures

• Theory of computation

  • Logic

    • Programming logic

    • Proof theory

    • Verification by model checking

  • Semantics and reasoning

    • Program constructs

      • Type structures

    • Program reasoning

      • Assertions

      • Invariants

      • Pre- and post-conditions

      • Program analysis

      • Program specifications

      • Program verification

    • Program semantics