المؤلفون: Matsushita, Yusuke, Denis, Xavier, Jourdan, Jacques-Henri, Dreyer, Derek

المساهمون: Tokyo University of Science Tokyo, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Max Planck Institute for Software Systems (MPI-SWS), European Project: 683289,H2020,ERC-2015-CoG,RustBelt(2016)

المصدر: PLDI 2022 - 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation ; https://inria.hal.science/hal-03777103Test ; PLDI 2022 - 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2022, San Diego CA USA, United States. pp.841-856, ⟨10.1145/3519939.3523704⟩

مصطلحات موضوعية: CCS Concepts: • Theory of computation → Programming logic, Separation logic, Type theory Rust, verification, type systems, prophecy variables, Iris, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: San Diego CA USA, United States

العلاقة: info:eu-repo/grantAgreement//683289/EU/Logical Foundations for the Future of Safe Systems Programming/RustBelt; hal-03777103; https://inria.hal.science/hal-03777103Test; https://inria.hal.science/hal-03777103/documentTest; https://inria.hal.science/hal-03777103/file/3519939.3523704.pdfTest

الإتاحة: https://doi.org/10.1145/3519939.3523704Test
https://inria.hal.science/hal-03777103Test
https://inria.hal.science/hal-03777103/documentTest
https://inria.hal.science/hal-03777103/file/3519939.3523704.pdfTest

المؤلفون: Hesselink, W H

المصدر: Hesselink , W H 2022 , ' Trylock, a case for temporal logic and eternity variables ' , Science of computer programming , vol. 216 , 102767 . https://doi.org/10.1016/j.scico.2021.102767Test

مصطلحات موضوعية: concurrency, locking, CTL, LTL, prophecy variables, simulation

وصف الملف: application/pdf

العلاقة: https://research.rug.nl/en/publications/0ce08589-96de-444a-87e3-46b1ba9bd513Test

الإتاحة: https://doi.org/10.1016/j.scico.2021.102767Test
https://hdl.handle.net/11370/0ce08589-96de-444a-87e3-46b1ba9bd513Test
https://research.rug.nl/en/publications/0ce08589-96de-444a-87e3-46b1ba9bd513Test
https://pure.rug.nl/ws/files/199228210/1_s2.0_S016764232100160X_main.pdfTest

المؤلفون: de Vilhena, Paulo, Emílio, Pottier, François, Jourdan, Jacques-Henri

المساهمون: Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Saclay, ANR-15-CE25-0008,VOCAL,Bibliothèque OCaml vérifiée(2015)

المصدر: ISSN: 2475-1421 ; Proceedings of the ACM on Programming Languages ; https://hal.science/hal-02351562Test ; Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371101⟩ ; https://popl20.sigplan.orgTest/.

مصطلحات موضوعية: Program verification, Separation logic, Least fixed point, Prophecy variables, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF]

العلاقة: hal-02351562; https://hal.science/hal-02351562Test; https://hal.science/hal-02351562/documentTest; https://hal.science/hal-02351562/file/main.pdfTest

الإتاحة: https://doi.org/10.1145/3371101Test
https://hal.science/hal-02351562Test
https://hal.science/hal-02351562/documentTest
https://hal.science/hal-02351562/file/main.pdfTest

المؤلفون: Wim Hesselink

المساهمون: Fundamental Computing Science

المصدر: Science of computer programming, 216:102767. ELSEVIER SCIENCE BV

مصطلحات موضوعية: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, CTL, simulation, concurrency, locking, CTL, LTL, prophecy variables, simulation, concurrency, locking, prophecy variables, Software, LTL

وصف الملف: application/pdf

الوصول الحر: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5bd85fad1dc45cab3cd45eebb1c62e97Test
https://doi.org/10.1016/j.scico.2021.102767Test

المؤلفون: Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer

المساهمون: Tokyo University of Science [Tokyo], Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Max Planck Institute for Software Systems (MPI-SWS), European Project: 683289,H2020,ERC-2015-CoG,RustBelt(2016)

المصدر: PLDI 2022-43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
PLDI 2022-43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2022, San Diego CA USA, United States. pp.841-856, ⟨10.1145/3519939.3523704⟩
PLDI '22

