Диссертация (1149932), страница 26
Текст из файла (страница 26)
27–51.45. Peled, D. A. Model Checking / D. A. Peled, P. Pelliccione, P. Spoletini // WileyEncyclopedia of Computer Science and Engineering. — 2008.46. Clarke, E. M. Model checking / E. M. Clarke, O. Grumberg, D. Peled. — MITpress, 1999.47. Hoare, C. A. R. An Axiomatic Basis for Computer Programming /C. A. R. Hoare // Commun. ACM. — 1969. — Vol.
12, no. 10. — P. 576–580.13348. Owicki, S. S. An Axiomatic Proof Technique for Parallel Programs I / S. S. Owicki, D. Gries // Acta Inf. — 1976. — Vol. 6. — P. 319–340.49. Owicki, S. S. Verifying Properties of Parallel Programs: An Axiomatic Approach /S. S. Owicki, D. Gries // Commun. ACM.
— 1976. — Vol. 19, no. 5. — P. 279–285.50. O’Hearn, P. W. Resources, Concurrency and Local Reasoning / P. W. O’Hearn //CONCUR 2004 - Concurrency Theory, 15th International Conference, London,UK, August 31 - September 3, 2004, Proceedings. — 2004. — P. 49–67.51. Bornat, R. Permission accounting in separation logic / R. Bornat, C.
Calcagno,P. W. O’Hearn, M. J. Parkinson // Proceedings of the 32nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2005,Long Beach, California, USA, January 12–14, 2005. — 2005. — P. 259–270.52. Hobor, A. Oracle Semantics for Concurrent Separation Logic / A. Hobor,A. W. Appel, F. Zappa Nardelli // Programming Languages and Systems, 17thEuropean Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest,Hungary, March 29–April 6, 2008.
Proceedings. — 2008. — P. 353–367.53. Dockins, R. Multimodal Separation Logic for Reasoning About Operational Semantics / R. Dockins, A. W. Appel, A. Hobor // Electr. Notes Theor. Comput. Sci.— 2008. — Vol. 218. — P. 5–20.54. Hobor, A. Barriers in Concurrent Separation Logic / A. Hobor, C. Gherghina //Programming Languages and Systems — 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory andPractice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3,2011. Proceedings. — 2011. — P. 276–296.55. Gotsman, A. Local Reasoning for Storable Locks and Threads / A.
Gotsman,J. Berdine, B. Cook, N. Rinetzky, M. Sagiv // Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December1, 2007, Proceedings. — 2007. — P. 19–37.56. Jacobs, B. Expressive modular fine-grained concurrency specification / B. Jacobs,F. Piessens // Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on134Principles of Programming Languages, POPL 2011, Austin, TX, USA, January26–28, 2011. — 2011.
— P. 271–282.57. Svendsen, K. Impredicative Concurrent Abstract Predicates / K. Svendsen,L. Birkedal // Programming Languages and Systems — 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April5–13, 2014, Proceedings. — 2014. — P. 149–168.58.
Dinsdale-Young, T. Concurrent Abstract Predicates / T. Dinsdale-Young,M. Dodds, P. Gardner, M. J. Parkinson, V. Vafeiadis // ECOOP 2010 - ObjectOriented Programming, 24th European Conference, Maribor, Slovenia, June 21–25, 2010. Proceedings. — 2010.
— P. 504–528.59. Jung, R. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning / R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal,D. Dreyer // Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India,January 15–17, 2015. — 2015. — P. 637–650.60. Ley-Wild, R. Subjective auxiliary state for coarse-grained concurrency / R. LeyWild, A. Nanevski // The 40th Annual ACM SIGPLAN-SIGACT Symposium onPrinciples of Programming Languages, POPL ’13, Rome, Italy, January 23–25,2013. — 2013. — P.
561–574.61. Sergey, I. Mechanized verification of fine-grained concurrent programs / I. Sergey,A. Nanevski, A. Banerjee // Proceedings of the 36th ACM SIGPLAN Conferenceon Programming Language Design and Implementation, Portland, OR, USA, June15–17, 2015.
— 2015. — P. 77–87.62. Vechev, M. T. Abstraction-guided synthesis of synchronization / M. T. Vechev,E. Yahav, G. Yorsh // STTT. — 2013. — Vol. 15, no. 5-6. — P. 413–431.63. Raychev, V. Automatic Synthesis of Deterministic Concurrency / V. Raychev,M. T.
Vechev, E. Yahav // Static Analysis — 20th International Symposium, SAS2013, Seattle, WA, USA, June 20–22, 2013. Proceedings. — 2013. — P. 283–303.64. Kaiser, J.-O. Strong Logic for Weak Memory: Reasoning About Release-AcquireConsistency in Iris / J.-O. Kaiser, H.-H. Dang, D. Dreyer, O. Lahav, V. Vafeiadis //13531st European Conference on Object-Oriented Programming, ECOOP 2017, June19–23, 2017, Barcelona, Spain. — 2017. — P. 17:1–17:29.65.
Vafeiadis, V. Relaxed separation logic: a program logic for C11 concurrency /V. Vafeiadis, C. Narayan // Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October26–31, 2013. — 2013. — P. 867–884.66. Turon, A. GPS: navigating weak memory with ghosts, protocols, and separation /A. Turon, V. Vafeiadis, D.
Dreyer // Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20–24,2014. — 2014. — P. 691–707.67. Lahav, O. Owicki-Gries Reasoning for Weak Memory Models / O. Lahav,V. Vafeiadis // Automata, Languages, and Programming — 42nd InternationalColloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II.— 2015. — P.
311–323.68. Meshman, Y. Pattern-based Synthesis of Synchronization for the C++ MemoryModel / Y. Meshman, N. Rinetzky, E. Yahav // Formal Methods in ComputerAided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015. —2015. — P. 120–127.69. Dan, A. M. Predicate Abstraction for Relaxed Memory Models / A. M. Dan,Y. Meshman, M. T. Vechev, E.
Yahav // Static Analysis — 20th InternationalSymposium, SAS 2013, Seattle, WA, USA, June 20–22, 2013. Proceedings. —2013. — P. 84–104.70. Документация архитектуры DEC Alpha [Электронный ресурс]. — URL:http://www.ece.cmu.edu/~ece447/s14/lib/exe/fetch.php?media=alphaahb.pdf(дата обращения: 29.12.2017).71. Batty, M. The Problem of Programming Language Concurrency Semantics /M. Batty, K. Memarian, K. Nienhuis, J. Pichon-Pharabod, P. Sewell // LNCS,Programming Languages and Systems — 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and136Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings.— Vol. 9032.
— Springer, 2015. — P. 283–307.72. Gosling, J. The Java Language Specification / J. Gosling, W. N. Joy, G. L. Steele Jr.— Addison-Wesley, 1996.73. The Java Language Specification, Java SE 8 Edition [Электронный ресурс].— URL: https://docs.oracle.com/javase/specs/jls/se8/html/index.html. (датаобращения: 29.12.2017).74. Jackson, D. Software Abstractions: Logic, Language, and Analysis / D. Jackson.— The MIT Press, 2006.75. Torlak, E. Growing Solver-aided Languages with Rosette / E.
Torlak, R. Bodik //Onward! 2013, Proceedings of the 2013 ACM International Symposium on NewIdeas, New Paradigms, and Reflections on Programming & Software. — Onward!2013. — 2013. — P. 135–152.76. Torlak, E. A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages / E. Torlak, R. Bodik // PLDI ’14, Proceedings of the 35th ACM SIGPLANConference on Programming Language Design and Implementation. — PLDI ’14.— 2014. — P. 530–541.77. Wickerson, J.
Automatically Comparing Memory Consistency Models / J. Wickerson, M. Batty, T. Sorensen, G. A. Constantinides // Proceedings of the 44thACM SIGPLAN Symposium on Principles of Programming Languages, POPL2017, Paris, France, January 18–20, 2017. — ACM, 2017.78. Bornholt, J. Synthesizing memory models from framework sketches and Litmus tests / J.
Bornholt, E. Torlak // Proceedings of the 38th ACM SIGPLANConference on Programming Language Design and Implementation, PLDI 2017,Barcelona, Spain, June 18–23, 2017. — 2017. — P. 467–481.79. Memarian, K. Into the Depths of C: Elaborating the De Facto Standards /K. Memarian, J. Matthiesen, J. Lingard, K.
Nienhuis, D. Chisnall, R. N. M. Watson, P. Sewell // PLDI ’16, Proceedings of the 37th ACM SIGPLAN Conferenceon Programming Language Design and Implementation. — PLDI ’16. — 2016.— P. 1–15.13780. Pugh, W. Fixing the Java Memory Model / W. Pugh // Proceedings of the ACM1999 Conference on Java Grande, JAVA ’99, San Francisco, CA, USA, June 12–14, 1999. — 1999. — P. 89–98.81. Pugh, W. The Java memory model is fatally flawed / W. Pugh // Concurrency Practice and Experience. — 2000.
— Vol. 12, no. 6. — P. 445–455.82. ISO/IEC 14882:2014. Programming language C++. — 2014.83. ISO/IEC 14882:2017. Programming language C++. — 2017.84. Batty, M. Clarifying and compiling C/C++ concurrency: from C++11 to POWER /M. Batty, K. Memarian, S. Owens, S.
Sarkar, P. Sewell // POPL 2012. — 2012.— P. 509–520.85. Chakraborty, S. Validating optimizations of concurrent C/C++ programs /S. Chakraborty, V. Vafeiadis // CGO 2016. — 2016. — P. 216–226.86. Lahav, O. Repairing sequential consistency in C/C++11 / O. Lahav, V. Vafeiadis,J. Kang, C.-K. Hur, D. Dreyer // PLDI 2017. — 2017. — P. 618–632.87. Batty, M.
Overhauling SC atomics in C11 and OpenCL / M. Batty, A. F. Donaldson, J. Wickerson // Proceedings of the 43rd Annual ACM SIGPLAN-SIGACTSymposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20–22, 2016. — 2016. — P. 634–648.88. Doko, M.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
