Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language

Apt, 1981, Ten years of Hoare’s logic: a survey — part 1, ACM Trans. Programming Lang. Syst., 3, 431, 10.1145/357146.357150 Apt, 1984, Ten years of Hoare’s logic: a survey part II: nondeterminism, Theoret. Comput. Sci., 28 J.P. Bowen, J. He, Q. Xu, An animatable operational semantics of the Verilog Hardware Description Language, in: Proc.ICFEM 2000: 3rd IEEE International Conference on Formal Engineering Methods, IEEE Computer Society Press, 2000, pp. 199–207. Brookes, 2006, A grainless semantics for parallel programs with shared mutable data, Electron. Notes Theor. Comput. Sci., 155, 277, 10.1016/j.entcs.2005.11.060 Brookes, 1996, Full abstraction for a shared-variable parallel language, Inform. and Comput., 127, 145, 10.1006/inco.1996.0056 M. Butler, S. Ripon, Executable semantics for compensating CSP, in: Proc. EPEW 2005: International Workshop on Web Services and Formal Methods, Versailles, France, September 1–3, 2005, Lecture Notes in Computer Science, vol. 3670, Springer-Verlag, 2005, pp. 243–256. Clocksin, 2003 de Bakker, 1996 F.S. de Boer, A sound and complete shared-variable concurrency model for multi-threaded Java programs, in: Proc. 9th IFIP WG 6.1 International Conference on Formal Methods for Open Object-based Distributed Systems, FMOODS’07, Springer-Verlag, 2007, pp 252–268. de Roever, 2001 J. den Hartog, Probabilistic extensions of semantic models, Ph.D. thesis, Vrije University, The Netherlands, 2002. den Hartog, 1999, Mixing up nondeterminism and probability: a preliminary report, Electron. Notes Theoret. Comput. Sci., 22, 10.1016/S1571-0661(05)82521-6 den Hartog, 2002, Verifying probabilistic programs using a Hoare like logic, Internat. J. Found. Comput. Sci., 40, 315, 10.1142/S012905410200114X den Hartog, 2001, Metric semantics and full abstractness for action refinement and probabilistic choice, Electron. Notes Theoret. Comput. Sci., 40, 10.1016/S1571-0661(05)80038-6 Dijkstra, 1968, The structure of the THE-multiprogramming system, Commun. ACM, 11, 341, 10.1145/363095.363143 Hansen, 1972, Structured multiprogramming, Commun. ACM, 15, 574, 10.1145/361454.361473 He, 1994 J. He, An algebraic approach to the Verilog programming, in: Proc. 10th Anniversary Colloquium of UNU/IIST, Lisbon, Portugal, March 18–20, 2002, Lecture Notes in Computer Science, vol. 2757, Springer, 2003, pp 65–80. J. He, J.W. Sanders, Unifying probability, in: Proc. UTP 2006: Unifying Theories of Programming, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5–7, 2006, Lecture Notes in Computer Science, vol. 4010, Springer, 2006, pp. 173–199. J. He, H. Zhu, Formalising Verilog, in: Proc. ICECS 2000: IEEE International Conference on Electronics, Circuits and Systems, IEEE Computer Society Press, 2000, pp. 412–415. He, 1997, Probabilistic models for the guarded command language, Sci. Comput. Programming, 28, 171 Hehner, 1984, Predicative programming, part I, Commun. ACM, 27, 134, 10.1145/69610.357988 Hehner, 1984, Predicative programming, part II, Commun. ACM, 27, 144, 10.1145/69610.357990 E.C.R. Hehner, Probabilistic predicative programming, In: Proc. MPC 2004: 7th International Conference on Mathematics of Program Construction, Stirling, Scotland, UK, July 12–14, 2004, Lecture Notes in Computer Science, vol. 3125, Springer, 2004, pp. 169–185. Hennessy, 1988 C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall International Series in Computer Science, 1985. Hoare, 1993, From algebra to operational semantics, Inform. Process. Lett., 45, 75, 10.1016/0020-0190(93)90219-Y C.A.R. Hoare, J. He, Unifying Theories of Programming, Prentice Hall International Series in Computer Science, 1998. Hoare, 1987, Laws of programming, Commun. ACM, 38, 672, 10.1145/27651.27653 F. Leymann, Web Services Flow Language (WSFL 1.0), IBM, 2001. Available from: <http://www-3.ibm.com/software/solutions/webservices/pdf/WSDL.pdf>. Manna, 1992 Manna, 1995 Manson, 2005, The Java memory model, Principles Programming Lang. (POPL), 378 McIver, 2001, Partial correctness for probabilistic demonic programs, Theoret. Comput. Sci., 266, 513, 10.1016/S0304-3975(00)00208-5 McIver, 2004 McIver, 1996, Probabilistic predicate transformers, ACM Trans. Programming Lang. Syst., 18, 325, 10.1145/229542.229547 Motwani, 1995 U. Ndukwu, J.W. Sanders, Reason about a distributed probabilistic system, Tech. Rep. 401, UNU/IIST, P.O. Box 3058, Macau SAR, China, 2008. U. Ndukwu, J.W. Sanders, Reasoning about a distributed probabilistic system, in: Proc. CATS 2009: Fifteenth Australasian Symposium on Computing: The Australasian Theory, vol. 94, Australian Computer Society, Wellington, New Zealand, 2009, pp. 35–42. N. Nissanke, Realtime Systems, Prentice Hall International Series in Computer Science, 1997. Núñez, 2003, Algebraic theory of probabilistic processes, J. Logic Algebr. Programming, 56, 117, 10.1016/S1567-8326(02)00069-3 M. Núñez, D. de Frutos-Escrig, Testing semantics for probabilistic LOTOS, in: Proc. FORTE’95: IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995, IFIP Conference Proceedings, vol. 43, Chapman & Hall, 1996, pp. 367–382. M. Núñez, D. de Frutos-Escrig, L.F.L. Dı´az, Acceptance trees for probabilistic processes, in: Proc. CONCUR’95: 6th International Conference on Concurrency, Philadelphia, PA, USA, August, 1995, Lecture Notes in Computer Science, vol. 962, Springer, 1995. S. Park, F. Pfenning, S. Thrun, A probabilistic language based upon sampling functions, in: Proc. POPL 2005: 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 2005, pp. 171–182. G. Plotkin, A structural approach to operational semantics, Tech. Rep. 19, University of Aahus, 1981 (also published in The Journal of Logic and Algebraic Programming, vols. 60–61, 2004, pp. 17–139). J.C. Reynolds, Toward a grainless semantics for shared-variable concurrency, in: Proc. FSTTCS 2004, Lecture Notes in Computer Science, vol. 3328, Springer-Verlag, 2004, pp. 35–48. Seidel, 1995, Probabilistic communicating processes, Theoret. Comput. Sci., 152, 219, 10.1016/0304-3975(94)00286-0 Stoy, 1977 H. Zhu, Linking the semantics of a multithreaded discrete event simulation language, Ph.D. thesis, London South Bank University, 2005. H. Zhu, J.P. Bowen, J. He, From operational semantics to denotational semantics for Verilog, in: Proc. CHARME 2001: 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science, vol. 2144, Springer-Verlag, 2001, pp. 449–464. H. Zhu, S. Qin, J. He, J.P. Bowen, Integrating probability with time and shared-variable concurrency, in: Proc. SEW-30: 30th NASA/IEEE Software Engineering Workshop, IEEE Computer Society, 2006, pp. 179–189. H. Zhu, J. He, G. Pu , J. Li, An operational approach to BPEL-like programming, in: Proc. SEW-31: 31st IEEE Software Engineering Workshop, Baltimore, USA, IEEE Computer Society Press, 2007, pp. 236–245. Zhu, 2009, PTSC: Probability, time and shared-variable concurrency, Innov. Syst. Softw. Eng. NASA J., 5, 271, 10.1007/s11334-009-0100-9