Abstract
We advocate an automated refinement approach to developing programs and their proofs. The approach is partially embodied in the Specware system [6] which has found industrial and government applications. Our view is that the future of software engineering lies in the tight integration of synthesis and analysis processes.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Becker, M., Gilham, L., Smith, D. R. Planware II: Synthesis of schedulers for complex resource systems. Tech. rep. Kestrel Technology (2003)
Boehm, B.: Software Engineering Economics. Prentice-Hall, Englewood Cliffs (1981)
Coglio, A.: Toward automatic generation of provably correct Java Card applets. In: Proc. 5th ECOOP Workshop on Formal Techniques for Java-like Programs (July 2003)
Green, C.: Application of theorem proving to problem solving. In: Proceedings of the First International Joint Conference on Artificial Intelligence, pp. 219–239 (1969)
Green, C., Westfold, S.: Experiments suggest high level formal models and automated code synthesis significantly increase dependability. Tech. Rep. KES.U.00.8, Kestrel Institute (January 2001)
Kestrel Institute. Specware System and documentation (2003), http://www.specware.org/
Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems 2(1), 90–121 (1980)
Pavlovic, D., Smith, D.R.: Composition and refinement of behavioral specifications. In: Proceedings of Sixteenth International Conference on Automated Software Engineering, pp. 157–165. IEEE Computer Society Press, Los Alamitos (2001)
Smith, D.R.: KIDS – a semi-automatic program development system. IEEE Transactions on Software Engineering Special Issue on Formal Methods in Software Engineering 16(9), 1024–1043 (1990)
Smith, D.R.: Constructing specification morphisms. Journal of Symbolic Computation, Special Issue on Automatic Programming 15(5-6), 571–606 (1993)
Smith, D.R.: Toward a classification approach to design. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 62–84. Springer, Heidelberg (1996)
Smith, D.R.: Mechanizing the development of software. In: Broy, M., Steinbrueggen, R. (eds.) Calculational System Design, Proceedings of the NATO Advanced Study Institute, pp. 251–292. IOS Press, Amsterdam (1999)
Smith, D.R., Lowry, M.R.: Algorithm theories and design tactics. Science of Computer Programming 14( 2-3), 305–321 (1990)
Whalen, M., Schumann, J., Fischer, B.: Synthesizing certified code. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 431–450. Springer, Heidelberg (2002)
Whittle, J., Schumann, J. Automating the implementation of Kalman filter algorithms. Tech. rep. NASA Ames Automated Software Engineering Group(submitted, 2004)
Widmaier, J., Schmidts, C., Huang, X.: Producing more reliable software: Mature software engineering process vs. state-of-the-art technology? In: Proceedings of the International Conference on Software Engineering 2000, Limerick, Ireland, pp. 87–92. ACM Press, New York (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Smith, D.R. (2008). Generating Programs Plus Proofs by Refinement. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)