449
views
0
recommends
+1 Recommend
1 collections
    4
    shares
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      Verifying Invariant Based Programs in the SOCOS Environment

      proceedings-article

      , ,

      Teaching Formal Methods: Practice and Experience (TFM)

      Teaching Formal Methods: Practice and Experience

      15 December 2006

      Invariant based programming, verification, SOCOS

      Bookmark

            Abstract

            An invariant based program is a state transition diagram consisting of nested situations (predicates over program variables) and transitions between situations (predicate transformers). Reasoning about correctness is performed in a local fashion by examining each situation at a time and proving that the situation is satisfied for all possible executions. Since the invariants are in place from the beginning and the verification conditions are easily extracted from the diagram there is no need for complicated proof rules, making invariant diagrams a suitable notation for introducing formal verification to students and programmers. Our preliminary experience from using invariant diagrams in the classroom has prompted the need for a tool to support the method: we introduce here SOCOS, an environment for invariant based programming. SOCOS generates correctness conditions based on weakest precondition semantics, and the user can attempt to automatically discharge these conditions using the Simplify theorem prover; conditions which were not automatically discharged can be proved interactively in the PVS theorem prover.

            Content

            Author and article information

            Contributors
            Conference
            December 2006
            December 2006
            : 1-6
            Affiliations
            [0001]Turku Centre for Computer Science

            Åbo Akademi University, Department of Information Technologies

            Joukahaisenkatu 3-5 A, FIN-20520, Turku, Finland
            Article
            10.14236/ewic/TFM2006.5
            2dcfa90f-144d-4fc6-baed-cab7dbc8688b
            © Ralph-Johan Back et al. Published by BCS Learning and Development Ltd. Teaching Formal Methods: Practice and Experience, BCS London Office, UK

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Teaching Formal Methods: Practice and Experience
            TFM
            BCS London Office, UK
            15 December 2006
            Electronic Workshops in Computing (eWiC)
            Teaching Formal Methods: Practice and Experience
            Product
            Product Information: 1477-9358BCS Learning & Development
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Comments

            Comment on this article