ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
An axiomatic basis for computer programming
Full text PdfPdf (659 KB)
Source
Communications of the ACM archive
Volume 12 ,  Issue 10  (October 1969) table of contents
Pages: 576 - 580  
Year of Publication: 1969
ISSN:0001-0782
Author
C. A. R. Hoare  Queen's Univ. of Belfast, Northern Ireland
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 104,   Downloads (12 Months): 652,   Citation Count: 585
Additional Information:

abstract   references   cited by   index terms   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/363235.363259
What is a DOI?

ABSTRACT

In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantage, both theoretical and practical, may follow from a pursuance of these topics.


REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
1
YANOV, Yu I. Logical operator schemes. Kybernetika 1, (1958).
 
2
IGARASHI, S. An axiomatic approach to equivalence problems of algorithms with applications. Ph.D. Thesis 1964. Rep. Compt. Centre, U. Tokyo, 1968, pp. 1-101.
 
3
DE BAKICER, J. W. Axiomatics of simple assignment statements. M.R. 94, Mathematisch Centrum, Amsterdam, June 1968.
 
4
McCARTHY, J. Towards a mathematical theory of computation. Proc. IFIP Cong. 1962, North Holland Pub. Co., Amsterdam, 1963.
 
5
BURSTALL, R. Proving properties of programs by structural induction. Experimental Programming Reports: No. 17 DMIP, Edinburgh, Feb. 1968.
 
6
VAN WIJNGAARDEN, A. Numerical analysis as an independent science. BIT 6 (1966), 66-81.
 
7
J. G Laski, Sets and other types, ALGOL Bulletin  [doi>10.1145/1061098.1061107]
 
8
FLOYD, R. W. Assigning meanings to programs. Proc. Amer. Math. Soc. Symposia in Applied Mathematics, Vol. 19, pp. 19-31.
 
9
NAUR, P. Proof of algorithms by general snapshots. BIT 6 (1966), 310-316.

