Results for 'program verification (‘correctness’ proofs, testing)'

Order:
  1.  50
    Deductive program verification (a practitioner's commentary).David A. Nelson - 1992 - Minds and Machines 2 (3):283-307.
    A proof of ‘correctness’ for a mathematical algorithm cannot be relevant to executions of a program based on that algorithm because both the algorithm and the proof are based on assumptions that do not hold for computations carried out by real-world computers. Thus, proving the ‘correctness’ of an algorithm cannot establish the trustworthiness of programs based on that algorithm. Despite the (deceptive) sameness of the notations used to represent them, the transformation of an algorithm into an executable program (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  2.  39
    On the Mutual Dependence Between Formal Methods and Empirical Testing in Program Verification.Nicola Angius - 2020 - Philosophy and Technology 33 (2):349-355.
    This paper provides a review of Raymond Turner’s book Computational Artefacts. Towards a Philosophy of Computer Science. Focus is made on the definition of program correctness as the twofold problem of evaluating whether both the symbolic program and the physical implementation satisfy a set of specifications. The review stresses how these are not two separate problems. First, it is highlighted how formal proofs of correctness need to rely on the analysis of physical computational processes. Secondly, it is underlined (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  3.  27
    Tableaux for constructive concurrent dynamic logic.Duminda Wijesekera & Anil Nerode - 2005 - Annals of Pure and Applied Logic 135 (1-3):1-72.
    This is the first paper on constructive concurrent dynamic logic . For the first time, either for concurrent or sequential dynamic logic, we give a satisfactory treatment of what statements are forced to be true by partial information about the underlying computer. Dynamic logic was developed by Pratt [V. Pratt, Semantical considerations on Floyd–Hoare logic, in: 17th Annual IEEE Symp. on Found. Comp. Sci., New York, 1976, pp. 109–121, V. Pratt, Applications of modal logic to programming, Studia Logica 39 257–274] (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations