Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

local.bib 5.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
@Misc{mcas,
  author =    {Nicolas Assouad and KC Sivaramakrishnan},
  title =     {Multi-word compare-and-swap},
  year="2017",
  URL={https://github.com/ocaml-multicore/kcas},
}

@Misc{lockfree,
  author =    {Nicolas Assouad and KC Sivaramakrishnan},
  title =     {Lock-free data structures},
  month=apr,
  year="2017",
  URL={https://github.com/ocaml-multicore/lockfree},
}

@Misc{reagents,
  author =    {Nicolas Assouad and KC Sivaramakrishnan},
  title =     {Reagents},
  month=apr,
  year="2016",
  URL={https://github.com/ocaml-multicore/reagents},
}

Glen Mével's avatar
Glen Mével committed
24
25
26
27
28
29
30
@Misc{iris-examples,
  author =    {{Iris developers and contributors}},
  title =     {Iris examples},
  year="2021",
  URL={https://gitlab.mpi-sws.org/iris/examples},
}

31
32
33
34
35
36
@Misc{jung-slides-2019,
  author =    {Ralf Jung},
  title =     {Logical Atomicity in Iris: the Good, the Bad, and the Ugly},
  howpublished = {Iris Workshop},
  month =     oct,
  year =      2019,
POTTIER Francois's avatar
URL.    
POTTIER Francois committed
37
  URL={https://people.mpi-sws.org/~jung/iris/talk-iris2019.pdf},
38
39
40
41
}

@Misc{repo,
  author =    {Glen Mével and Jacques-Henri Jourdan and François Pottier},
Glen Mével's avatar
Glen Mével committed
42
  title =     {Coq proofs for Cosmo and examples},
43
  howpublished = {\url{https://gitlab.inria.fr/gmevel/cosmo}},
Glen Mével's avatar
Glen Mével committed
44
  year =      "2021",
45
}
Jacques-Henri Jourdan's avatar
Intro    
Jacques-Henri Jourdan committed
46
47
48
49
50
51
52

@inproceedings{da2014tada,
  title={TaDA: A logic for time and data abstraction},
  author={da Rocha Pinto, Pedro and Dinsdale-Young, Thomas and Gardner, Philippa},
  booktitle={European Conference on Object-Oriented Programming},
  pages={207--231},
  year={2014},
53
54
  organization={Springer},
  doi={10.1007/978-3-662-44202-9_9}
Jacques-Henri Jourdan's avatar
Intro    
Jacques-Henri Jourdan committed
55
}
POTTIER Francois's avatar
POTTIER Francois committed
56
57
58
59
60
61
62
63
64

@Unpublished{vindum-frumin-birkedal-21,
  author =       {Simon Friis Vindum and Dan Frumin and Lars Birkedal},
  title={Mechanized Verification of a Fine-Grained Concurrent Queue from Facebook's Folly Library},
  note =         {Submitted for publication},
  month =     mar,
  year =      2021,
  note =    {\url{https://cs.au.dk/~birke/papers/mpmc-queue.pdf}},
}
65
66
67
68
69
70
71

@Misc{rigtorp,
  author =    {Erik Rigtorp},
  title =     {MPMCQueue},
  month =     mar,
  year =      2021,
  note =      {\url{https://github.com/rigtorp/MPMCQueue}}}
72
73
74
75
76
77
78


@inproceedings{frumin2018reloc,
  title={ReLoC: A mechanised relational logic for fine-grained concurrency},
  author={Frumin, Dan and Krebbers, Robbert and Birkedal, Lars},
  booktitle={Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
  pages={442--451},
79
80
  year={2018},
  doi={10.1145/3209108.3209174}
81
82
83
84
85
86
87
88
89
90
91
92
93
94
}

@article{frumin2020reloc,
  title={ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity},
  author={Frumin, Dan and Krebbers, Robbert and Birkedal, Lars},
  journal={arXiv preprint arXiv:2006.13635},
  year={2020}
}

@inproceedings{jacobs2011expressive,
  title={Expressive modular fine-grained concurrency specification},
  author={Jacobs, Bart and Piessens, Frank},
  booktitle={Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={271--282},
95
96
  year={2011},
  doi={10.1145/1926385.1926417}
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
}

@inproceedings{le2013correctws,
  title={Correct and efficient work-stealing for weak memory models},
  author={L{\^e}, Nhat Minh and Pop, Antoniu and Cohen, Albert and Zappa Nardelli, Francesco},
  booktitle={Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of parallel programming},
  pages={69--80},
  year={2013}
}

@inproceedings{le2013correctfifo,
  title={Correct and efficient bounded FIFO queues},
  author={L{\^e}, Nhat Minh and Guatto, Adrien and Cohen, Albert and Pop, Antoniu},
  booktitle={2013 25th International Symposium on Computer Architecture and High Performance Computing},
  pages={144--151},
  year={2013},
  organization={IEEE}
}

@inproceedings{lahav2015owicki,
  title={Owicki-Gries reasoning for weak memory models},
  author={Lahav, Ori and Vafeiadis, Viktor},
  booktitle={International Colloquium on Automata, Languages, and Programming},
  pages={311--323},
  year={2015},
122
123
  organization={Springer},
  doi={10.1007/978-3-662-47666-6_25}
124
125
126
127
128
129
130
131
132
133
}

@article{dongol2015verifying,
  title={Verifying linearisability: A comparative survey},
  author={Dongol, Brijesh and Derrick, John},
  journal={ACM Computing Surveys (CSUR)},
  volume={48},
  number={2},
  pages={1--43},
  year={2015},
134
135
  publisher={ACM},
  doi={10.1145/2796550}
136
}
Jacques-Henri Jourdan's avatar
Misc    
Jacques-Henri Jourdan committed
137

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
138
@article{gueneau2021theorems,
Jacques-Henri Jourdan's avatar
Misc    
Jacques-Henri Jourdan committed
139
  title={Theorems for Free from Separation Logic Specifications},
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
140
141
142
143
  author={Birkedal, Lars and Dinsdale-Young, Thomas and Guéneau, Armaël and Jaber, Guilhem and Svendsen, Kasper and Tzevelekos, Nikos},
  journal      = pacmpl,
  volume = "5",
  number = "ICFP",
144
  year={2021},
145
  url={https://cs.au.dk/~birke/papers/free-theorems-sep-logic.pdf}
146
147
148
149
150
151
152
153
154
}

@inproceedings{zakowski2018verified,
  title={Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement},
  author={Zakowski, Yannick and Cachera, David and Demange, Delphine and Pichardie, David},
  booktitle={Proceedings of the 33rd Annual ACM Symposium on Applied Computing},
  pages={1881--1890},
  year={2018}
}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
155
156
157
158
159
160
161
162
163

@article{smith2019linearizability,
  title={Linearizability on hardware weak memory models},
  author={Smith, Graeme and Winter, Kirsten and Colvin, Robert J},
  journal={Formal Aspects of Computing},
  pages={1--32},
  year={2019},
  publisher={Springer}
}
Glen Mével's avatar
Glen Mével committed
164
165
166
167
168
169
170
171
172
173
174

@inproceedings{timany2021monotonicity,
  author = {Timany, Amin and Birkedal, Lars},
  title = {Reasoning about Monotonicity in Separation Logic},
  booktitle = {Certified Programs and Proofs (CPP)},
  month= jan,
  year = {2021},
  pages = {91–104},
  url = {https://cs.au.dk/~timany/publications/files/2021_CPP_monotone.pdf}
}

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
175
176
177
178
@techreport{fraser2004practical,
  title={Practical lock-freedom},
  author={Fraser, Keir},
  year={2004},
179
180
  institution={University of Cambridge, Computer Laboratory},
  doi={}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
181
}