{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T18:37:04Z","timestamp":1761935824532,"version":"build-2065373602"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Real-Time Systems"],"published-print":{"date-parts":[[1996,9]]},"DOI":"10.1007\/bf00365316","type":"journal-article","created":{"date-parts":[[2004,11,2]],"date-time":"2004-11-02T12:58:28Z","timestamp":1099400308000},"page":"145-171","source":"Crossref","is-referenced-by-count":43,"title":["Combining static worst-case timing analysis and program proof"],"prefix":"10.1007","volume":"11","author":[{"given":"Roderick","family":"Chapman","sequence":"first","affiliation":[]},{"given":"Alan","family":"Burns","sequence":"additional","affiliation":[]},{"given":"Andy","family":"Wellings","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","unstructured":"Carr\u00e9, B., and Garnsworthy, J. 1990. Experiences with SPARK and its support tool, the SPARK Examiner. Ada User 11 (Supplement):"},{"key":"CR2","unstructured":"Carr\u00e9, B. A. 1990. Validation Techniques II. Software Engineering for Electronic System Designers. Peter Peregrinus Ltd. 248?255."},{"key":"CR3","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1145\/2363.2366","volume":"7","author":"B. A. Carr\u00e9","year":"1985","unstructured":"Carr\u00e9, B. A., and Bergeretti, J. F. 1985. Information-flow and data-flow analysis of while-programs. ACM Transactions on Programming Languages and Systems 7: 37?61.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR4","unstructured":"Carr\u00e9, B. A., Jennings, T. J., Maclennan, F. J., Farrow, P. F., and Garnsworthy, J. R. 1992. SPARK: the SPADE Ada Kernel (edition 3.1). Program Validation Ltd."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Chapman, R. 1994. Worst-case timing analysis via finding longest paths in SPARK Ada basic-path graphs. Department of Computer Science, University of York.","DOI":"10.1145\/192867.192873"},{"key":"CR6","unstructured":"Chapman, R. 1995. Static Timing Analysis and Program Proof. DPhil Thesis. Department of Computer Science, University of York, U.K. YCST-95-05. Also available via FTP from ftp.cs.york.ac.uk in file\/reports\/YCST-95-05.tar.Z"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Char, B. W., Geddes, K. O., G. H., Leong, B. L., Monagan, M. B., and Watt, S. M. 1992. First Leaves: A Tutorial Introduction to Maple V. Springer-Verlag.","DOI":"10.1007\/978-1-4615-6996-1"},{"key":"CR8","unstructured":"Coen-Porisini, A., and DePaoli, F. 1990. SYMBAD?A symbolic executor of sequential Ada programs. Safety of Computer Control Systems (SAFECOMP '90), Gatwick, England, IFAC Symposia Series ISS.17, 105?111."},{"key":"CR9","first-page":"226","volume-title":"Third European Software Engineering Conference?ESEC '91 Milano, Italy","author":"A. Coen-Porisini","year":"1991","unstructured":"Coen-Porisini, A., and DePaoli, F. 1991. SESAda, an Environment supporting Software Specialization. Third European Software Engineering Conference?ESEC '91 Milano, Italy, Springer-Verlag, Berlin, 226?289."},{"key":"CR10","unstructured":"DoD 1983. Reference Manual for the Ada Programming Language ANSI\/MIL-STD 1815A."},{"key":"CR11","unstructured":"Firth, J. R., Forsyth, C. H., and Wand, I. C. 1995. The Compilation of Ada. Department of Computer Science, University of York."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Goldberg, A., Wang, T. C., and Zimmerman, D. 1994. Applications of feasible path analysis to program testing. Proceedings of the International Symposium on Software Testing and Analysis, Seattle, Washington.","DOI":"10.1145\/186258.186523"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0165-6074(83)90185-0","volume":"12","author":"W. A. Halang","year":"1983","unstructured":"Halang, W. A. 1983. On real-time features available in high-level languages and yet to be implemented. Microprocessing and Microprogramming 12: 79?87.","journal-title":"Microprocessing and Microprogramming"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Halang, W. A. 1989. A Priori Execution Time Analysis for Parallel Processes. Proceedings of the Euromicro workshop on real-time systems, IEEE computer society press, 62?65.","DOI":"10.1109\/EMWRT.1989.43442"},{"issue":"3","key":"CR15","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1145\/356674.356677","volume":"8","author":"S. L. Hantler","year":"1976","unstructured":"Hantler, S. L., and King, J. C. 1976. An introduction to proving the correctness of programs. ACM Computing Surveys 8(3): 331?353.","journal-title":"ACM Computing Surveys"},{"issue":"2","key":"CR16","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/BF01088803","volume":"7","author":"M. G. Harmon","year":"1994","unstructured":"Harmon, M. G., Baker, T. P., and Whalley, D. B. 1994. A retargetable technique for predicting the execution time of code segments. Journal of Real Time Systems 7(2): 159?182.","journal-title":"Journal of Real Time Systems"},{"issue":"8","key":"CR17","doi-asserted-by":"crossref","first-page":"880","DOI":"10.1109\/32.57625","volume":"16","author":"J. Huang","year":"1990","unstructured":"Huang, J. 1990. State constraints and pathwise decomposition of programs. IEEE Transactions on Software Engineering 16(8): 880?896.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR18","unstructured":"Internetrics 1995. Ada95 Reference Manual. International Standard ANSI\/ISO\/IEC-8652:1995. International Standards Organisation."},{"issue":"1","key":"CR19","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1109\/TSE.1986.6312924","volume":"12","author":"F. Jahanian","year":"1986","unstructured":"Jahanian, F., and Mok, A. K. 1986. Safety analysis of timing properties in real-time systems. IEEE Transactions on Software Engineering SE-12(1): 96?109.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"Jasper, R., Brennan, M., Williamson, K., Currier, C., and Zimmerman, D. 1994. Test data generation and feasible path analysis. Internanational Symposium on Software Testing and Analysis, Seattle, Washington.","DOI":"10.1145\/186258.187150"},{"issue":"5","key":"CR21","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1002\/spe.4380150504","volume":"15","author":"R. A. Kemmerer","year":"1985","unstructured":"Kemmerer, R. A., and Eckmann, S. T. 1985. UNISEX: A UNIx-based Symbolic EXecutor for Pascal. Software?Practice and Experience 15(5): 439?458.","journal-title":"Software?Practice and Experience"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"Ko, L., and Whalley, D. 1995. Supporting user-friendly analysis of timing constraints. Proceedings of the 1995 workshop on Language, Compiler and Tool Support for Real-Time Systems (in conjunction with the ACM conference on Programming Language Design and Implementation), La Jolla, California, USA.","DOI":"10.1145\/216636.216668"},{"key":"CR23","first-page":"223","volume-title":"IEEE Real-Time Systems Symposium","author":"H. Kopetz","year":"1992","unstructured":"Kopetz, H., Fohler, G., Gr\u00fcnsteidl, G., Kantz, H., Pospischil, G., Puschner, P., Reisinger, J., Schlatterbeck, R., Sch\u00fctz, W., Vrchoticky, A., and Zainlinger, R. 1992. The Programmer's View of MARS, IEEE Real-Time Systems Symposium, Pheonix, Arizona, USA, IEEE Press, 223?226."},{"key":"CR24","first-page":"98","volume-title":"Proceedings of the Real-Time Systems Symposium","author":"M. Lee","year":"1993","unstructured":"Lee, M., Min, S. L., Park, C. Y., Bae, Y. H., Shin, H., and Kim, C. S. 1993. A Dual-Mode Instruction Prefetch Scheme for Improved Worst Case and Average Case Program Execution Times. Proceedings of the Real-Time Systems Symposium, Raliegh-Durham, North Carolina, IEEE Computer Society Press, 98?105."},{"key":"CR25","first-page":"97","volume-title":"Real-Time Systems Symposium","author":"S. Lim","year":"1994","unstructured":"Lim, S., Rhee, B., Shin, H., Bae, Y. H., Min, S. L., Park, K., Jang, G. T., Park, C. Y., and Kim, C. S. 1994. An accurate worst-case timing analysis technique for RISC processors. Real-Time Systems Symposium, Puerto-Rico, IEEE Press, 97?108."},{"key":"CR26","first-page":"182","volume-title":"Real-Time Systems Symposium","author":"J. Liu","year":"1994","unstructured":"Liu, J., and Lee, H. 1994. Deterministic upperbounds of the worst-case execution times of cached programs. Real-Time Systems Symposium, Puerto-Rico, IEEE Press, 182?191."},{"key":"CR27","unstructured":"Manna, Z. 1974. Mathematical Theory of Computation. McGraw Hill."},{"key":"CR28","unstructured":"Mok, A. 1989. Evaluating Tight Execution Time Bounds of Programs by Annotations. Proceedings of 6th IEEE Workshop on Real-time operating Systems and Software, 74?80."},{"key":"CR29","unstructured":"Motorola 1985. MC68020 32-Bit Microprocessor User's Manual (2nd edition). Prentice Hall, Inc."},{"key":"CR30","first-page":"172","volume-title":"Real-Time Systems Symposium","author":"F. Mueller","year":"1994","unstructured":"Mueller, F., Arnold, R., and Whalley, D. 1994. Bounding Worst-Case Instruction Cache Performance. Real-Time Systems Symposium, Puerto-Rico, IEEE Press, 172?181."},{"key":"CR31","unstructured":"Nilsen, K., and Narasimhan, K. 1994. Portable Execution Time Analysis for RISC Processors. ACM Workshop on language, compiler and tool support for real-time systems (in conjunction with the 1994 ACM SUGPLAN PLDI conference), Walt Disney World, Florida, USA, University of Maryland."},{"key":"CR32","unstructured":"Nilsen, K. D., and Basumallick, S. 1994. Cache Issues in Real-Time Systems. ACM Workshop on Language, Compiler, and Tool Support for Real-Time Systems (in conjuntion with the 1994 ACM SIGPLAN PLDI conference), Florida, University of Maryland."},{"key":"CR33","unstructured":"Park, C. Y. 1992. Predicting determinstic execution times of real-time programs. PhD Thesis. University of Washington."},{"key":"CR34","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF01088696","volume":"5","author":"C. Y. Park","year":"1993","unstructured":"Park, C. Y. 1993. Predicting program execution times by analyzing static and dynamic program paths. Journal of Real Time Systems 5: 31?62.","journal-title":"Journal of Real Time Systems"},{"issue":"5","key":"CR35","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1109\/2.76286","volume":"24","author":"C. Y. Park","year":"1991","unstructured":"Park, C. Y., and Shaw, A. C. 1991. Experiments with a program timing tool based on source-level timing schema. IEEE Computer 24(5): 48?57.","journal-title":"IEEE Computer"},{"key":"CR36","first-page":"121","volume-title":"ACM SIGPLAN '94 Conference on Programming Language Design and Implementation, Walt Disney World","author":"W. Pugh","year":"1994","unstructured":"Pugh, W. 1994. Counting solutions to Presburger Formulas: How and Why. ACM SIGPLAN '94 Conference on Programming Language Design and Implementation, Walt Disney World, Florida, U.S.A., ACM Press, 121?134."},{"issue":"2","key":"CR37","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/BF00571421","volume":"1","author":"P. Puschner","year":"1989","unstructured":"Puschner, P., and Koza, C. 1989. Calculating the maximum execution time of real-time programs. Journal of Real Time Systems 1(2): 159?176.","journal-title":"Journal of Real Time Systems"},{"key":"CR38","volume-title":"Generation of Path Functions and Verification Conditions for SPARK Programs Edition 1.2(c)","author":"PVL","year":"1992","unstructured":"PVL 1992a. Generation of Path Functions and Verification Conditions for SPARK Programs Edition 1.2(c). Southampton, U.K.: Program Validation Limited."},{"key":"CR39","unstructured":"PVL 1992b. SPARK Examiner Version A Release 1.2(a)."},{"key":"CR40","unstructured":"Radstone 1993. PME 68-23\/23M CPU Manual. Radstone Technologies PLC, Towcester, Northants, U.K."},{"issue":"2","key":"CR41","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0898-1221(93)90322-M","volume":"26","author":"B. D. Raduenz","year":"1993","unstructured":"Raduenz, B. D., Suter, B. W., and Christensen, E. R. 1993. Analysis of an Ada based version of Glassman's general N point fast fourier transform. Computer and Mathematics with Applications 26(2): 61?65.","journal-title":"Computer and Mathematics with Applications"},{"key":"CR42","unstructured":"Sedgewick, R. 1988. Algorithms (2nd edition). Addison-Wesley."},{"issue":"7","key":"CR43","doi-asserted-by":"crossref","first-page":"875","DOI":"10.1109\/32.29487","volume":"15","author":"A. C. Shaw","year":"1989","unstructured":"Shaw, A. C. 1989. Reasoning about time in higher level language software. IEEE Transactions on Software Engineering 15(7): 875?889.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"8","key":"CR44","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1109\/32.83911","volume":"17","author":"A. D. Stoyenko","year":"1991","unstructured":"Stoyenko, A. D., Hamacher, C., and Holt, R. C. 1991. Analyzing hard real-time programs for guaranteed schedulability. IEEE Transactions on Software Engineering 17(8): 737?750.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR45","doi-asserted-by":"crossref","unstructured":"Stoyenko, A. D., Younis, M., Marlowe, T. J., and Halang, W. A. 1992. Enabling Efficient Schedulability Analysis through Conditional Linking and Program Transformations. New Jersey Institute of Technology.","DOI":"10.1016\/B978-0-08-041894-0.50048-4"},{"issue":"3","key":"CR46","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1145\/322261.322272","volume":"28","author":"R. E. Tarjan","year":"1981","unstructured":"Tarjan, R. E. 1981. A unified approach to path problems. Journal of the ACM 28(3): 577?593.","journal-title":"Journal of the ACM"},{"key":"CR47","volume-title":"Validation Code for the Whetstone Benchmark","author":"B. A. Wichmann","year":"1988","unstructured":"Wichmann, B. A. 1988. Validation Code for the Whetstone Benchmark. Teddington, Middlesex, TW11 OLW, U.K.: National Physical Laboratory."},{"key":"CR48","volume-title":"Mathematica: A System for Doing Mathematics by Computer","author":"S. Wolfram","year":"1988","unstructured":"Wolfram, S. 1988. Mathematica: A System for Doing Mathematics by Computer. Redwood City: Addison-Wesley."},{"issue":"4","key":"CR49","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF01088834","volume":"5","author":"N. Zhang","year":"1993","unstructured":"Zhang, N., Burns, A., and Nicholson, M. 1993. Pipelined processors and worst-case execution times. Journal of Real Time Systems 5(4): 319?343.","journal-title":"Journal of Real Time Systems"}],"container-title":["Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00365316.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00365316\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00365316","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T17:47:43Z","timestamp":1585936063000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00365316"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["BF00365316"],"URL":"https:\/\/doi.org\/10.1007\/bf00365316","relation":{},"ISSN":["0922-6443","1573-1383"],"issn-type":[{"type":"print","value":"0922-6443"},{"type":"electronic","value":"1573-1383"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}