Verifying Temporal Properties of Reactive Systems by Transformation

Article, Preprint English OPEN
Hamilton, Geoff;
(2015)
  • Publisher: Open Publishing Association
  • Journal: Electronic Proceedings in Theoretical Computer Science (issn: 2075-2180)
  • Publisher copyright policies & self-archiving
  • Related identifiers: doi: 10.4204/EPTCS.199.3
  • Subject: Computer Science - Programming Languages | Mathematics | Electronic computers. Computer science | Computer Science - Logic in Computer Science | QA1-939 | QA75.5-76.95 | I.2.2, F.3.2
    acm: ComputerApplications_COMPUTERSINOTHERSYSTEMS

We show how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. In particular, we show how the program transformation technique distillation can be used to transform reactive systems specified in... View more
  • References (20)
    20 references, page 1 of 2

    [1] Alberto Pettorossi and Maurizio Proietti and Valerio Senni (2009): Deciding Full Branching Time Logic by Program Transformation. In: 19th International Symposium on Logic-Based Program Synthesis and Transformation, pp. 5-21 doi:10.1007/978-3-642-12592-8 2.

    [2] Alexei Lisitsa and Andrei P. Nemytykh (2008): Reachability Analysis in Verification via Supercompilation. International Journal of Foundations of Computer Science 19(4), pp. 953-969 doi:10.1142/S0129054108006066.

    [3] Amir Pnueli and Elad Shahar (1996): A Platform for Combining Deductive with Algorithmic Verification. In: 8th International Conference on Computer Aided Verification, pp. 184-195 doi:10.1007/3-540-61474-5 68.

    [4] E.M. Clarke, E.A. Emerson & A.P. Sistla (1986): Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2), pp. 244-263 doi:10.1145/5397.5399.

    [5] Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti (2001): Verification of Sets of Infinite State Processes Using Program Transformation. In: 11th International Workshop on Logic Based Program Synthesis and Transformation, pp. 111-128 doi:10.1007/3-540-45607-4 7.

    [6] G.W. Hamilton (2007): Distillation: Extracting the Essence of Programs. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 61-70 doi:10.1145/1244381.1244391.

    [7] G.W. Hamilton & N.D. Jones (2012): Distillation With Labelled Transition Systems. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ACM, pp. 15-24 doi:10.1145/2103746.2103753.

    [8] Henny Sipma and Toma´s E. Uribe and Zohar Manna (1999): Deductive Model Checking. Formal Methods in System Design 15(1), pp. 49-74 doi:10.1023/A:1008791913551.

    [9] Hirohisa Seki (2011): Proving Properties of Co-Logic Programs by Unfold/Fold Transformations. In: 21st International Symposium on Logic-Based Program Synthesis and Transformation, pp. 205-220 doi:10.1007/978-3-642-32211-2 14.

    [10] L. Lamport (1974): A New Solution of Dijkstra's Concurrent Programming Problem. Communications of the ACM 17(8), pp. 453-455 doi:10.1145/361082.361093.

  • Metrics
Share - Bookmark