مصطلحات موضوعية: Separation logic, type systems, Type theory Rust, Iris, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], verification, prophecy variables, CCS Concepts: • Theory of computation → Programming logic

وصف الملف: application/pdf

الوصول الحر: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4135a9010341ceb1abf9c622f2d6ff3aTest
https://doi.org/10.1145/3519939.3523704Test

المؤلفون: François Pottier, Jacques-Henri Jourdan, Paulo Emílio de Vilhena

المساهمون: Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Saclay, ANR-15-CE25-0008,VOCAL,Bibliothèque OCaml vérifiée(2015)

المصدر: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371101⟩

مصطلحات موضوعية: Theoretical computer science, Dependency (UML), Correctness, Computer science, Memoization, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], 0102 computer and information sciences, 02 engineering and technology, Separation logic, 01 natural sciences, 0202 electrical engineering, electronic engineering, information engineering, Prophecy variables, Safety, Risk, Reliability and Quality, Logic programming, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Solver, 16. Peace & justice, Least fixed point, [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], Monotone polygon, 010201 computation theory & mathematics, Program verification, Software

الوصول الحر: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1a8f73dced264c8159da15fea52104d9Test
https://hal.archives-ouvertes.fr/hal-02351562/file/main.pdfTest

المؤلفون: Hesselink, Wim H.

المصدر: Hesselink , W H 2005 , ' Eternity Variables to Prove Simulation of Specifications ' , ACM Transactions on Computational Logic , vol. 6 , pp. 175 - 201 .

مصطلحات موضوعية: simulation, refinement mapping, prophecy variables, preservation of quiescence, invariant, implementation, history variables

وصف الملف: application/pdf

العلاقة: https://research.rug.nl/en/publications/19ce7442-7306-48f2-8a94-d946afa8f1d5Test

الإتاحة: https://hdl.handle.net/11370/19ce7442-7306-48f2-8a94-d946afa8f1d5Test
https://research.rug.nl/en/publications/19ce7442-7306-48f2-8a94-d946afa8f1d5Test
https://pure.rug.nl/ws/files/2897512/2005ACMTransCompLogHesselink.pdfTest

المؤلفون: Hesselink, Wim H.

المصدر: Hesselink , W H 2004 , ' Using eternity variables to specify and prove a serializable database interface ' , Science of computer programming , vol. 51 , no. 1-2 , pp. 47-85 . https://doi.org/10.1016/j.scico.2003.06.001Test

مصطلحات موضوعية: scrializability, specification, implementation, history variables, prophecy variables, forward invariant, backward invariant, mechanical verification

وصف الملف: application/pdf

العلاقة: https://research.rug.nl/en/publications/c7123860-d0c3-42e3-8c7b-d8fd2cf5fe85Test

الإتاحة: https://doi.org/10.1016/j.scico.2003.06.001Test
https://hdl.handle.net/11370/c7123860-d0c3-42e3-8c7b-d8fd2cf5fe85Test
https://research.rug.nl/en/publications/c7123860-d0c3-42e3-8c7b-d8fd2cf5fe85Test
https://pure.rug.nl/ws/files/2968057/2004SciCompProgHesselink.pdfTest

المؤلفون: David Griffioen, Frits Vaandrager

المساهمون: The Pennsylvania State University CiteSeerX Archives

المصدر: http://arxiv.org/pdf/cs/0007030v1.pdfTest.

مصطلحات موضوعية: Computer aided verification, normed simulations, automata, refinement mappings, forward simulations, backward simulations, history variables, prophecy variables

وصف الملف: application/pdf

العلاقة: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.342.4970Test; http://arxiv.org/pdf/cs/0007030v1.pdfTest

الإتاحة: http://arxiv.org/pdf/cs/0007030v1.pdfTest

المؤلفون: Wim H. Hesselink, Th May

المساهمون: The Pennsylvania State University CiteSeerX Archives

المصدر: http://www.cs.rug.nl/~wim/pub/whh282a.pdfTest.

مصطلحات موضوعية: serializability, specification, implementation, history variables, prophecy variables

وصف الملف: application/pdf

العلاقة: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.7.4718Test; http://www.cs.rug.nl/~wim/pub/whh282a.pdfTest

الإتاحة: http://www.cs.rug.nl/~wim/pub/whh282a.pdfTest