CITED BY  590
Rogier M. Van Eijk , Frank S. De Boer , Wiebe Van Der Hoek , John-Jules Ch. Meyer, A Verification Framework for Agent Communication, Autonomous Agents and Multi-Agent Systems, v.6 n.2, p.185-219, March 2003
Michael Wooldridge, Semantic Issues in the Verification of Agent Communication Languages, Autonomous Agents and Multi-Agent Systems, v.3 n.1, p.9-31, March 2000
Shmuel Katz , Zohar Manna, Logical analysis of programs, Communications of the ACM, v.19 n.4, p.188-206, April 1976
L. Flon , A. N. Habermann, Towards the construction of verifiable software systems, ACM SIGMOD Record, v.8 n.2, p.141-148, March 1976
Marvin V. Zelkowitz, Perspectives in Software Engineering, ACM Computing Surveys (CSUR), v.10 n.2, p.197-216, June 1978
Manfred Broy , Bernd Krieg-Bruckner, Derivation of Invariant Assertions During Program Development by Transformation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.321-337, July 1980
R. Gerth , A. Pnueli, Rooting UNITY, ACM SIGSOFT Software Engineering Notes, v.14 n.3, p.11-19, May 1989
E. A. Ashcroft , W. W. Wadge, Lucid, a nonprocedural language with iteration, Communications of the ACM, v.20 n.7, p.519-526, July 1977
Frank S. de Boer , Maurizio Gabbrielli , Elena Marchiori , Catuscia Palamidessi, Proving concurrent constraint programs correct, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-108, January 16-19, 1994, Portland, Oregon, United States
Mitchell Wand, A New Incompleteness Result for Hoare's System, Journal of the ACM (JACM), v.25 n.1, p.168-175, Jan. 1978
W. D. Maurer, The teaching of program correctness, ACM SIGCSE Bulletin, v.9 n.1, p.142-144, Feb 1977
Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California
C. Bellon , G. Saucier , J. M. Gobbi, Hardware description levels and test for complex circuits, Proceedings of the 18th conference on Design automation, p.213-219, June 29-July 01, 1981, Nashville, Tennessee, United States
Stephen A. Cook , Derek C. Oppen, An assertion language for data structures, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.160-166, January 20-22, 1975, Palo Alto, California
Daniel Brand, Path Calculus in Program Verification, Journal of the ACM (JACM), v.25 n.4, p.630-651, Oct. 1978
Zohar Manna , Richard Waldinger, Is “sometime” sometimes better than “always”?: Intermittent assertions in proving program correctness, Proceedings of the 2nd international conference on Software engineering, p.32-39, October 13-15, 1976, San Francisco, California, United States
Robert L. Baber, Comparison of Electrical "Engineering" of Heaviside's Times and Software "Engineering" of Our Times, IEEE Annals of the History of Computing, v.19 n.4, p.5-17, October 1997
Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, ACM SIGPLAN Notices, v.36 n.5, p.221-231, May 2001
C. A. R. Hoare, Assertions: A Personal Perspective, IEEE Annals of the History of Computing, v.25 n.2, p.14-25, April 2003
Russell Turpin, A logical approach to data structures, ACM SIGSOFT Software Engineering Notes, v.18 n.5, p.138-148, Dec. 1993
Raymond T. Yeh , Donald I. Good , David R. Musser, New directions in teaching the fundamentals of computer science — discrete structures and computational analysis, ACM SIGCSE Bulletin, v.5 n.1, p.60-67, February 1973
Susan L. Gerhart, Knowledge about programs: A model and case study, ACM SIGPLAN Notices, v.10 n.6, p.88-95, June 1975
A. Udaya Shankar, An introduction to assertional reasoning for concurrent systems, ACM Computing Surveys (CSUR), v.25 n.3, p.225-262, Sept. 1993
George T. Ligler, The assignment axiom and programming language design, Proceedings of the annual conference, p.2-6, October 20-22, 1976, Houston, Texas, United States
Ralph L. London, A view of program verification, ACM SIGPLAN Notices, v.10 n.6, p.534-545, June 1975
Susan Horwitz , Jan Prins , Thomas Reps, Integrating noninterfering versions of programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.3, p.345-387, July 1989
Bowen Alpern , Fred B. Schneider, Verifying temporal properties without temporal logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.1, p.147-167, Jan. 1989
Harlan D. Mills, How to write correct programs and know it, ACM SIGPLAN Notices, v.10 n.6, p.363-370, June 1975
Paul R. Kosinski, A straightforward denotational semantics for non-determinate data flow programs, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.214-221, January 23-25, 1978, Tucson, Arizona
B. J. MacLennan, Fen—an axiomatic basis for program semantics, Communications of the ACM, v.16 n.8, p.468-474, Aug. 1973
Shmuel Katz , Zohar Manna, Towards automatic debugging of programs, ACM SIGPLAN Notices, v.10 n.6, p.143-155, June 1975
Michael Burrows , Martin Abadi , Roger Needham, A logic of authentication, ACM Transactions on Computer Systems (TOCS), v.8 n.1, p.18-36, Feb. 1990
Michel Sintzoff , Axel Van Lamsweerde, Constructing correct and efficient concurrent programs, ACM SIGPLAN Notices, v.10 n.6, p.319-326, June 1975
Ali Mili, A case for teaching program verification: Its importance in the CS curriculum, ACM SIGCSE Bulletin, v.15 n.1, p.2-6, February 1983
Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981
Frank S. De Boer , Maurizio Gabbrielli , Elena Marchiori , Catuscia Palamidessi, Proving concurrent constraint programs correct, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.685-725, Sept. 1997
K. Culik , M. M. Rizki, Logic versus mathematics in computer science education, ACM SIGCSE Bulletin, v.15 n.1, p.14-20, February 1983
Daniel Hoffman , Paul Strooper, State abstraction and modular software development, ACM SIGSOFT Software Engineering Notes, v.20 n.4, p.53-61, Oct. 1995
Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas
J. Mack Adams , James Armstrong , Melissa Smartt, Assertional checking and symbolic execution: An effective combination for debugging, Proceedings of the 1979 annual conference, p.152-156, January 1979
M. Moriconi, A practical approach to semantic configuration management, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.103-113, Dec. 1989
Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992
Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992
Carroll Morgan , Annabelle McIver , Karen Seidel, Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.3, p.325-353, May 1996
Nachum Dershowitz , Zohar Manna, Inference rules for program annotation, Proceedings of the 3rd international conference on Software engineering, p.158-167, May 10-12, 1978, Atlanta, Georgia, United States
Paul R. Kosinski, Mathematical semantics and data flow programming, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.175-184, January 19-21, 1976, Atlanta, Georgia
Subrata Dasgupta, Towards a microprogramming language schema, ACM SIGMICRO Newsletter, v.9 n.4, p.144-153, Dec. 1978
David C. Luckham , Wolfgang Polak, A practical method of documenting and verifying Ada programs with packages, Proceedings of the ACM-SIGPLAN symposium on The ADA programming language, p.113-122, January 1980
John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978
Gleb N. Naumovich , Lori A. Clarke , Leon J. Osterweil, Verification of communication protocols using data flow analysis, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.93-105, Nov. 1996
Richard J. Waldinger , Karl N. Levitt, Reasoning about programs, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.169-182, October 01-03, 1973, Boston, Massachusetts
C. T. Zahn, A phased programming paradigm, ACM SIGCSE Bulletin, v.20 n.1, p.9-12, Feb. 1988
J. Kramer , R. J. Cunningham, Invariants for specifications, Proceedings of the 4th international conference on Software engineering, p.183-193, September 17-19, 1979, Munich, Germany
George S. Avrunin , Jack C. Wileden, Describing and analyzing distributed software system designs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.380-403, July 1985
Stefan Sokolowski, Soundness of Hoare's logic: an automated proof using LCF, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.1, p.100-121, Jan. 1987
Patricia P. Griffiths , Charles J. Prenner, Verifying formal specifications of synchronous processes, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.192-208, January 19-21, 1976, Atlanta, Georgia
Michael J. O'Donnell, A critique of the foundations of Hoare style programming logics, Communications of the ACM, v.25 n.12, p.927-935, Dec 1982
Marco R. Casanova , Phillip A. Bernstein, A Formal System for Reasoning about Programs Accessing a Relational Database, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.386-414, July 1980
Irene Greif , Albert R. Meyer, Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.484-507, Oct. 1981
Gregory R. Andrews , Fred B. Schneider, Concepts and Notations for Concurrent Programming, ACM Computing Surveys (CSUR), v.15 n.1, p.3-43, March 1983
Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976
M. P. Herlihy , J. M. Wing, Axioms for concurrent objects, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.13-26, January 21-23, 1987, Munich, West Germany
Irene Greif , Carl Hewitt, Actor semantics of PLANNER-73, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.67-77, January 20-22, 1975, Palo Alto, California
Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984
John H. Howard, Proving monitors, Communications of the ACM, v.19 n.5, p.273-279, May 1976
Riccardo Pucella, Review of Dynamic Logic (Foundations of Computing): authors of book: D. Harel, D. Kozen and J. Tiuryn, ACM SIGACT News, v.32 n.4, December 2001
K. Y. Lee, Status of graduate software engineering education, Proceedings of the ACM '81 conference, p.179-183, January 1981
Shang-Cheng Chyou, Structure charts and program correctness proofs, Proceedings of the 7th international conference on Software engineering, p.486-498, March 26-29, 1984, Orlando, Florida, United States
David Harel, Recursion in logics of programs, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.81-92, January 29-31, 1979, San Antonio, Texas
Kung-Kiu Lau , Vicky J. Bush , Pete J. Jinks, Towards an introductory formal programming course, ACM SIGCSE Bulletin, v.26 n.1, p.121-125, March 1994
M. Burrows , M. Abadi , R. Needham, A logic of authentication, ACM SIGOPS Operating Systems Review, v.23 n.5, p.1-13, Dec. 3–6, 1989
Jürgen F. H. Winkler, A safe variant of the unsafe integer arithmetic of JavaTM, Software—Practice & Experience, v.32 n.7, p.669-701, June 2002
Susan L. Graham , Mark Wegman, A Fast and Usually Linear Algorithm for Global Flow Analysis, Journal of the ACM (JACM), v.23 n.1, p.172-202, Jan. 1976
Michael C. McFarland, On proving the correctness of optimizing transformations in a digital design automation system, Proceedings of the 18th conference on Design automation, p.90-97, June 29-July 01, 1981, Nashville, Tennessee, United States
Richard P. Reitman, A mechanism for information control in parallel systems, Proceedings of the seventh ACM symposium on Operating systems principles, p.55-63, December 10-12, 1979, Pacific Grove, California, United States
Robert Paige, Transformational programming: applications to algorithms and systems, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.73-87, January 24-26, 1983, Austin, Texas
Bengt Nordström, An outline of a mathematical model for the definition and manipulation of data, ACM SIGMOD Record, v.8 n.2, p.1-11, March 1976
Andreas Blass , Yuri Gurevich, Inadequacy of computable loop invariants, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.1-11, Jan. 2001
Robert Paige , Shaye Koenig, Finite Differencing of Computable Expressions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.402-454, July 1982
Werner Damm, An axiomatization of low-level parallelism in microarchitectures, ACM SIGMICRO Newsletter, v.15 n.4, p.314-323, Dec. 1984
Chin Soon Lee , Neil D. Jones , Amir M. Ben-Amram, The size-change principle for program termination, ACM SIGPLAN Notices, v.36 n.3, p.81-92, March 2001
Tim Sheard , David Stemple, Automatic verification of database transaction safety, ACM Transactions on Database Systems (TODS), v.14 n.3, p.322-368, Sept. 1989
Richard D. Schlichting , Fred B. Schneider, Understanding and using asynchronous message passing (Preliminary Version), Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.141-147, August 18-20, 1982, Ottawa, Canada
V. R. Pratt, A practical decision method for propositional dynamic logic (Preliminary Report), Proceedings of the tenth annual ACM symposium on Theory of computing, p.326-337, May 01-03, 1978, San Diego, California, United States
Laura K. Dillon, Verifying General Safety Properties of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.16 n.1, p.51-63, January 1990
Lloyd D. Fosdick, The production of better mathematical software, Communications of the ACM, v.15 n.7, p.611-617, July 1972
Martin Odersky, Defining context-dependent syntax without using contexts, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.3, p.535-562, July 1993
Bengt Jonsson, Compositional specification and verification of distributed systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.2, p.259-303, March 1994
Stuart Shapiro, Splitting the Difference: The Historical Necessity of Synthesis in Software Engineering, IEEE Annals of the History of Computing, v.19 n.1, p.20-54, January 1997
Yves Ledru , Pierre-Yves Schobbens, Applying VDM to large developments, ACM SIGSOFT Software Engineering Notes, v.15 n.4, p.55-58, Sep. 1990
Bart Jacobs , Joachim van den Berg , Marieke Huisman , Martijn van Berkum , U. Hensel , H. Tews, Reasoning about Java classes: preliminary report, ACM SIGPLAN Notices, v.33 n.10, p.329-340, Oct. 1998
Edmund M. Clarke, Proving the correctness of coroutines without history variables, Proceedings of the 16th annual Southeast regional conference, p.160-167, April 13-15, 1978, Atlanta, Georgia
Donald E. Knuth, Structured Programming with go to Statements, ACM Computing Surveys (CSUR), v.6 n.4, p.261-301, Dec. 1974
Bertrand Meyer, Lessons from the design of the Eiffel libraries, Communications of the ACM, v.33 n.9, p.68-88, Sept. 1990
V. R. Pratt, Dynamic algebras and the nature of induction, Proceedings of the twelfth annual ACM symposium on Theory of computing, p.22-28, April 28-30, 1980, Los Angeles, California, United States
David Harel, And/Or Programs: A New Approach to Structured Programming, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.1-17, Jan. 1980
CORPORATE Tech Correspondence, Technical correspondence, Communications of the ACM, v.33 n.5, p.584-586, May 1990
C. A. R. Hoare, Proof of a program: FIND, Communications of the ACM, v.14 n.1, p.39-45, Jan. 1971
Jeannette M. Wing, Writing Larch interface language specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.1, p.1-24, Jan. 1987
J. Craig Cleaveland, Programming languages considered as abstract data types, Proceedings of the ACM 1980 annual conference, p.236-245, January 1980
Peter Henderson, Derived semantics for some programming language constructs, Communications of the ACM, v.15 n.11, p.967-973, Nov. 1972
Niklaus Wirth, On the Composition of Well-Structured Programs, ACM Computing Surveys (CSUR), v.6 n.4, p.247-259, Dec. 1974
Verlynda Dobbs, A comparison of concurrent languages: a class project, ACM SIGCSE Bulletin, v.19 n.1, p.62-66, Feb. 1987
Anne-Marie G. Discepolo, Towards a practical specification language, Proceedings of the ACM '81 conference, p.144-153, January 1981
Tadao Takaoka, Parallel program verification with directed graphs, Proceedings of the 1994 ACM symposium on Applied computing, p.462-466, March 06-08, 1994, Phoenix, Arizona, United States
Ali Mili , Jules Desharnais , Jean Raynomd Gagné, Formal models of stepwise refinements of programs, ACM Computing Surveys (CSUR), v.18 n.3, p.231-276, Sept. 1986
R. B. Kieburtz , J. L. Hennessy, TOMAL-a high-level programming language for microprocessor process control applications, ACM SIGPLAN Notices, v.11 n.4, p.127-134, April 1976
David Ginat, Loop invariants and mathematical games, ACM SIGCSE Bulletin, v.27 n.1, p.263-267, March 1995
I. Greif , A. Meyer, Specifying programming language semantics: a tutorial and critique of a paper by Hoare and Lauer, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.180-189, January 29-31, 1979, San Antonio, Texas
Brent Hailpern , Susan Owicki, Modular verification of concurrent programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.322-336, January 25-27, 1982, Albuquerque, Mexico
J. R. Jefferson Wadkins, Rigorous proofs of program correctness without formal logic, ACM SIGCSE Bulletin, v.27 n.1, p.307-311, March 1995
George Milne , Robin Milner, Concurrent Processes and Their Syntax, Journal of the ACM (JACM), v.26 n.2, p.302-321, April 1979
H. D. Mills , V. R. Basili , J. D. Gannon , R. G. Hamlet, Teaching principles of computer programming, Proceedings of the 15th annual conference on Computer Science, p.336-341, February 1987, St. Louis, Missouri, United States
Paul A. Steckler , Mitchell Wand, Lightweight closure conversion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.1, p.48-86, Jan. 1997
D. Y. Cheng, HDB-a high level debugging, Proceedings of the 1989 ACM/IEEE conference on Supercomputing, p.568-573, November 12-17, 1989, Reno, Nevada, United States
Edmund M. Clarke, Jr. , Steven M. German , Joseph Y. Halpern, Effective Axiomatizations of Hoare Logics, Journal of the ACM (JACM), v.30 n.3, p.612-636, July 1983
Martin Lippert , Cristina Videira Lopes, A study on exception detection and handling using aspect-oriented programming, Proceedings of the 22nd international conference on Software engineering, p.418-427, June 04-11, 2000, Limerick, Ireland
S. K. Basu , J. Misra, Some classes of naturally provable programs, Proceedings of the 2nd international conference on Software engineering, p.400-406, October 13-15, 1976, San Francisco, California, United States
George T. Ligler, A mathematical approach to language design, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.41-53, January 20-22, 1975, Palo Alto, California
Peter J. McCann , Gruia-Catalin Roman, Modeling mobile IP in mobile UNITY, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.2, p.115-146, April 1999
Rob Gerth, Transition logic: How to reason about temporal properties in a compositional way, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.39-50, December 1984
Dexter Kozen, On Hoare logic and Kleene algebra with tests, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.60-76, July 2000
Howard Barringer , Ruurd Kuiper , Amir Pnueli, Now you may compose temporal logic specifications, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.51-63, December 1984
David D. Riley, Teaching problem solving in an introductory computer science class, ACM SIGCSE Bulletin, v.13 n.1, p.244-251, February 1981
R. J. R. Back , F. Kurki-Suonio, Distributed cooperation with action systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.4, p.513-554, Oct. 1988
Andy Podgurski, Reliability, sampling, and algorithmic randomness, Proceedings of the symposium on Testing, analysis, and verification, p.11-20, October 08-10, 1991, Victoria, British Columbia, Canada
Peter T. Breuer , Natividad Martínez Madrid, A native process algebra for VHDL, Proceedings of the conference on European design automation, p.420-426, September 18-22, 1995, Brighton, England
Raymond J. Hookway , George W. Ernst, A program verification system, Proceedings of the annual conference, p.504-508, October 20-22, 1976, Houston, Texas, United States
D. E. Perry, Software interconnection models, Proceedings of the 9th international conference on Software Engineering, p.61-69, March 1987, Monterey, California, United States
D. Garlan , S. Jha , D. Notkin , J. Dingel, Reasoning about implicit invocation, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.209-221, Nov. 1998
Jacques Cohen, Computer-assisted microanalysis of programs, Communications of the ACM, v.25 n.10, p.724-733, Oct 1982
Paul Eggert, Toward special-purpose program verification, ACM SIGSOFT Software Engineering Notes, v.15 n.4, p.25-29, Sep. 1990
Jianxin Li, Improvements to systematic program development, Proceedings of the 30th annual Southeast regional conference, April 08-10, 1992, Raleigh, North Carolina
David C. Luckham , Norihisa Suzuki, Verification of Array, Record, and Pointer Operations in Pascal, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.226-244, Oct. 1979
Carl E. Landwehr, Formal Models for Computer Security, ACM Computing Surveys (CSUR), v.13 n.3, p.247-278, Sept. 1981
Allen Goldberg , T. C. Wang , David Zimmerman, Applications of feasible path analysis to program testing, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.80-94, August 17-19, 1994, Seattle, Washington, United States
C David Allen, Derivation of axiomatic definitions of programming languages from algorithmic definitions, ACM SIGACT News
Maureen Harris Cheheyl , Morrie Gasser , George A. Huff , Jonathan K. Millen, Verifying Security, ACM Computing Surveys (CSUR), v.13 n.3, p.279-339, Sept. 1981
Subrata Dasgupta, Some Aspects of High-Level Microprogramming, ACM Computing Surveys (CSUR), v.12 n.3, p.295-323, Sept. 1980
Michael J. Fischer , Richard E. Ladner, Propositional modal logic of programs, Proceedings of the ninth annual ACM symposium on Theory of computing, p.286-294, May 04-04, 1977, Boulder, Colorado, United States
Douglas D. Dunlop , Victor R. Basili, A Comparative Analysis of Functional Correctness, ACM Computing Surveys (CSUR), v.14 n.2, p.229-244, June 1982
Guido Persch , Georg Winterstein, Symbolic interpretation and tracing of PASCAL-programs, Proceedings of the 3rd international conference on Software engineering, p.312-319, May 10-12, 1978, Atlanta, Georgia, United States
Lawrence A. Rowe, Data abstraction from a programming language viewpoint, ACM SIGMOD Record, v.11 n.2, p.29-35, Feb 1981
Robert L. Constable , Scott D. Johnson, A PL/CV precis, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.7-20, January 29-31, 1979, San Antonio, Texas
B. R. Hunt, A comment on axiomatic approaches to programming, Communications of the ACM, v.13 n.7, p.452, July 1970
Ïsmaïlcem Budak Arpinar , Uğur Halici , Sena Arpinar , Asuman Doğaç, Formalization of Workflows and Correctness Issues in the Presence of Concurrency, Distributed and Parallel Databases, v.7 n.2, p.199-248, April 1999
Erik Crank , Matthias Felleisen, Parameter-passing and the lambda calculus, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-244, January 21-23, 1991, Orlando, Florida, United States
Zohar Manna , Richard Waldinger, Is “sometime” sometimes better than “always”?: intermittent assertions in proving program correctness, Communications of the ACM, v.21 n.2, p.159-172, Feb. 1978
B. Szymanski , N. Prywes , E. Lock , A. Pnueli, On the scope of static checking in definitional languages, Proceedings of the 1984 annual conference of the ACM on The fifth generation challenge, p.197-207, January 1984
Douglas D. Dunlop , Victor R. Basili, Generalizing specifications for uniformly implemented loops, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.137-158, Jan. 1985
D. Perry, The logic of propagation in the inscape environment, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.114-121, Dec. 1989
John C. Reynolds, Reasoning about arrays, Communications of the ACM, v.22 n.5, p.290-299, May 1979
Gregory R. Andrews, Parallel programs: proofs, principles, and practice, Communications of the ACM, v.24 n.3, p.140-145, March 1981
Zohar Manna , Jean Vuillemin, Fixpoint approach to the theory of computation, Communications of the ACM, v.15 n.7, p.528-536, July 1972
D. E. Perry, Version control in the Inscape environment, Proceedings of the 9th international conference on Software Engineering, p.142-149, March 1987, Monterey, California, United States
G. E. Kaiser , P. H. Feiler, An architecture for intelligent assistance in software development, Proceedings of the 9th international conference on Software Engineering, p.180-188, March 1987, Monterey, California, United States
Peter Henderson, Modern introductory computer science, ACM SIGCSE Bulletin, v.19 n.1, p.183-190, Feb. 1987
Huai-An Lin , Ming T. Liu , Charles J. Graff, Verification of a methodology for designing reliable communication protocols, ACM SIGCOMM Computer Communication Review, v.13 n.4, p.141-149, October 1983
Fred Appleyard , Roger Hui, Design: a financial modelling system, ACM SIGAPL APL Quote Quad, v.15 n.4, p.156-165, May 12, 1985
Axel van Lamsweerde, Formal specification: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.147-159, June 04-11, 2000, Limerick, Ireland
Tomasz Kowaltowski, Data Structures and Correctness of Programs, Journal of the ACM (JACM), v.26 n.2, p.283-301, April 1979
Robert Cartwright , Robert Hood , Philip Matthews, Paths: an abstract alternative to pointers, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-27, January 26-28, 1981, Williamsburg, Virginia
Maurice P. Herlihy , Jeannette M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.463-492, July 1990
Robert S. Boyer , Yuan Yu, Automated proofs of object code for a widely used microprocessor, Journal of the ACM (JACM), v.43 n.1, p.166-192, Jan. 1996
L. G. Williams, Software process modeling: a behavioral approach, Proceedings of the 10th international conference on Software engineering, p.174-186, April 11-15, 1988, Singapore
John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States
W. D. Maurer, Some correctness principles for machine language programs and microprograms, Conference record of the 7th annual workshop on Microprogramming, p.225-234, September 30-October 02, 1974, Pal Alto, California, United States
Robert L. Constable, On the theory of programming logics, Proceedings of the ninth annual ACM symposium on Theory of computing, p.269-285, May 04-04, 1977, Boulder, Colorado, United States
Harlan D. Mills, The new math of computer programming, Communications of the ACM, v.18 n.1, p.43-48, Jan. 1975
Derek C. Oppen , Stephen A. Cook, Proving assertions about programs that manipulate data structures, Proceedings of seventh annual ACM symposium on Theory of computing, p.107-116, May 05-07, 1975, Albuquerque, New Mexico, United States
Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994
Paresh B. Shah , James C. Pleasant, Formal program verification and computability theory, Proceedings of the 30th annual Southeast regional conference, April 08-10, 1992, Raleigh, North Carolina
Krithivasan Ramamritham , Robert M. Keller, Specifying and proving properties of sentinel processes, Proceedings of the 5th international conference on Software engineering, p.374-382, March 09-12, 1981, San Diego, California, United States
Ashvin Radiya , Robert G. Sargent, A new formalism for discrete event simulation, Proceedings of the 19th conference on Winter simulation, p.554-558, December 14-16, 1987, Atlanta, Georgia, United States
Thomas Reps , Bowen Alpern, Interactive proof checking, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.36-45, January 15-18, 1984, Salt Lake City, Utah, United States
Richard D. Schlichting , Fred B. Schneider, Using message passing for distributed programming: proof rules and disciplines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.3, p.402-431, July 1984
Nobuyuki Nezu , Huizhu Lu, Modeling deflection networks: design and specification, Proceedings of the 1999 ACM symposium on Applied computing, p.66-73, February 28-March 02, 1999, San Antonio, Texas, United States
Robert Cartwright , John McCarthy, First order programming logic, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.68-80, January 29-31, 1979, San Antonio, Texas
Leslie Lamport, win and sin: predicate transformers for concurrency, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.396-428, July 1990
Shaula Yemini , Daniel M. Berry, An axiomatic treatment of exception handling in an expression-oriented language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.3, p.390-407, July 1987
Sten Andler, Predicate path expressions, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.226-236, January 29-31, 1979, San Antonio, Texas
Pradip Bose , B. R. Rau , M. S. Schlansker, Systematically derived instruction sets for high-level language support, Proceedings of the 20th annual Southeast regional conference, p.73-84, April 01-03, 1982, Knoxville, Tennessee
John H. Howard, Signaling in monitors, Proceedings of the 2nd international conference on Software engineering, p.47-52, October 13-15, 1976, San Francisco, California, United States
Ralph L. London, The current state of proving programs correct, Proceedings of the ACM annual conference, p.39-46, August 01-01, 1972, Boston, Massachusetts, United States
James,H. Fetzer, Program verification: the very idea, Communications of the ACM, v.31 n.9, p.1048-1063, Sept. 1988
P. Jain , S. S. Lam, Specification and verification of collusion-free broadcast networks, ACM SIGCOMM Computer Communication Review, v.18 n.4, p.282-291, August 1988
Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972
Vijay Pitchumani , Edward P. Stabler, A formal method for computer design verification, Proceedings of the 19th conference on Design automation, p.809-814, January 1982
Susan Owicki, A consistent and complete deductive system for the verification of parallel programs, Proceedings of the eighth annual ACM symposium on Theory of computing, p.73-86, May 03-05, 1976, Hershey, Pennsylvania, United States
Patrick Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, v.277 n.1-2, p.47-103, April 28, 2002
Roberto Giacobazzi , Isabella Mastroeni, A characterization of symmetric semantics by domain complementation, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.115-126, September 20-23, 2000, Montreal, Quebec, Canada
George W. Ernst , William F. Ogden, Specification of Abstract Data Types in Modula, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.4, p.522-543, Oct. 1980
Krithivasan Ramamritham, Resource controller tasks in ADA: Their structure and semantics, Proceedings of the 7th international conference on Software engineering, p.67-76, March 26-29, 1984, Orlando, Florida, United States
Stephen L. Bloom , Zoltán Ésik, Floyd-Hoare logic in iteration theories, Journal of the ACM (JACM), v.38 n.4, p.887-934, Oct. 1991
David Goldberg, The design of floating-point data types, ACM Letters on Programming Languages and Systems (LOPLAS), v.1 n.2, p.138-151, June 1992
Ali Mili , Jules Desharnais, A system for classifying program verification methods: Assigning meanings to program verification methods, Proceedings of the 7th international conference on Software engineering, p.499-509, March 26-29, 1984, Orlando, Florida, United States
Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975
Hans-Juergen Boehm, Side effects and aliasing can have simple axiomatic descriptions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.4, p.637-655, Oct. 1985
J. Arsac , Y. Kodratoff, Some Techniques for Recursion Removal from Recursive Functions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.295-322, April 1982
D. Whitfield , M. L. Soffa, An approach to ordering optimizing transformations, ACM SIGPLAN Notices, v.25 n.3, p.137-146, Mar. 1990
K. A. Redish, Comment on London's certification of algorithms 245, Communications of the ACM, v.14 n.1, p.50-51, Jan. 1971
K. Kishida , T. Katayama , M. Matsuo , I. Miyamoto , K. Ochimizu , Nobuo Saito , Johner H. Sayler , K. Torii , L. G. Williams, SDA: A novel approach to software environment design and construction, Proceedings of the 10th international conference on Software engineering, p.69-79, April 11-15, 1988, Singapore
James C. Pleasant, Systematic program development/proof using Dromey's method: some comparisons with top-down design, Proceedings of the 19th annual conference on Computer Science, p.169-173, April 1991, San Antonio, Texas, United States
Mitchell Wand, A new incompleteness result for Hoare's system, Proceedings of the eighth annual ACM symposium on Theory of computing, p.87-91, May 03-05, 1976, Hershey, Pennsylvania, United States
Yongmei Liu, A hoare-style proof system for robot programs, Eighteenth national conference on Artificial intelligence, p.74-79, July 28-August 01, 2002, Edmonton, Alberta, Canada
R. B. Terwilliger , R. H. Campbell, An early report on encompass, Proceedings of the 10th international conference on Software engineering, p.344-354, April 11-15, 1988, Singapore
Dewayne E. Perry, The inscape environment, Proceedings of the 11th international conference on Software engineering, p.2-11, May 1989, Pittsburgh, Pennsylvania, United States
Russell J. Abbott, Program design by informal English descriptions, Communications of the ACM, v.26 n.11, p.882-894, Nov. 1983
Frank D. Anger, On Lamport's interprocessor communication model, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.3, p.404-417, July 1989
N Liu , M T Liu, Conformity analysis for communication protocols, ACM SIGCOMM Computer Communication Review, v.16 n.3, p.216-226, Aug. 5, 1986
Zohar Manna , Richard Waldinger, The synthesis of structure-changing programs, Proceedings of the 3rd international conference on Software engineering, p.175-187, May 10-12, 1978, Atlanta, Georgia, United States
Zhichen Xu , Barton P. Miller , Thomas Reps, Safety checking of machine code, ACM SIGPLAN Notices, v.35 n.5, p.70-82, May 2000
Terrence W. Pratt , George D. Maydwell, Experience with the formal semantic definition of HAL/S, ACM SIGPLAN Notices, v.17 n.6, p.327-333, June 1982
Wolfgang Polak, Program verification based on denotation semantics, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-158, January 26-28, 1981, Williamsburg, Virginia
Norihisa Suzuki, Verifying programs by algebraic and logical reduction, ACM SIGPLAN Notices, v.10 n.6, p.473-481, June 1975
Gerald J. Popek , David A. Farber, A model for verification of data security in operating systems, Communications of the ACM, v.21 n.9, p.737-749, Sept. 1978
Bengt Jonsson, Modular verification of asynchronous networks, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.152-166, August 10-12, 1987, Vancouver, British Columbia, Canada
David Gries, Is Sometimes Ever Better Than Always?, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.258-265, Oct. 1979
Eric C. R. Hehner, Predicative programming Part I, Communications of the ACM, v.27 n.2, p.134-143, Feb. 1984
Susan L. Gerhart , Richard J. Orgass, A proposal for a handbook for APL program verification, ACM SIGAPL APL Quote Quad, v.5 n.4, Winter 1974
Paul C. Attie , E. Allen Emerson, Synthesis of concurrent programs for an atomic read/write model of computation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.2, p.187-242, March 2001
Divyakant Agrawal , Amr El Abbadi , Ambuj K. Singh, Consistency and orderability: semantics-based correctness criteria for databases, ACM Transactions on Database Systems (TODS), v.18 n.3, p.460-486, Sept. 1993
Edmund Melson Clarke, Jr., Programming language constructs for which it is impossible to obtain good hoare-like axiom systems, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.10-20, January 17-19, 1977, Los Angeles, California
J. Craig Cleaveland, Mathematical specifications, ACM SIGPLAN Notices, v.15 n.12, p.31-42, December 1980
C. A. R. Hoare, Proof of correctness of data representations, Software pioneers: contributions to software engineering, Springer-Verlag New York, Inc., New York, NY, 2002
C. A. R. Hoare, Proof of correctness of data representations, Software pioneers: contributions to software engineering, Springer-Verlag New York, Inc., New York, NY, 2002
Johann Blieberger, Data-Flow Frameworks for Worst-Case Execution Time Analysis, Real-Time Systems, v.22 n.3, p.183-227, May 2002
Joseph V. Giordano, Some verification problems in Pascal-like languages, ACM SIGSOFT Software Engineering Notes, v.5 n.1, p.18-27, January 1980
Bernd Krieg Brückner , David C. Luckham, ANNA: Towards a language for annotating Ada programs, Proceedings of the ACM-SIGPLAN symposium on The ADA programming language, p.128-138, January 1980
M. M. Lehman , J. F. Ramil, Evolution in software and related areas, Proceedings of the 4th International Workshop on Principles of Software Evolution, September 10-11, 2001, Vienna, Austria
K. Rustan M. Leino, Recursive object types in a logic of object-oriented programs, Nordic Journal of Computing, v.5 n.4, p.330-360, Winter 1998
David Stemple , Tim Sheard, Specification and verification of abstract database types, Proceedings of the 3rd ACM SIGACT-SIGMOD symposium on Principles of database systems, April 02-04, 1984, Waterloo, Ontario, Canada
Gail E. Kaiser , Peter H. Feiler , Steven S. Popovich, Intelligent Assistance for Software Development and Maintenance, IEEE Software, v.5 n.3, p.40-49, May 1988
R. Geoff Dromey, Software Quality—Prevention versus Cure?, Software Quality Control, v.11 n.3, p.197-210, July 2003
David C. Luckham, A brief account: Implementation and applications of a Pascal program verifier (Position Statement), Proceedings of the 1978 annual conference, p.786-792, January 1978
C. A. R. Hoare, Assertions: a personal perspective, Software pioneers: contributions to software engineering, Springer-Verlag New York, Inc., New York, NY, 2002
Barbara G. Ryder , Mary Lou Soffa, Influences on the design of exception handling: ACM SIGSOFT project on the impact of software engineering research on programming language design, ACM SIGPLAN Notices, v.38 n.6, June 2003
J.-J. Ch. Meyer, Dynamic logic for reasoning about actions and agents, Logic-based artificial intelligence, Kluwer Academic Publishers, Norwell, MA, 2000
Natarajan Shankar, Automated verification using deduction, exploration, and abstraction, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
Shaula Yemini, An axiomatic treatment of exception handling, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.281-288, January 25-27, 1982, Albuquerque, Mexico
John V. Guttag, Abstract data types, then and now, Software pioneers: contributions to software engineering, Springer-Verlag New York, Inc., New York, NY, 2002
Wolfgang A. Halang , Bernd J. Krämer, Safety Assurance in Process Control, IEEE Software, v.11 n.1, p.61-67, January 1994
Olivier Lecarme, Structured programming, programming teaching and the language Pascal, ACM SIGPLAN Notices, v.9 n.7, p.15-21, July 1974
Barbara G. Ryder , Mary Lou Soffa, Influences on the design of exception handling ACM SIGSOFT project on the impact of software engineering research on programming language design, ACM SIGSOFT Software Engineering Notes, v.28 n.4, July 2003
William D. Young , Donald I. Good, Generics and verification in Ada, ACM SIGPLAN Notices, v.15 n.11, November 1980
Vaughan R. Pratt, The competence/performance dichotomy in programming preliminary report, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-200, January 17-19, 1977, Los Angeles, California
Ted Venema , Jim des Rivieres, Euclid and PASCAL, ACM SIGPLAN Notices, v.13 n.3, p.57-69, March 1978
Fubo Zhang , Erik H. D'Hollander, Using Hammock Graphs to Structure Programs, IEEE Transactions on Software Engineering, v.30 n.4, p.231-245, April 2004
Nancy Durgin , John Mitchell , Dusko Pavlovic, A compositional logic for proving security properties of protocols, Journal of Computer Security, v.11 n.4, p.677-721, 01/01/2004
Timothy S. Gegg-Harrison , Gary R. Bunce , Rebecca D. Ganetzky , Christina M. Olson , Joshua D. Wilson, Studying program correctness by constructing contracts, ACM SIGCSE Bulletin, v.35 n.3, September 2003
Sanjaya Kumar , James H. Aylor , Barry W. Johnson , Wm. A. Wulf, Object-Oriented Techniques in Hardware Design, Computer, v.27 n.6, p.64-70, June 1994
Yifeng Chen, A fixpoint theory for non-monotonic parallelism, Theoretical Computer Science, v.308 n.1-3, p.367-392, 3 November 2003
Nick Benton, Simple relational correctness proofs for static analyses and program transformations, ACM SIGPLAN Notices, v.39 n.1, p.14-25, January 2004
Leslie Lamport, Reasoning about nonatomic operations, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.28-37, January 24-26, 1983, Austin, Texas
Robert Goldblatt, Mathematical modal logic: a view of its evolution, Journal of Applied Logic, v.1 n.5-6, p.309-392, October 2003
Ralph-Johan Back , Viorel Preoteasa, Reasoning about recursive procedures with parameters, Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.1-7, August 26, 2003, Uppsala, Sweden
Yingzhou Zhang , Baowen Xu, A survey of semantic description frameworks for programming languages, ACM SIGPLAN Notices, v.39 n.3, March 2004
Gregory R. Andrews , Richard P. Reitman, An Axiomatic Approach to Information Flow in Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.56-76, Jan. 1980
Chris A. Vissers, Interface, a dispersed architecture, ACM SIGARCH Computer Architecture News, v.4 n.4, p.98-104, January 1976
S. Antoy , J. Gannon, Using Term Rewriting to Verify Software, IEEE Transactions on Software Engineering, v.20 n.4, p.259-274, April 1994
G. W. Ernst , R. J. Hookway , W. F. Ogden, Modular Verification of Data Abstractions with Shared Realizations, IEEE Transactions on Software Engineering, v.20 n.4, p.288-307, April 1994
Zerksis D. Umrigar , Vijay Pitchumani, Formal verification of a real-time hardware design, Proceedings of the 20th conference on Design automation, p.221-227, June 27-29, 1983, Miami Beach, Florida, United States
Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
W. D. Maurer, Proving the correctness of a flight-director program for an airborne minicomputer, ACM SIGPLAN Notices, v.11 n.4, p.103-108, April 1976
W. Damm, A Microprogramming Logic, IEEE Transactions on Software Engineering, v.14 n.5, p.559-574, May 1988
F. L. Bauer, Programming as an evolutionary process, Proceedings of the 2nd international conference on Software engineering, p.223-234, October 13-15, 1976, San Francisco, California, United States
Raymond T. Yeh, An approach to program verification, Proceedings of the 13th conference on Design automation, p.295-300, June 28-30, 1976, San Francisco, California, United States
Mark T. Vandevoorde , John V. Guttag, Using specialized procedures and specification-based analysis to reduce the runtime costs of modularity, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.121-127, Dec. 1994
Laurian M. Chirica , David F. Martin, Toward compiler implementation correctness proofs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.185-214, April 1986
Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001
Richard D. Schlichting , Fred B. Schneider, Fail-stop processors: an approach to designing fault-tolerant computing systems, ACM Transactions on Computer Systems (TOCS), v.1 n.3, p.222-238, August 1983
Edmund Melson Clarke, Jr., Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems, Journal of the ACM (JACM), v.26 n.1, p.129-147, Jan. 1979
M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona
Paul C. Attie , E. Allen Emerson, Synthesis of concurrent systems with many similar processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.51-115, Jan. 1998
David Harel , Amir Puneli , Jonathan Stavi, A complete axiomatic system for proving deductions about recursive programs, Proceedings of the ninth annual ACM symposium on Theory of computing, p.249-260, May 04-04, 1977, Boulder, Colorado, United States
Joseph L. Bates , Robert L. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.113-136, Jan. 1985
Robert L. Constable , James E. Donahue, A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.1, p.98-114, July 1979
D. Harel , A. R. Meyer , V. R. Pratt, Computability and completeness in logics of programs (Preliminary Report), Proceedings of the ninth annual ACM symposium on Theory of computing, p.261-268, May 04-04, 1977, Boulder, Colorado, United States
Arthur Bernstein , Paul K. Harter, Jr., Proving real-time properties of programs with temporal logic, ACM SIGOPS Operating Systems Review, v.15 n.5, p.1-11, December 1981
Leslie Lamport, Control predicates are better than dummy variables for reasoning about program control, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.267-281, April 1988
David Gries, An exercise in proving parallel programs correct, Communications of the ACM, v.20 n.12, p.921-930, Dec. 1977
Tal Lev-Ami , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Putting static analysis to work for verification: A case study, ACM SIGSOFT Software Engineering Notes, v.25 n.5, p.26-38, Sept. 2000
David Arnow, Teaching programming to liberal arts students: using loop invariants, ACM SIGCSE Bulletin, v.26 n.1, p.141-144, March 1994
Mark R. Blackburn, Using Expert Systems to Construct Formal Specifications, IEEE Expert: Intelligent Systems and Their Applications, v.4 n.1, p.62-74, March 1989
Andrés Silva, Dynamic logic a review, AI Magazine, v.23 n.1, p.119-120, March 2002
Robert Cartwright , Derek Oppen, Unrestricted procedure calls in Hoare's logic, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.131-140, January 23-25, 1978, Tucson, Arizona
Timothy Hickey , Jacques Cohen, Automating program analysis, Journal of the ACM (JACM), v.35 n.1, p.185-220, Jan. 1988
Dan Craigen , Susan Gerhart , Ted Ralston, Case Study: Darlington Nuclear Generating Station, IEEE Software, v.11 n.1, p.30-39, 28, January 1994
Grady Early, Functional programming and the two-pass assembler, ACM SIGPLAN Notices, v.17 n.8, p.34-42, August 1982
Roberto Giacobazzi , Isabella Mastroeni, Non-Standard Semantics for Program Slicing, Higher-Order and Symbolic Computation, v.16 n.4, p.297-339, December 2003
Anne Dinning, A Survey of Synchronization Methods for Parallel Computers, Computer, v.22 n.7, p.66-77, July 1989
Salwa K. Abd-El-Hafiz , Victor R. Basili, A Knowledge-Based Approach to the Analysis of Loops, IEEE Transactions on Software Engineering, v.22 n.5, p.339-360, May 1996
Chris Fox , Sebastian Danicic , Mark Harman , Robert M. Hierons, CONSIT: a fully automated conditioned program slicer, Software—Practice & Experience, v.34 n.1, p.15-46, January 2004
Changqing Wang , David R. Musser, Dynamic Verification of C++ Generic Algorithms, IEEE Transactions on Software Engineering, v.23 n.5, p.314-323, May 1997
Leonard H. Weiner, The roots of structured programming, ACM SIGCSE Bulletin, v.10 n.1, February 1978
Christopher Westphal, Knowledge engineering for software design, ACM SIGSOFT Software Engineering Notes, v.13 n.1, p.57-58, Jan. 1988
Donald MacKenzie, The Automation of Proof: A Historical and Sociological Exploration, IEEE Annals of the History of Computing, v.17 n.3, p.7-29, September 1995
M. G. Staskauskas, The Formal Specification and Design of a Distributed Electronic Funds-Transfer System, IEEE Transactions on Computers, v.37 n.12, p.1515-1528, December 1988
Pradeep Jain , Simon S. Lam, Specification of Real-Time Broadcast Networks, IEEE Transactions on Computers, v.40 n.4, p.404-422, April 1991
Ying Liu , Ambuj K. Singh , Rajive L. Bagrodia, A Decompositional Approach to the Design of Parallel Programs, IEEE Transactions on Software Engineering, v.20 n.12, p.914-932, December 1994
Marvin V. Zelkowitz, A Functional Correctness Model of Program Verification, Computer, v.23 n.11, p.30-39, November 1990
Dachuan Yu , Nadeem A. Hamid , Zhong Shao, Building certified libraries for PCC: dynamic storage allocation, Science of Computer Programming, v.50 n.1-3, p.101-127, March 2004
IEEE Expert staff, Design Theory and Computer Science, IEEE Expert: Intelligent Systems and Their Applications, v.7 n.1, p.88-89, February 1992
Virginia Niculescu, On Data Distributions in the Construction of Parallel Programs, The Journal of Supercomputing, v.29 n.1, p.5-25, July 2004
Bernd Krieg-Brückner, Consistency checking in Ada and Anna: a transformational approach, ACM SIGAda Ada Letters, v.III n.2, p.46-54, September/October 1983
Martin Ward, Derivation of Data Intensive Algorithms by Formal Transformation: The Schnorr-Waite Graph Marking Algorithm, IEEE Transactions on Software Engineering, v.22 n.9, p.665-686, September 1996
John D. Gannon, Language and compiler design to enhance reliability, ACM SIGPLAN Notices, v.8 n.6, June 1973
Piotr Dembinski , Richard Schwartz, The taming of the pointer, ACM SIGPLAN Notices, v.12 n.7, p.60-74, July 1977
Kohei Honda , Nobuko Yoshida, A compositional logic for polymorphic higher-order functions, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.191-202, August 24-26, 2004, Verona, Italy
Sriram Sankaranarayanan , Henny B. Sipma , Zohar Manna, Non-linear loop invariant generation using Gröbner bases, ACM SIGPLAN Notices, v.39 n.1, p.318-329, January 2004
W. P. de Roever, Operational and mathematical semantics for recursive polyadic program schemata, ACM SIGPLAN Notices, v.8 n.6, June 1973
John K. Dixon , John McLean , David L. Parnas, Rapid prototyping by means of abstract module specifications written as trace axioms, ACM SIGSOFT Software Engineering Notes, v.7 n.5, p.45-49, December 1982
Michael Burrows , Martín Abadi , Roger Needham, Authentication: a practical study in belief and action, Proceedings of the 2nd conference on Theoretical aspects of reasoning about knowledge, March 07-09, 1988, Pacific Grove, California
Karel Culik, Theory of computation on abstract/concrete computer automata, ACM SIGACT News, v.14 n.1, p.21-35, Winter 1982
S. Chaki , E. Clarke , A. Groce , J. Ouaknine , O. Strichman , K. Yorav, Efficient Verification of Sequential and Concurrent C Programs, Formal Methods in System Design, v.25 n.2-3, p.129-166, September-November 2004
Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, ACM SIGPLAN Notices, v.39 n.9, September 2004
Peter J. McCann , Gruia-Catalin Roman, Compositional Programming Abstractions for Mobile Computing, IEEE Transactions on Software Engineering, v.24 n.2, p.97-110, February 1998
Richard E. Ladner , John H. Reif, The logic of distributed protocols: preliminary report, Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, March 19-22, 1986, Monterey, California
Beth Levy, Microcode verification using SDVS-the method and a case study, ACM SIGMICRO Newsletter, v.15 n.4, p.234-245, Dec. 1984
Anne Fitzpatrick , Mary Croarken, Events and Sightings, IEEE Annals of the History of Computing, v.23 n.2, p.68-73, April 2001
Robert van Engelen , David Whalley , Xin Yuan, Automatic validation of code-improving transformations on low-level program representations, Science of Computer Programming, v.52 n.1-3, p.257-280, August 2004
Daniel Powell, Automatic derivation of loop termination conditions to support verification, Proceedings of the 27th Australasian conference on Computer science, p.89-97, January 01, 2004, Dunedin, New Zealand
Dines Bjørner , Jorge R. Cuéllar, Software engineering education: Rôles of formal specification and design calculi, Annals of Software Engineering, v.6 n.1-4, p.365-409, April 1999
Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004
Karel Culik, An advanced programming language definition and domain correctness of programs, ACM SIGPLAN Notices, v.17 n.8, p.57-66, August 1982
John Backus, The History of Fortran I, II, and III, IEEE Annals of the History of Computing, v.20 n.4, p.68-78, October 1998
Edsger W. Dijkstra, Guarded commands, non-determinacy and a calculus for the derivation of programs, ACM SIGPLAN Notices, v.10 n.6, p.2-2.13, June 1975
J. Hagelstein, Proving properties of shared data structures application to functional programming, Proceedings of the ACM '82 conference, p.142-148, January 1982
Brandon Morel , Perry Alexander, SPARTACAS Automating Component Reuse and Adaptation, IEEE Transactions on Software Engineering, v.30 n.9, p.587-600, September 2004
D. M. Goldschlag, Mechanically Verifying Concurrent Programs with the Boyer-Moore Prove, IEEE Transactions on Software Engineering, v.16 n.9, p.1005-1023, September 1990
Eric C. R. Hehner, Structuring, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.201-205, January 17-19, 1977, Los Angeles, California
Bernd Krieg-Brückner , David C. Luckham, ANNA: towards a language for annotating Ada programs, ACM SIGPLAN Notices, v.15 n.11, November 1980
V. Donzeau-Gouge , G. Kahn , B. Lang , B. Mélèse, Document structure and modularity in mentor, ACM SIGPLAN Notices, v.19 n.5, p.141-148, May 1984
John Backus, The history of FORTRAN I, II, and III, ACM SIGPLAN Notices, v.13 n.8, p.165-180, August 1978
Frederick J. Drasch , Richard A. Bowen, IDBUG: A tool for program development, ACM SIGSOFT Software Engineering Notes, v.3 n.5, p.106-110, November 1978
V. R. Pratt, On specifying verifiers, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-116, January 28-30, 1980, Las Vegas, Nevada
Ziyang Duan , Arthur Bernstein , Philip Lewis , Shiyong Lu, A model for abstract process specification, verification and composition, Proceedings of the 2nd international conference on Service oriented computing, November 15-19, 2004, New York, NY, USA
William D. Young , Donald I. Good, Generics and verification in Ada, Proceedings of the ACM-SIGPLAN symposium on The ADA programming language, p.123-127, January 1980
Chia-Chu Chiang, Teaching a formal method in a software engineering course, Proceedings of the 2nd annual conference on Mid-south college computing, p.39-52, April 02-03, 2004, Little Rock, Arkansas
Daniel Le Métayer , Valérie-Anne Nicolas , Olivier Ridoux, Exploring the Software Development Trilogy, IEEE Software, v.15 n.6, p.75-81, November 1998
Matthias Blume , David McAllester, A sound (and complete) model of contracts, ACM SIGPLAN Notices, v.39 n.9, September 2004
Allan M. Stavely, Verifying Definite Iteration Over Data Structures, IEEE Transactions on Software Engineering, v.21 n.6, p.506-514, June 1995
Riccardo Pucella, The finite and the infinite in temporal logic, ACM SIGACT News, v.36 n.1, March 2005
Lars Birkedal , Noah Torp-Smith , John C. Reynolds, Local reasoning about a copying garbage collector, ACM SIGPLAN Notices, v.39 n.1, p.220-231, January 2004
Kostas Kontogiannis, Toward program representation and program understanding using process algebras, Proceedings of the 1992 conference of the Centre for Advanced Studies on Collaborative research, November 09-12, 1992, Toronto, Ontario, Canada
Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004
Susan L. Gerhart, Correctness-preserving program transformations, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.54-66, January 20-22, 1975, Palo Alto, California
Barry K. Rosen, Applications of high level control flow, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-47, January 17-19, 1977, Los Angeles, California
Barbara Liskov , Stephen Zilles, Specification techniques for data abstractions, ACM SIGPLAN Notices, v.10 n.6, p.72-87, June 1975
A. Mahmood , E. J. McCluskey, Concurrent Error Detection Using Watchdog Processors-A Survey, IEEE Transactions on Computers, v.37 n.2, p.160-174, February 1988
David Beech, On the definitional method of standard PL/I, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.87-94, October 01-03, 1973, Boston, Massachusetts
Hans-J. Boehm, A logic for expressions with side-effects, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 25-27, 1982, Albuquerque, Mexico
Donald MacKenzie, A view from the Sonnenbichl: on the historical sociology of software and system dependability, Proceedings of the international conference on History of computing: software issues, p.97-122, April 05-07, 2000, Paderborn, Germany
Donald MacKenzie, A view from the Sonnenbichl: on the historical sociology of software and system dependability, Proceedings of the international conference on History of computing: software issues, p.97-122, April 05-07, 2000, Paderborn, Germany
T. Camp , P. Kearns , M. Ahuja, Proof Rules for Flush Channels, IEEE Transactions on Software Engineering, v.19 n.4, p.366-378, April 1993
Cliff B. Jones, The Early Search for Tractable Ways of Reasoning about Programs, IEEE Annals of the History of Computing, v.25 n.2, p.26-49, April 2003
Jozef Hooman , Onno van Roosmalen, Formal design of real-time systems in a platform-independent way, Engineering of distributed control systems, Nova Science Publishers, Inc., Commack, NY, 2001
Alva L. Couch, An Expectant Chat About Script Maturity, Proceedings of the 14th USENIX conference on System administration, December 03-08, 2000, New Orleans, Louisiana
Jan Peleska, Design and verification of fault tolerant systems with CSP, Distributed Computing, v.5 n.2, p.95-106, September 1991
Sigurd Meldal, A complete axiomatic semantics of spawning, Distributed Computing, v.5 n.3, p.159-174, December 1991
Étienne Lozes, Elimination of spatial connectives in static spatial logics, Theoretical Computer Science, v.330 n.3, p.475-499, 9 February 2005
Michael Lutz, Ontology-based service discovery in spatial data infrastructures, Proceedings of the 2005 workshop on Geographic information retrieval, November 04-04, 2005, Bremen, Germany
Mike Adler , Michael A. Gray, A formalization of Myers cause-effect graphs for unit testing, ACM SIGSOFT Software Engineering Notes, v.8 n.5, p.24-32, October 1983
Paolo Bientinesi , John A. Gunnels , Margaret E. Myers , Enrique S. Quintana-Ortí , Robert A. van de Geijn, The science of deriving dense linear algebra algorithms, ACM Transactions on Mathematical Software (TOMS), v.31 n.1, p.1-26, March 2005
Zhaozhong Ni , Zhong Shao, Certified assembly programming with embedded code pointers, ACM SIGPLAN Notices, v.41 n.1, p.320-333, January 2006
Jeannette M. Wing , Mark R. Nixon, Extending Ina Jo with Temporal Logic, IEEE Transactions on Software Engineering, v.15 n.2, p.181-197, February 1989
Michelle Mills Strout , Larry Carter , Jeanne Ferrante , Barbara Kreaseck, Sparse Tiling for Stationary Iterative Methods, International Journal of High Performance Computing Applications, v.18 n.1, p.95-113, February 2004
Dick Hamlet, Invariants and state in testing and formal methods, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
Conrad Mueller, Axiomatic computational model, ACM SIGPLAN Notices, v.40 n.3, p.29-39, March 2005
Martin Berger , Kohei Honda , Nobuko Yoshida, A logical analysis of aliasing in imperative higher-order functions, ACM SIGPLAN Notices, v.40 n.9, September 2005
Roberto Giacobazzi , Isabella Mastroeni, Transforming semantics by abstract interpretation, Theoretical Computer Science, v.337 n.1-3, p.1-50, 9 June 2005
J. C. M. Baeten, A brief history of process algebra, Theoretical Computer Science, v.335 n.2-3, p.131-146, 23 May 2005
Gudmund Grov, Verifying the correctness of hume programs: an approach combining deductive and algorithmic reasoning, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
George E. Collins , Rüdiger G. K. Loos, The Jacobi symbol algorithm, ACM SIGSAM Bulletin, v.16 n.1, p.12-16, February 1982
Olivier Ponsini , Carine Fédèle , Emmanuel Kounalis, Rewriting of imperative programs into logical equations, Science of Computer Programming, v.56 n.3, p.363-401, May/June 2005
Barbara G. Ryder , Mary Lou Soffa , Margaret Burnett, The impact of software engineering research on modern progamming languages, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.4, p.431-477, October 2005
Raymond J. Hookway, Verifying Ada programs, ACM SIGSOFT Software Engineering Notes, v.10 n.4, August 1985
D. R. Morrison, On the language of information science, ACM SIGIR Forum, v.10 n.1, p.21-32, Summer 1975
Gruia-Catalin Roman , Jamie Payton, A principled exploration of coordination models, Theoretical Computer Science, v.336 n.2-3, p.367-401, 26 May 2005
Roland Backhouse, Galois connections and fixed point calculus, Algebraic and coalgebraic methods in the mathematics of program construction, Springer-Verlag New York, Inc., New York, NY, 2002
Robert N. Britcher, Using Inspections to Investigate Program Correctness, Computer, v.21 n.11, p.38-44, November 1988
Xuan Li , Lunjin Lu, Inverting abstract unification for set-sharing, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.129-138, July 11-13, 2005, Lisbon, Portugal
Alan Wagner , Subrata Dasgupta, Axiomatic proof rules for a machine-specific microprogramming language, ACM SIGMICRO Newsletter, v.14 n.4, December 1983
Klaus-Dieter Schewe , Bernhard Thalheim, Conceptual modelling of web information systems, Data & Knowledge Engineering, v.54 n.2, p.147-188, August 2005
David Lorge Parnas , Jan Madey , Michal Iglewski, Precise Documentation of Well-Structured Programs, IEEE Transactions on Software Engineering, v.20 n.12, p.948-976, December 1994
Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990
David C. Luckham , Wolfgang Polak, A practical method of documenting and verifying Ada programs with packages, ACM SIGPLAN Notices, v.15 n.11, November 1980
M. Moriconi , T. C. Winkler, Approximate Reasoning About the Semantic Effects of Program Changes, IEEE Transactions on Software Engineering, v.16 n.9, p.980-992, September 1990
Roberto Ziller , Klaus Schneider, Combining supervisor synthesis and model checking, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.2, p.331-362, May 2005
Gary T. Leavens , Yoonsik Cheon , Curtis Clifton , Clyde Ruby , David R. Cok, How the design of JML accommodates both runtime assertion checking and formal verification, Science of Computer Programming, v.55 n.1-3, p.185-208, March 2005
Isabelle Dony , Baudouin Le Charlier, A tool for helping teach a programming method, ACM SIGCSE Bulletin, v.38 n.3, September 2006
Harlan D. Mills , Victor R. Basili , John D. Gannon , Richard G. Hamlet, Mathematical Principles for a First Course in Software Engineering, IEEE Transactions on Software Engineering, v.15 n.5, p.550-559, May 1989
Hai Zhou, Deriving a new efficient algorithm for min-period retiming, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
Pierre Wolper, Expressing interesting properties of programs in propositional temporal logic, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.184-193, January 01, 1986, St. Petersburg Beach, Florida
Alan C. Shaw, Communicating Real-Time State Machines, IEEE Transactions on Software Engineering, v.18 n.9, p.805-816, September 1992
Susan L. Graham , Mark Wegman, A fast and usually linear algorithm for global flow analysis, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.22-34, January 20-22, 1975, Palo Alto, California
Ernst-Rüdiger Olderog, A characterization of Hoare's logic for programs with Pascal-like procedures, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.320-329, December 1983
Murat Karaorman , Parker Abercrombie, jContractor: Introducing Design-by-Contract to Java Using Reflective Bytecode Instrumentation, Formal Methods in System Design, v.27 n.3, p.275-312, November 2005
Raymond T. Boute, Calculational semantics: Deriving programming theories from equations by functional predicate calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.747-793, July 2006
Frederick G. Sayward, A correctness criterion for CSP parallel programs, ACM SIGPLAN Notices, v.10 n.9, September 1975
Kohei Honda, From process logic to program logic, ACM SIGPLAN Notices, v.39 n.9, September 2004
Shane Stephens , Gernot Heiser, Fault tolerance and avoidance in biomedical systems, Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC, July 01-01, 2002, Saint-Emilion, France
Christoph Sprenger , Krzysztof Worytkiewicz, A verification methodology for concurrent software with synchronous communication, Formal methods and models for system design: a system level perspective, Kluwer Academic Publishers, Norwell, MA, 2004
Cees Pierik , Frank S. de Boer, A proof outline logic for object-oriented programming, Theoretical Computer Science, v.343 n.3, p.413-442, 17 October 2005
Élodie-Jane Sims, Extending separation logic with fixpoints and postponed substitution, Theoretical Computer Science, v.351 n.2, p.258-275, 21 February 2006
Cong-Cong Xing, Enhancing program verifications by restricting object types, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
Francesco Curatelli , Leonardo Mangeruca, A Method for Computing the Number of Iterations in Data Dependent Loops, Real-Time Systems, v.32 n.1-2, p.73-104, February 2006
Xinyu Feng , Zhong Shao , Alexander Vaynberg , Sen Xiang , Zhaozhong Ni, Modular verification of assembly code with stack-based control abstractions, ACM SIGPLAN Notices, v.41 n.6, June 2006
Lori A. Clarke , David S. Rosenblum, A historical perspective on runtime assertion checking in software development, ACM SIGSOFT Software Engineering Notes, v.31 n.3, May 2006
Laurian M. Chirica , David F. Martin, An approach to compiler correctness, ACM SIGPLAN Notices, v.10 n.6, p.96-103, June 1975
Susan L. Gerhart, Methods for teaching program verification, ACM SIGCSE Bulletin, v.7 n.1, p.172-178, February 1975
V. R. Pratt, Process logic: preliminary report, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.93-100, January 29-31, 1979, San Antonio, Texas
K. Culik, On formal and informal proofs for program correctness, ACM SIGPLAN Notices, v.18 n.1, p.23-28, January 1983
D. Guaspari , C. Marceau , W. Polak, Formal Verification of Ada Programs, IEEE Transactions on Software Engineering, v.16 n.9, p.1058-1075, September 1990
A. C. Shaw, Reasoning About Time in Higher-Level Language Software, IEEE Transactions on Software Engineering, v.15 n.7, p.875-889, July 1989
R. Sherman , A. Pnueli , D. Harel, Is the interesting part of process logic uninteresting?: a translation from PL to PDL, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.347-360, January 25-27, 1982, Albuquerque, Mexico
Gruia-Catalin Roman , Peter J. McCann, A Notation and Logic for Mobile Computing, Formal Methods in System Design, v.20 n.1, p.47-68, January 2002
Ando Saabas , Tarmo Uustalu, Compositional type systems for stack-based low-level languages, Proceedings of the 12th Computing: The Australasian Theroy Symposium, p.27-39, January 16-19, 2006, Hobart, Australia
MARTIN BERGER , KOHEI HONDA , NOBUKO YOSHIDA, A logical analysis of aliasing in imperative higher-order functions, Journal of Functional Programming, v.17 n.4-5, p.473-546, July 2007
I. B. Bourdonov , A. S. Kossatchev , V. V. Kuliamin, Formalization of test experiments, Programming and Computing Software, v.33 n.5, p.239-260, September 2007
Vincenzo De Florio , Chris Blondia, A survey of linguistic structures for application-level fault tolerance, ACM Computing Surveys (CSUR), v.40 n.2, p.1-37, April 2008
Jamieson M. Cobleigh , George S. Avrunin , Lori A. Clarke, Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-52, April 2008
Marvin V. Zelkowitz, Algebra and models (and reality), ACM SIGSOFT Software Engineering Notes, v.19 n.4, p.79-81, Oct. 1994
Arthur Fleck, Prolog as the first programming language, ACM SIGCSE Bulletin, v.39 n.4, December 2007
Jack B. Dennis, Bibliography, Record of the Project MAC conference on concurrent systems and parallel computation, ACM, New York, NY, 1970
Noah Torp-Smith , Lars Birkedal , John C. Reynolds, Local reasoning about a copying garbage collector, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-58, July 2008
V. A. Nepomniaschy, Verification of Finite Iterations over Tuples of Data Structures, Programming and Computing Software, v.28 n.1, p.1-8, January-February 2002
Gary T. Leavens , Albert L. Baker , Clyde Ruby, Preliminary design of JML: a behavioral interface specification language for java, ACM SIGSOFT Software Engineering Notes, v.31 n.3, May 2006
Barry Boehm, A view of 20th and 21st century software engineering, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.4, p.596-619, Oct. 1983
Yoonsik Cheon , Gary T. Leavens, The Larch/Smalltalk interface specification language, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.3, p.221-153, July 1994
Randal E. Bryant, A methodology for hardware verification based on logic simulation, Journal of the ACM (JACM), v.38 n.2, p.299-328, April 1991
Bruce J. Walker , Richard A. Kemmerer , Gerald J. Popek, Specification and verification of the UCLA Unix security kernel, Communications of the ACM, v.23 n.2, p.118-131, Feb. 1980
Uday S. Reddy, Programming with sequences, Proceedings of the 20th annual Southeast regional conference, p.189-198, April 01-03, 1982, Knoxville, Tennessee
Gary T. Leavens , Jean-Raymond Abrial , Don Batory , Michael Butler , Alessandro Coglio , Kathi Fisler , Eric Hehner , Cliff Jones , Dale Miller , Simon Peyton-Jones , Murali Sitaraman , Douglas R. Smith , Aaron Stump, Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
Anupam Datta , Ante Derek , John C. Mitchell , Arnab Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.311-358, April, 2007
Erika Ábrahám , Frank S. de Boer , Willem-Paul de Roever , Martin Steffen, An assertion-based proof system for multithreaded Java, Theoretical Computer Science, v.331 n.2-3, p.251-290, 25 February 2005
Hidetaka Kondoh , Kokichi Futatsugi, To use or not to use the goto statement: programming styles viewed from Hoare logic, Science of Computer Programming, v.60 n.1, p.82-116, March 2006
James J. Hunt , Fridtjof B. Siebert , Peter H. Schmitt , Isabel Tonin, Provably correct loops bounds for realtime Java programs, Proceedings of the 4th international workshop on Java technologies for real-time and embedded systems, October 11-13, 2006, Paris, France
Daniel J. Dougherty , Claudio Gutiérrez, Normal forms for binary relations, Theoretical Computer Science, v.360 n.1, p.228-246, 21 August 2006
Neelakantan R. Krishnaswami, Reasoning about iterators with separation logic, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon
Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Certified In-lined Reference Monitoring on .NET, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
Timothy S. Gegg-Harrison, Constructing contracts: Making discrete mathematics relevant to beginning programmers, Journal on Educational Resources in Computing (JERIC), v.5 n.2, p.3-es, June 2005
Gabriel J. Ferrer, Teaching cleanroom software engineering with object-oriented data abstraction, Journal of Computing Sciences in Colleges, v.21 n.5, p.155-161, May 2006
Cristiano Calcagno , Philippa Gardner , Uri Zarfaty, Local Reasoning about Data Update, Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.133-175, April, 2007
N. Wirth, On the composition of well-structured programs, Classics in software engineering, Yourdon Press, Upper Saddle River, NJ, 1979
John Backus, The history of Fortran I, II, and III, History of programming languages I, ACM Press, New York, NY, 1978
Isar Stubbe, Towards "dynamic domains": Totally continuous cocomplete Q-categories, Theoretical Computer Science, v.373 n.1-2, p.142-160, March, 2007
Chandan Karfa , Dipankar Sarkar , Chittaranjan Mandal , Chris Reade, Hand-in-hand verification of high-level synthesis, Proceedings of the 17th great lakes symposium on Great lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy
Ando Saabas , Tarmo Uustalu, A compositional natural semantics and Hoare logic for low-level languages, Theoretical Computer Science, v.373 n.3, p.273-302, April, 2007
Jean-Christophe Filliâtre, Formal proof of a program: Find, Science of Computer Programming, v.64 n.3, p.332-340, February, 2007
Ken Koster , David Kao, State coverage: a structural test adequacy criterion for behavior checking, The 6th Joint Meeting on European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering: companion papers, September 03-07, 2007, Dubrovnik, Croatia
David Aspinall , Lennart Beringer , Martin Hofmann , Hans-Wolfgang Loidl , Alberto Momigliano, A program logic for resources, Theoretical Computer Science, v.389 n.3, p.411-445, December, 2007
Marcelo F. Frias , Carlos G. Lopez Pombo , Juan P. Galeotti , Nazareno M. Aguirre, Efficient Analysis of DynAlloy Specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.1, p.1-34, December 2007
Helmut K. Berg, Firmware testing and test data selection, Proceedings of the May 4-7, 1981, national computer conference, May 04-07, 1981, Chicago, Illinois
Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Polymorphism and separation in hoare type theory, ACM SIGPLAN Notices, v.41 n.9, September 2006
Gruia-Catalin Roman , Christine Julien , Jamie Payton, Modeling adaptive behaviors in Context UNITY, Theoretical Computer Science, v.376 n.3, p.185-204, May, 2007
Philip A. Bernstein , Barbara T. Blaustein , Edmund M. Clarke, Fast maintenance of semantic integrity assertions using redundant aggregate data, Proceedings of the sixth international conference on Very Large Data Bases, p.126-136, October 01-03, 1980, Montreal, Quebec, Canada
Alexander Borgida , Harry K. T. Wong, Data models and data manipulation languages: complementary semantics and proof theory, Proceedings of the seventh international conference on Very Large Data Bases, p.260-271, September 09-11, 1981, Cannes, France
Shaye Koenig , Robert Paige, A transformational framework for the automatic control of derived data, Proceedings of the seventh international conference on Very Large Data Bases, p.306-318, September 09-11, 1981, Cannes, France
Colette Rolland , S. Leifert , Christian Richard, Tools for information system dynamics management, Proceedings of the fifth international conference on Very Large Data Bases, p.251-261, October 03-05, 1979, Rio de Janeiro, Brazil
Georges Gardarin , Michel A. Melkanoff, Proving consistency of database transactions, Proceedings of the fifth international conference on Very Large Data Bases, p.291-298, October 03-05, 1979, Rio de Janeiro, Brazil
Nicola Bombieri , Franco Fummi , Graziano Pravadelli, Incremental ABV for functional validation of TL-to-RTL design refinement, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
David Monniaux, The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.3, p.1-41, May 2008
David A. Naumann, Observational purity and encapsulation, Theoretical Computer Science, v.376 n.3, p.205-224, May, 2007
R. Chadha , L. Cruz-Filipe , P. Mateus , A. Sernadas, Reasoning about probabilistic sequential programs, Theoretical Computer Science, v.379 n.1-2, p.142-165, June, 2007
Klaus-Dieter Schewe , Bernhard Thalheim, Personalisation of web information systems - A term rewriting approach, Data & Knowledge Engineering, v.62 n.1, p.101-117, July, 2007
Virginia Niculescu, Cost-efficient parallel programs based on set-distributions for polynomial interpolation, Journal of Parallel and Distributed Computing, v.67 n.8, p.935-946, August, 2007
Dirk Beyer , Thomas A. Henzinger , Rupak Majumdar , Andrey Rybalchenko, Path invariants, ACM SIGPLAN Notices, v.42 n.6, June 2007
Carlos J. Lucena , Daniel M. Berry, Towards a definition of structured programming, Proceedings of the 1974 annual ACM conference, January 01-01, 1974
D. Knuth, Structured programming with go to statements, Classics in software engineering, Yourdon Press, Upper Saddle River, NJ, 1979
Andrew Ireland , Jamie Stark, Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis, Automated Software Engineering, v.13 n.1, p.65-105, January 2006
Matthew B. Dwyer , John Hatcliff , Robby Robby , Corina S. Pasareanu , Willem Visser, Formal Software Analysis Emerging Trends in Software Model Checking, 2007 Future of Software Engineering, p.120-136, May 23-25, 2007
Heinz Schmidt , Iman Poernomo , Ralf Reussner, Trust-By-Contract: Modelling, Analysing And Predicting Behaviour Of Software Architectures, Journal of Integrated Design & Process Science, v.5 n.3, p.25-51, August 2001
Cengiz Erbas , Murat M. Tanik, Modeling And Verification Of Real-Time Systems, Journal of Integrated Design & Process Science, v.7 n.3, p.11-37, August 2003
Meir M. Lehman , Juan F. Ramil, Software Evolution and Software Evolution Processes, Annals of Software Engineering, v.14 n.1-4, p.275-309, December 2002
A. Mili , R. Mili , R. T. Mittermeir, A survey of software reuse libraries, Annals of Software Engineering, 5, p.349-414, 1998
Leslie Lamport , Fred B. Schneider, Constraints: a uniform approach to aliasing and typing, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.205-216, January 14-16, 1985, New Orleans, Louisiana, United States
Wee Kheng Leow , Siau Cheng Khoo , Yi Sun, Automated Generation of Test Programs from Closed Specifications of Classes and Test Cases, Proceedings of the 26th International Conference on Software Engineering, p.96-105, May 23-28, 2004
Bernhard Reus , Jan Schwinghammer, Denotational semantics for a program logic of objects, Mathematical Structures in Computer Science, v.16 n.2, p.313-358, April 2006
John Penix , Perry Alexander, Efficient Specification-Based Component Retrieval, Automated Software Engineering, v.6 n.2, p.139-170, April 1999
Ali Mili, Desert Island Column: The Long Story of a Short Theorem, Automated Software Engineering, v.6 n.2, p.199-204, April 1999
Farn Wang , Chia-Tien Lo, Procedure-Level Verification of Real-time Concurrent Systems, Real-Time Systems, v.16 n.1, p.81-114, Jan. 1999
Jianguo Lu , John Mylopoulos , Masateru Harao , Masami Hagiya, Higher order generalization and its application in program verification, Annals of Mathematics and Artificial Intelligence, v.28 n.1-4, p.107-126, 2000
Andrew Ireland , Jamie Stark, Proof planning for strategy development, Annals of Mathematics and Artificial Intelligence, v.29 n.1-4, p.65-97, 2000
Jozef Hooman , Onno Van Roosmalen, An Approach to Platform Independent Real-Time Programming: (1) Formal Description, Real-Time Systems, v.19 n.1, p.61-85, July 2000
C Karfa , C Mandal , D Sarkar , S R. Pentakota , Chris Reade, A Formal Verification Method of Scheduling in High-level Synthesis, Proceedings of the 7th International Symposium on Quality Electronic Design, p.71-78, March 27-29, 2006
Matthias Blume , David McAllester, Sound and complete models of contracts, Journal of Functional Programming, v.16 n.4-5, p.375-414, July 2006
Ellie D'hondt , Prakash Panangaden, Quantum weakest preconditions, Mathematical Structures in Computer Science, v.16 n.3, p.429-451, June 2006
Henning Christiansen , Davide Martinenghi, On Simplification of Database Integrity Constraints, Fundamenta Informaticae, v.71 n.4, p.371-417, December 2006
V. Dagdilelis , M. Satratzemi, Post's Machine: A Didactic Microworld as an Introduction to Formal Programming, Education and Information Technologies, v.6 n.2, p.123-141, June 2001
Allen Leung , Krishna V. Palem , Amir Pnueli, TimeC: A Time Constraint Language for ILP Processor Compilation, Constraints, v.7 n.2, p.75-115, April 2002
José Mauro V. de Castilho , Marco A. Casanova , Antonio L. Furtado, A Temporal Framework for Database Specifications, Proceedings of the 8th International Conference on Very Large Data Bases, p.280-291, September 08-10, 1982
V. A. Nepomniaschy, Symbolic method of verification of definite iterations over altered data structures, Programming and Computing Software, v.31 n.1, p.1-9, January 2005
Mike A. Marin, Effective use of assertions in C++, ACM SIGPLAN Notices, v.31 n.11, p.28-32, Nov. 1996
Andreas Rösel , Paul Bailes, Identifying foundations of software engineering expertise, ACM SIGCSE Bulletin, v.24 n.4, p.52-64, Dec. 1992
Nimish Shah, Knowledge Representation, Reasoning and Declarative Problem Solving by C. Baral, Cambridge University Press, 2003, Journal of Functional Programming, v.14 n.5, p.588-589, September 2004
Alvaro Arenas , Benjamin Aziz , Juan Bicarregui , Brian Matthews, Managing Conflicts of Interest in Virtual Organisations, Electronic Notes in Theoretical Computer Science (ENTCS), v.197 n.2, p.45-56, February, 2008
R. S. Lazić , T. C. Newcomb , A. W. Roscoe, On model checking data-independent systems with arrays without reset, Theory and Practice of Logic Programming, v.4 n.5-6, p.659-693, September 2004
Patrick Cousot , Radhia Cousot, Bi-inductive Structural Semantics, Electronic Notes in Theoretical Computer Science (ENTCS), v.192 n.1, p.29-44, October, 2007
Marvin V. Zelkowitz, Algebra and models (and reality), ACM SIGSOFT Software Engineering Notes, v.20 n.2, p.55-57, April 1995
V. A. Nepomniaschy , I. S. Anureev , A. V. Promskii, Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language, Programming and Computing Software, v.29 n.6, p.338-350, November-December 2003
V. A. Nepomniaschy, Verification of finite iterations over collections of variable data structures, Cybernetics and Systems Analysis, v.43 n.3, p.341-352, May 2007
A. L. Furtado , P. A. S. Velosa, Iteration for applicative languages, ACM SIGPLAN Notices, v.23 n.12, p.86-94, Dec. 1988
Daniel J. Salomon, Four Dimensions of programming-language independence, ACM SIGPLAN Notices, v.27 n.3, p.35-53, March 1992
Mouloud Arab, Enhancing program comprehension: formatting and documenting, ACM SIGPLAN Notices, v.27 n.2, p.37-46, Feb. 1992
Amnon H. Eden, Three Paradigms of Computer Science, Minds and Machines, v.17 n.2, p.135-167, July 2007
Raymond Turner, Understanding Programming Languages, Minds and Machines, v.17 n.2, p.203-216, July 2007
Andrew Ireland , Bill J. Ellis , Andrew Cook , Roderick Chapman , Janet Barnes, An Integrated Approach to High Integrity Software Verification, Journal of Automated Reasoning, v.36 n.4, p.379-410, April 2006
P. Grogono, Comments, assertions and pragmas, ACM SIGPLAN Notices, v.24 n.3, p.79-84, March 1989
John R. Thompson, The use and abuse of formal proofs, ACM SIGPLAN Notices, v.18 n.7, July 1983
William J. Pervin, Verification of Ada 1/0 statements, ACM SIGCSE Bulletin, v.21 n.2, p.57-60, June 1989
Ralph Benzinger, Automated complexity analysis of Nuprl extracted programs, Journal of Functional Programming, v.11 n.1, p.3-31, January 2001
David M. Goldschlag, A Mechanization of Unity in PC-NQTHM-92, Journal of Automated Reasoning, v.23 n.3, p.445-498, November 1999
David A. Schmidt, Induction, Domains, Calculi: Strachey's Contributions to Programming-Language Engineering, Higher-Order and Symbolic Computation, v.13 n.1-2, p.89-101, April 2000
Robert D. Tennent , Dan R. Ghica, Abstract Models of Storage, Higher-Order and Symbolic Computation, v.13 n.1-2, p.119-129, April 2000
Jean-Christophe Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of Functional Programming, v.13 n.4, p.709-745, July 2003
John C. Reynolds, Definitional Interpreters for Higher-Order Programming Languages, Higher-Order and Symbolic Computation, v.11 n.4, p.363-397, December 1998
Ralf Sasse , José Meseguer, Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics, Electronic Notes in Theoretical Computer Science (ENTCS), v.176 n.4, p.29-46, July, 2007
Z. Manna , A. Pnueli, Specification and verification of concurrent programs by A∀automata, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.1-2, January 21-23, 1987, Munich, West Germany
Thomas E. Hart , Marsha Chechik , David Lie, Security benchmarking using partial verification, Proceedings of the 3rd conference on Hot topics in security, p.1-6, July 29, 2008, San Jose, CA
Helmut K. Berg , Prakash Rao , Bruce D. Shriver, Firmware quality assurance, Proceedings of the June 7-10, 1982, national computer conference, June 07-10, 1982, Houston, Texas
John R. Hughes , Cliff B. Jones, Reasoning about programs via operational semantics: requirements for a support system, Automated Software Engineering, v.15 n.3-4, p.299-312, December 2008
Enrique Alba , Francisco Chicano, Observations in using parallel and sequential evolutionary algorithms for automatic software testing, Computers and Operations Research, v.35 n.10, p.3161-3183, October, 2008
Arnold Pears , Stephen Seidman , Lauri Malmi , Linda Mannila , Elizabeth Adams , Jens Bennedsen , Marie Devlin , James Paterson, A survey of literature on the teaching of introductory programming, ACM SIGCSE Bulletin, v.39 n.4, December 2007
Raimund Kirner, SCCP/x: a compilation profile to support testing and verification of optimized code, Proceedings of the 2007 international conference on Compilers, architecture, and synthesis for embedded systems, September 30-October 03, 2007, Salzburg, Austria
John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, ACM Turing award lectures, ACM, New York, NY, 2007
Kenneth Koster , David C. Kao, State coverage: a structural test adequacy criterion for behavior checking, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
Annalisa Bossi , Ombretta Gaggi, Enriching SMIL with assertions for temporal validation, Proceedings of the 15th international conference on Multimedia, September 25-29, 2007, Augsburg, Germany
Hai Zhou, A new efficient retiming algorithm derived by formal manipulation, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.1, p.1-19, January 2008
Sunae Seo , Hongseok Yang , Kwangkeun Yi , Taisook Han, Goal-directed weakening of abstract interpretation results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.6, p.39-es, October 2007
Martin Karsten , S. Keshav , Sanjiva Prasad , Mirza Beg, An axiomatic basis for communication, ACM SIGCOMM Computer Communication Review, v.37 n.4, October 2007
Andrew Ireland, Cooperative reasoning for automatic software verification, Proceedings of the second workshop on Automated formal methods, p.51-54, November 06-06, 2007, Atlanta, Georgia
Steve M. Shaner , Gary T. Leavens , David A. Naumann, Modular verification of higher-order methods with mandatory calls specified by model programs, ACM SIGPLAN Notices, v.42 n.10, October 2007
Henrique Rebêlo , Sérgio Soares , Ricardo Lima , Leopoldo Ferreira , Márcio Cornélio, Implementing Java modeling language contracts with AspectJ, Proceedings of the 2008 ACM symposium on Applied computing, March 16-20, 2008, Fortaleza, Ceara, Brazil
Josep Carmona , Jordi Cortadella , Yousuke Takada , Ferdinand Peper, Formal methods for the analysis and synthesis of nanometer-scale cellular arrays, ACM Journal on Emerging Technologies in Computing Systems (JETC), v.4 n.2, p.1-27, April 2008
Patrick Eugster , Pascal Felber , Fabrice Le Fessant, The "art" of programming gossip-based systems, ACM SIGOPS Operating Systems Review, v.41 n.5, October 2007
Mikoláš Janota , Radu Grigore , Michal Moskal, Reachability analysis for annotated code, Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, p.23-30, September 03-04, 2007, Dubrovnik, Croatia
Gergely Dévai, Programming language elements for correctness proofs, Acta Cybernetica, v.18 n.3, p.403-425, January 2008
Jerry den Hartog, Towards mechanized correctness proofs for cryptographic algorithms, Science of Computer Programming, v.74 n.1-2, p.52-63, December, 2008
Erika Ábrahám , Frank S. de Boer , Willem-Paul de Roever , Martin Steffen, A Deductive Proof System for Multithreaded Java with Exceptions, Fundamenta Informaticae, v.82 n.4, p.391-463, February 2008
Sandip Ray , Warren A. Hunt, Jr. , John Matthews , J. Strother Moore, A Mechanical Analysis of Program Verification Strategies, Journal of Automated Reasoning, v.40 n.4, p.245-269, May 2008
Jacques Carette , Ryszard Janicki, Computing Properties of Numerical Imperative Programs by Symbolic Computation, Fundamenta Informaticae, v.80 n.1-3, p.125-146, January 2007
Michał Krynicki , Marcin Mostowski , Konrad Zdanowski, Finite Arithmetics, Fundamenta Informaticae, v.81 n.1-3, p.183-202, January 2007
Alexander Paar , Jürgen Reuter , John Soldatos , Kostas Stamatis , Lazaros Polymenakos, A formally specified ontology management API as a registry for ubiquitous computing systems, Applied Intelligence, v.30 n.1, p.37-46, February 2009
T. A. Linden, A summary of progress toward proving program correctness, Proceedings of the December 5-7, 1972, fall joint computer conference, part I, December 05-07, 1972, Anaheim, California
Edgar G. Daylight , Arnout Vandecappelle , Francky Catthoor, The formalism underlying EASYMAP: A precompiler for refinement-based exploration of hierarchical data organizations, Science of Computer Programming, v.72 n.3, p.71-135, August, 2008
Sérgio Agostinho , Ana Moreira , Pedro Guerreiro, Contracts for aspect-oriented design, Proceedings of the 2008 AOSD workshop on Software engineering properties of languages and aspect technologies, p.1-6, March 31-April 04, 2008, Brussels, Belgium
Nicola Bombieri , Franco Fummi , Graziano Pravadelli , Andrea Fedeli, Hybrid, Incremental Assertion-Based Verification for TLM Design Flows, IEEE Design & Test, v.24 n.2, p.140-152, March 2007
Michael J. McGill, Considerations in the transfer of software engineering technology, Proceedings of the May 19-22, 1980, national computer conference, May 19-22, 1980, Anaheim, California
Femke Jonge , Nico Roos , Cees Witteveen, Primary and secondary diagnosis of multi-agent plan execution, Autonomous Agents and Multi-Agent Systems, v.18 n.2, p.267-294, April 2009
Aleksandar Nanevski , Greg Morrisett , Lars Birkedal, Hoare type theory, polymorphism and separation1, Journal of Functional Programming, v.18 n.5-6, p.865-911, September 2008
Thomas Ridge, Verifying distributed systems: the operational approach, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
Ian Wehrman , C. A. R. Hoare , Peter W. O'Hearn, Graphical models of separation logic, Information Processing Letters, v.109 n.17, p.1001-1004, August, 2009
Matthias Klusch , Frank Kaufer, WSMO-MX: A hybrid Semantic Web service matchmaker, Web Intelligence and Agent Systems, v.7 n.1, p.23-42, January 2009
JosÉ m. CaÑete-valdeÓn, On the interpretation of mathematical entities in the formalisation of programming and modelling languages, Mathematical Structures in Computer Science, v.18 n.6, p.1017-1030, December 2008
Vaughan R. Pratt, Logics of programs, Encyclopedia of Computer Science, 4th edition, John Wiley and Sons Ltd., Chichester, 2003
David Gries, Loop invariant, Encyclopedia of Computer Science, 4th edition, John Wiley and Sons Ltd., Chichester, 2003
Patrick Cousot , Radhia Cousot, Bi-inductive structural semantics, Information and Computation, v.207 n.2, p.258-283, February, 2009
Leslie Lamport, Teaching concurrency, ACM SIGACT News, v.40 n.1, March 2009
Christian Fritz , Richard Hull , Jianwen Su, Automatic construction of simple artifact-based business processes, Proceedings of the 12th International Conference on Database Theory, March 23-25, 2009, St. Petersburg, Russia
Iman Narasamdya , Michaël Périn, Certification of smart-card applications in common criteria, Proceedings of the 2009 ACM symposium on Applied Computing, March 08-12, 2009, Honolulu, Hawaii
Renato Cherini , Javier O. Blanco, Local reasoning for abstraction and sharing, Proceedings of the 2009 ACM symposium on Applied Computing, March 08-12, 2009, Honolulu, Hawaii
Rajeev Alur , P. Madhusudan, Adding nesting structure to words, Journal of the ACM (JACM), v.56 n.3, p.1-43, May 2009
Filip Marić, Formalization and Implementation of Modern SAT Solvers, Journal of Automated Reasoning, v.43 n.1, p.81-119, June 2009
Benjamin Livshits , Aditya V. Nori , Sriram K. Rajamani , Anindya Banerjee, Merlin: specification inference for explicit information flow problems, ACM SIGPLAN Notices, v.44 n.6, June 2009
Joseph M. Morris , Alexander Bunkenburg , Malcolm Tyrrell, Term transformers: A new approach to state, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.4, p.1-42, May 2009
Carroll Morgan, The Shadow Knows: Refinement and security in sequential programs, Science of Computer Programming, v.74 n.8, p.629-653, June, 2009
Klaus Ostermann, Reasoning about aspects with common sense, Proceedings of the 7th international conference on Aspect-oriented software development, March 31-April 04, 2008, Brussels, Belgium
Eike Best , Kerstin Strecker, Relational Semantics Revisited, Electronic Notes in Theoretical Computer Science (ENTCS), v.229 n.4, p.27-47, August, 2009
Magnus O. Myreen , Michael J. C. Gordon, Transforming Programs into Recursive Functions, Electronic Notes in Theoretical Computer Science (ENTCS), 240, p.185-200, July, 2009
Jussi Rintanen, Regression for Classical and Nondeterministic Planning, Proceeding of the 2008 conference on ECAI 2008: 18th European Conference on Artificial Intelligence, p.568-572, June 27, 2008
Erkki Laitila, Foundation for program understanding, Proceeding of the 2008 conference on Tenth Scandinavian Conference on Artificial Intelligence: SCAI 2008, p.169-174, June 22, 2008
Long Li , Yu Zhang , Yi-Yun Chen , Yong Li, Certifying concurrent programs using transactional memory, Journal of Computer Science and Technology, v.24 n.1, p.110-121, January 2009
Luis Farinas-del-Cerro, Temporal reasoning and termination of programs, Proceedings of the Eighth international joint conference on Artificial intelligence, p.926-929, August 08-12, 1983, Karlsruhe, West Germany
Richard C. Waters, A method for automatically analyzing programs, Proceedings of the 6th international joint conference on Artificial intelligence, p.935-941, August 20-23, 1979, Tokyo, Japan
Peter Henderson, Derived semantics for some programming language constructs, Proceedings of the 2nd international joint conference on Artificial intelligence, p.490-496, September 01-03, 1971, London, England
Stephen Fickas , Ruven Brooks, Recognition in a program understanding system, Proceedings of the 6th international joint conference on Artificial intelligence, p.266-268, August 20-23, 1979, Tokyo, Japan
S. D. Litvintchouk , V. R. Pratt, A proof-checker for dynamic logic, Proceedings of the 5th international joint conference on Artificial intelligence, p.552-558, August 22-25, 1977, Cambridge, USA
Jean Louis Lauriere, Toward efficiency trough generality, Proceedings of the 6th international joint conference on Artificial intelligence, p.519-521, August 20-23, 1979, Tokyo, Japan
Jared L. Darlington, Automatic program synthesis in second-order logic, Proceedings of the 3rd international joint conference on Artificial intelligence, p.537-542, August 20-23, 1973, Stanford, USA
Dominique Méry, A simple refinement-based method for constructing algorithms, ACM SIGCSE Bulletin, v.41 n.2, June 2009
Raimund Kirner, Towards preserving model coverage and structural code coverage, EURASIP Journal on Embedded Systems, 2009, p.1-16, January 2009
Michal Armoni , Mordechai Ben-Ari, The concept of nondeterminism: its development and implications for teaching, ACM SIGCSE Bulletin, v.41 n.2, June 2009
Tobias Wrigstad , Patrick Eugster , John Field , Nate Nystrom , Jan Vitek, Software hardening: a research agenda, Proceedings for the 1st workshop on Script to Program Evolution, p.58-70, July 06-06, 2009, Genova, Italy
Andrea Asperti , Herman Geuvers , Raja Natarajan, Social processes, program verification and all that, Mathematical Structures in Computer Science, v.19 n.5, p.877-896, October 2009
R. Goldberg, Software engineering: an emerging discipline, IBM Systems Journal, v.25 n.3-4, p.334-353, September 1986
R. E. Quinnan, The management of software engineering: part V:software engineering management practices, IBM Systems Journal, v.19 n.4, p.466-477, December 1980
V. R. Yakhnis , J. A. Farrell , S. S. Shultz, Deriving programs using generic algorithms, IBM Systems Journal, v.33 n.1, p.158-181, 1994
H. D. Mills, The management of software engineering part I: principles of software engineering, IBM Systems Journal, v.38 n.2-3, p.289-295, 1999

INDEX TERMS

Primary Classification:
  D. Software

Additional Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.0 General
          Subjects: Computer arithmetic


General Terms:
Design, Theory


Keywords:
axiomatic method, formal language definition, machine-independent programming, program documentation, programming language design, theory of programming' proofs of programs

Collaborative Colleagues:
C. A. R. Hoare: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player