Krzysztof R. Apt
- W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt, and M. Ulbrich (Eds.). 2016. Deductive Software Verification—The KeY Book: From Theory to Practice, Vol. 10001 of Lecture Notes in Computer Science. Springer. ISBN 978-3-319-49811-9. DOI: .Google Scholar
Cross Ref
- K. R. Apt and E.-R. Olderog. 2019. Fifty years of Hoare’s logic. Form. Asp. Comput. 31, 6, 751–807. DOI: .Google ScholarDigital Library
- K. R. Apt, N. Francez, and W. P. de Roever. 1980. A proof system for communicating sequential processes. ACM Trans. Prog. Lang. Syst. 2, 3, 359–385. DOI: .Google ScholarDigital Library
- K. R. Apt, F. S. de Boer, and E.-R. Olderog. 2009. Verification of Sequential and Concurrent Programs (3rd. ed.). Springer-Verlag, New York. DOI: .Google ScholarCross Ref
- M. Barnett, B. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. 2005. Boogie: A modular reusable verifier for object-oriented programs. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever (Eds.), Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Revised Lectures, Vol. 4111 of Lecture Notes in Computer Science. Springer, 364–387. DOI: .Google ScholarDigital Library
- E. M. Clarke. 1979. Programming language constructs for which it is impossible to obtain good Hoare axiom systems. J. ACM 26, 1, 129–147. DOI: .Google ScholarDigital Library
- S. A. Cook. 1978. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1, 70–90. DOI: .Google ScholarDigital Library
- W. Damm and B. Josko. 1983. A sound and relatively complete Hoare-logic for a language with higher type procedures. Acta Inf. 20, 59–101. DOI: .Google ScholarDigital Library
- W. P. de Roever, F. S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. 2001. Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Vol. 54 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.Google ScholarDigital Library
- E. W. Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 453–457. DOI: .Google ScholarDigital Library
- E. W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ.Google ScholarDigital Library
- J.-C. Filliâtre. 2007. Formal proof of a program: Find. Sci. Comput. Program. 64, 3, 332–340. DOI: .Google ScholarCross Ref
- J. Filliâtre and A. Paskevich. 2013. Why3—Where programs meet provers. In M. Felleisen and P. Gardner (Eds.), Programming Languages and Systems—22nd European Symposium on Programming, ESOP 2013, Proceedings, Vol. 7792 of Lecture Notes in Computer Science. Springer, 125–128. DOI: .Google ScholarDigital Library
- R. W. Floyd. 1967. Assigning meaning to programs. In J. T. Schwartz (Ed.), Proceedings of Symposium on Applied Mathematics 19, Mathematical Aspects of Computer Science. American Mathematical Society, New York, 19–32.Google Scholar
- M. Foley and C. A. R. Hoare. 1971. Proof of a recursive program: Quicksort. Comput. J. 14, 4, 391–395. DOI: .Google ScholarCross Ref
- S. M. German, E. M. Clarke, and J. Y. Halpern. 1989. Reasoning about procedures as parameters in the language L4. Inf. Comput. 83, 3, 265–359. DOI: .Google ScholarDigital Library
- G. A. Gorelick. 1975. A Complete Axiomatic System for Proving Assertions about Recursive and Nonrecursive Programs. Technical Report 75, Department of Computer Science, University of Toronto. Available at https://archive.org/details/ACompleteAxiomaticSystemForProvingAssertionsAboutRecursiveAnd.Google Scholar
- I. Greif and A. R. Meyer. 1981. Specifying the semantics of while programs: A tutorial and critique of a paper by Hoare and Lauer. ACM Trans. Program. Lang. Syst. 3, 4, 484–507. .Google ScholarDigital Library
- D. Harel. 1979. First-Order Dynamic Logic. Lecture Notes in Computer Science 68, Springer-Verlag, New York. DOI: .Google ScholarCross Ref
- C. A. R. Hoare. 1961a. Algorithm 65: Find. Commun. ACM 4, 7, 321. DOI: .Google ScholarDigital Library
- C. A. R. Hoare. 1961b. Algorithm 64: Quicksort. Commun. ACM 4, 7, 321. DOI: .Google ScholarDigital Library
- C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 576–580, 583. DOI: .Google ScholarDigital Library
- C. A. R. Hoare. 1971a. Procedures and parameters: An axiomatic approach. In E. Engeler (Ed.), Proceedings of Symposium on the Semantics of Algorithmic Languages. Lecture Notes in Mathematics 188, Springer-Verlag, New York, 102–116.Google Scholar
- C. A. R. Hoare. 1971b. Proof of a program: FIND. Commun. ACM 14, 1, 39–45. DOI: .Google ScholarDigital Library
- C. A. R. Hoare. 1972a. Proof of a structured program: ‘The sieve of Eratosthenes’. Comput. J. 15, 4, 321–325. DOI: .Google ScholarCross Ref
- C. A. R. Hoare. 1972b. Proof of correctness of data representation. Acta Inf. 1, 271–281. DOI: .Google ScholarDigital Library
- C. A. R. Hoare. 1972c. Towards a theory of parallel programming. In C. A. R. Hoare and R. H. Perrot (Eds.), Operating Systems Techniques. Academic Press, London, 61–71.Google Scholar
- C. A. R. Hoare. 1975. Parallel programming: An axiomatic approach. Comput. Lang. 1, 2, 151–160. DOI: .Google ScholarDigital Library
- C. A. R. Hoare. 1978. Communicating sequential processes. Commun. ACM 21, 666–677. DOI: .Google ScholarDigital Library
- C. A. R. Hoare and N. Wirth. 1973. An axiomatic definition of the programming language PASCAL. Acta Inf. 2, 335–355. DOI: .Google ScholarDigital Library
- C. A. R. Hoare and P. E. Lauer. 1974. Consistent and complementary formal theories of the semantics of programming languages. Acta Inf. 3, 135–153. DOI: .Google ScholarDigital Library
- C. B. Jones. 1983. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5, 4, 596–619. DOI: .Google ScholarDigital Library
- L. Lamport. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2, 125–143. DOI: .Google ScholarDigital Library
- H. Langmaack and E.-R. Olderog. 1980. Present-day Hoare-like systems for programming languages with procedures: Power, limits and most likely expressions. In J. W. de Bakker and J. van Leeuwen (Eds.), Automata, Languages and Programming, 7th Colloquium, Vol. 85 of Lecture Notes in Computer Science. Springer, 363–373.Google Scholar
- G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok. 2005. How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55, 1–3, 185–208. DOI: .Google ScholarDigital Library
- G. Levin and D. Gries. 1981. A proof technique for communicating sequential processes. Acta Inf. 15, 281–302. DOI: .Google ScholarDigital Library
- Z. Manna and A. Pnueli. 1991. The Temporal Logic of Reactive and Concurrent Systems—Specification. Springer-Verlag, New York. DOI: .Google ScholarCross Ref
- Z. Manna and A. Pnueli. 1995. Temporal Verification of Reactive Systems—Safety. Springer-Verlag, New York. DOI: .Google ScholarCross Ref
- B. Meyer. 1997. Object-Oriented Software Construction (2nd. ed.). Prentice-Hall.Google Scholar
- G. Mirkowska and A. Salwicki. 1987. Algorithmic Logic. Kluwer Academic Publishers, Norwell, MA. ISBN 9027719284.Google Scholar
- F. L. Morris and C. B. Jones. 1984. An early program proof by Alan Turing. Ann. Hist. Comput. 6, 139–143. .Google ScholarDigital Library
- P. Naur. 1966. Proof of algorithms by general snapshots. BIT Numer. Math. 6, 4, 310–316. DOI: .Google ScholarDigital Library
- P. W. O’Hearn. 2007. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 1–3, 271–307. DOI: .Google ScholarDigital Library
- P. W. O’Hearn. 2019. Separation logic. Commun. ACM 62, 2, 86–95. DOI: .Google ScholarDigital Library
- E.-R. Olderog. 1984. Correctness of programs with Pascal-like procedures without global variables. Theor. Comput. Sci. 30, 49–90. DOI: .Google ScholarCross Ref
- S. Owicki. 1978. Verifying concurrent programs with shared data classes. In E. J. Neuhold (Ed.), Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts. North-Holland, Amsterdam, 79–298.Google Scholar
- S. Owicki and D. Gries. 1976a. An axiomatic proof technique for parallel programs. Acta Inf. 6, 319–340. DOI: .Google ScholarDigital Library
- S. Owicki and D. Gries. 1976b. Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19, 279–285. DOI: .Google ScholarDigital Library
- R. Piskac and P. Rümmer (Eds.). 2018. Verified Software. Theories, Tools, and Experiments—10th International Conference, VSTTE 2018, Oxford, UK, July 18–19, 2018, Revised Selected Papers, Vol. 11294 of Lecture Notes in Computer Science. Springer. ISBN 978-3-030-03591-4. DOI: .Google ScholarDigital Library
- A. Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science. 46–57. DOI: .Google ScholarDigital Library
- V. R. Pratt. 1976. Semantical considerations on Floyd–Hoare logic. In 17th Annual Symposium on Foundations of Computer Science (FoCS 1976). IEEE Computer Society, 109–121. DOI: .Google ScholarDigital Library
- J. C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002). IEEE Computer Society, 55–74. DOI: .Google ScholarCross Ref
- A. Salwicki. 1970. Formalized algorithmic languages. Bull. Acad. Pol. Sci. 18, 227–232.Google Scholar
- D. S. Scott and J. W. de Bakker. 1969. A theory of programs. Notes of an IBM Vienna Seminar.Google Scholar
- A. M. Turing. 1949. On checking a large routine. Report of a Conference on High Speed Automatic Calculating Machines. University Mathematics Laboratory, Cambridge, 67–69. (See also: F. L. Morris and C. B. Jones. 1984. An early program proof by Alan Turing. Ann. Hist. Comput. 6, 139–143.)Google Scholar
- M. Wand. 1978. A new incompleteness result for Hoare’s system. J. ACM 25, 1, 168–175. DOI: .Google ScholarDigital Library
- N. Wirth. 1971. Program development by stepwise refinement. Commun. ACM 14, 4, 221–227. DOI: .Google ScholarDigital Library
- N. Wirth. 1973. Systematic Programming: An Introduction. Prentice-Hall.Google ScholarDigital Library
Index Terms
- Assessing the Success and Impact of Hoare’s Logic
Index terms have been assigned to the content through auto-classification.
Recommendations
Design of reversible logic based full adder in current-mode logic circuits
AbstractDemand of Very Large Scale Integration (VLSI) circuits with very high speed and low power are increased due to communication system's transmission speed increase. During computation, heat is dissipated by a traditional binary logic or logic ...
Logic Networks of Carry-Save Adders
logic networks of carry-save adders such as high-speed multipliers, multioperand adders, and double-rail input parallel adders are designed based on the parallel adders with a minimum number of NOR gates discussed in [1]. After a discussion of the ...
Multiple-Valued Logic Charge-Coupled Devices
A new method to implement multiple-valued logic in large scale integrated circuits is introduced. The data are represented by discrete amounts of charge in a charge-coupled device. In this paper the design principles and realizations in four-valued ...
Comments