Difference between revisions of "Publications"

Latest revision as of 12:01, 6 September 2017

ref

[1]	Andrew Reynolds, Radu Iosif, and Cristina Serban. Reasoning in the bernays-schönfinkel-ramsey fragment of separation logic. In Proceedings of VMCAI'17, Paris, France, January 15-17, volume 10145 of LNCS, pages 462--482. Springer, 2017. [ bib ]
[2]	Radu Iosif and Xiao Xu. The impact of alternation. CoRR, abs/1705.05606, 2017. [ bib \| http ]
[3]	Radu Iosif and Cristina Serban. Complete cyclic proof systems for inductive entailments. CoRR, abs/1707.02415, 2017. [ bib \| http ]
[4]	Radu Iosif and Arnaud Sangnier. How hard is it to verify flat affine counter systems with the finite monoid property? In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, pages 89--105, 2016. [ bib ]
[5]	Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King. A decision procedure for separation logic in SMT. In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, pages 244--261, 2016. [ bib ]
[6]	Claire Dross and Yannick Moy. Auto-active proof of red-black trees in SPARK. In Proceedings of NFM, volume 10227 of LNAI, pages 68--83. Springer, 2017. [ bib ]
[7]	Raphaël Cauderlier and Catherine Dubois. FoCaLiZe and Dedukti to the rescue for proof interoperability. In Proceedigns of ITP'17, Brasilia, Bresil, September 26-29, 2017. Proceedings, number 10499 in LNAI. Springer, 2017. [ bib ]
[8]	Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. Compositional entailment checking for a fragment of separation logic. Form Methods Syst Des, 2017. [ bib \| DOI ]
[9]	Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. SPEN: A solver for separation logic. In Proceedings of NFM, volume 10227 of Lecture Notes in Computer Science, pages 302--309, 2017. [ bib \| DOI \| http ]
[10]	Bin Fang and Mihaela Sighireanu. A refinement hierarchy for free list memory allocators. In Proceedings of ISMM, pages 104--114. ACM, 2017. [ bib \| DOI \| http ]
[11]	Bin Fang and Mihaela Sighireanu. Hierarchical shape abstraction for analysis of free-list memory allocators. In LOPSTR, volume 10184 of Lecture Notes in Computer Science. Springer, 2016. [ bib ]
[12]	Michael Emmi and Constantin Enea. Symbolic abstract data type inference. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 513--525. ACM, 2016. [ bib \| http ]
[13]	Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. On automated lemma generation for separation logic with inductive definitions. In Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, volume 9364 of Lecture Notes in Computer Science, pages 80--96. Springer, 2015. [ bib \| DOI \| http ]
[14]	Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. On reducing linearizability to state reachability. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 95--107. Springer, 2015. [ bib \| DOI \| http ]
[15]	Michael Emmi, Constantin Enea, and Jad Hamza. Monitoring refinement via symbolic reasoning. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 260--269. ACM, 2015. [ bib \| DOI \| http ]
[16]	Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. Compositional entailment checking for a fragment of separation logic. In Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, pages 314--333, 2014. [ bib \| DOI \| http ]
[17]	Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. Deciding entailments in inductive separation logic with tree automata. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, pages 201--218, 2014. [ bib \| DOI \| http ]
[18]	Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. Abstraction refinement and antichains for trace inclusion of infinite state systems. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 71--89, 2016. [ bib ]
[19]	Claire Dross and Yannick Moy. Abstract software specifications and automatic proof of refinement. In 1st International Conference on Reliability, Safety and Security of Railway Systems (RSSR), 2016. [ bib ]
[20]	Sandrine Blazy, David Bühler, and Boris Yakobowski. Improving static analyses of C programs with conditional predicates. Science of Computer Programming, January 2016. Accepted manuscript. Available online 30 November 2015.Extended version of the FMICS 2014 paper. [ bib \| http ]
[21]	Mihaela Sighireanu and David R. Cok. Report on sl-comp 2014. Journal on Satisfiability, Boolean Modeling and Computation, 2014. [ bib ]
[22]	Sandrine Blazy, David Bühler, and Boris Yakobowski. Structuring abstract interpreters through state and value abstractions. In Ahmed Bouajjani and David Monniaux, editors, Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, volume 10145 of Lecture Notes in Computer Science, pages 112--130. Springer, 2017. [ bib \| DOI \| http ]

This file was generated by bibtex2html 1.98.

Difference between revisions of "Publications"

Latest revision as of 12:01, 6 September 2017

Navigation menu

Personal tools

Namespaces

Variants

Views

More

Search

Navigation

Tools

@@ Line 12: / Line 12: @@
       (see http://www.lri.fr/~filliatr/bibtex2html/),
       with the following command:
-      /usr/bin/bibtex2html ref.bib  -->
+      bibtex2html ref.bib  -->
@@ Line 19: / Line 19: @@
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="DBLP:conf/atva/EneaSW15">1</a>]
+[<a name="DBLP:conf/vmcai/ReynoldsIS17">1</a>]
+</td>
+<td class="bibtexitem">
+Andrew Reynolds, Radu Iosif, and Cristina Serban.
+ Reasoning in the bernays-sch&ouml;nfinkel-ramsey fragment of
+  separation logic.
+ In <em>Proceedings of VMCAI'17, Paris, France, January 15-17</em>,
+  volume 10145 of <em>LNCS</em>, pages 462--482. Springer, 2017.
+[&nbsp;<a href="ref_bib.html#DBLP:conf/vmcai/ReynoldsIS17">bib</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:journals/corr/IosifX17">2</a>]
+</td>
+<td class="bibtexitem">
+Radu Iosif and Xiao Xu.
+ The impact of alternation.
+ <em>CoRR</em>, abs/1705.05606, 2017.
+[&nbsp;<a href="ref_bib.html#DBLP:journals/corr/IosifX17">bib</a>&nbsp;|
+<a href="http://arxiv.org/abs/1705.05606">http</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:journals/corr/IosifS17">3</a>]
+</td>
+<td class="bibtexitem">
+Radu Iosif and Cristina Serban.
+ Complete cyclic proof systems for inductive entailments.
+ <em>CoRR</em>, abs/1707.02415, 2017.
+[&nbsp;<a href="ref_bib.html#DBLP:journals/corr/IosifS17">bib</a>&nbsp;|
+<a href="http://arxiv.org/abs/1707.02415">http</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:conf/atva/IosifS16">4</a>]
+</td>
+<td class="bibtexitem">
+Radu Iosif and Arnaud Sangnier.
+ How hard is it to verify flat affine counter systems with the finite
+  monoid property?
+ In <em>Automated Technology for Verification and Analysis - 14th
+  International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016,
+  Proceedings</em>, pages 89--105, 2016.
+[&nbsp;<a href="ref_bib.html#DBLP:conf/atva/IosifS16">bib</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:conf/atva/ReynoldsIS016">5</a>]
+</td>
+<td class="bibtexitem">
+Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King.
+ A decision procedure for separation logic in SMT.
+ In <em>Automated Technology for Verification and Analysis - 14th
+  International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016,
+  Proceedings</em>, pages 244--261, 2016.
+[&nbsp;<a href="ref_bib.html#DBLP:conf/atva/ReynoldsIS016">bib</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:conf/nfm/DrossM17">6</a>]
+</td>
+<td class="bibtexitem">
+Claire Dross and Yannick Moy.
+ Auto-active proof of red-black trees in SPARK.
+ In <em>Proceedings of NFM</em>, volume 10227 of <em>LNAI</em>, pages
+--83. Springer, 2017.
+[&nbsp;<a href="ref_bib.html#DBLP:conf/nfm/DrossM17">bib</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="ITP17Interop">7</a>]
+</td>
+<td class="bibtexitem">
+Rapha&euml;l Cauderlier and Catherine Dubois.
+ FoCaLiZe and Dedukti to the rescue for proof interoperability.
+ In <em>Proceedigns of ITP'17, Brasilia, Bresil, September 26-29,
+. Proceedings</em>, number 10499 in LNAI. Springer, 2017.
+[&nbsp;<a href="ref_bib.html#ITP17Interop">bib</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="EneaLSV17">8</a>]
+</td>
+<td class="bibtexitem">
+Constantin Enea, Ondrej Leng&aacute;l, Mihaela Sighireanu, and Tom&aacute;s
+  Vojnar.
+ Compositional entailment checking for a fragment of separation logic.
+ <em>Form Methods Syst Des</em>, 2017.
+[&nbsp;<a href="ref_bib.html#EneaLSV17">bib</a>&nbsp;|
+<a href="http://dx.doi.org/10.1007/s10703-017-0289-4">DOI</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:conf/nfm/EneaLSV17">9</a>]
+</td>
+<td class="bibtexitem">
+Constantin Enea, Ondrej Leng&aacute;l, Mihaela Sighireanu, and Tom&aacute;s
+  Vojnar.
+ SPEN: A solver for separation logic.
+ In <em>Proceedings of NFM</em>, volume 10227 of <em>Lecture Notes in
+  Computer Science</em>, pages 302--309, 2017.
+[&nbsp;<a href="ref_bib.html#DBLP:conf/nfm/EneaLSV17">bib</a>&nbsp;|
+<a href="http://dx.doi.org/10.1007/978-3-319-57288-8_22">DOI</a>&nbsp;|
+<a href="https://doi.org/10.1007/978-3-319-57288-8_22">http</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:conf/iwmm/FangS17">10</a>]
+</td>
+<td class="bibtexitem">
+Bin Fang and Mihaela Sighireanu.
+ A refinement hierarchy for free list memory allocators.
+ In <em>Proceedings of ISMM</em>, pages 104--114. ACM, 2017.
+[&nbsp;<a href="ref_bib.html#DBLP:conf/iwmm/FangS17">bib</a>&nbsp;|
+<a href="http://dx.doi.org/10.1145/3092255.3092275">DOI</a>&nbsp;|
+<a href="http://doi.acm.org/10.1145/3092255.3092275">http</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="FangS16">11</a>]
+</td>
+<td class="bibtexitem">
+Bin Fang and Mihaela Sighireanu.
+ Hierarchical shape abstraction for analysis of free-list memory
+  allocators.
+ In <em>LOPSTR</em>, volume 10184 of <em>Lecture Notes in Computer
+  Science</em>. Springer, 2016.
+[&nbsp;<a href="ref_bib.html#FangS16">bib</a>&nbsp;]
+<blockquote><font size="-1">
+</font></blockquote>
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:conf/popl/EmmiE16">12</a>]
+</td>
+<td class="bibtexitem">
+Michael Emmi and Constantin Enea.
+ Symbolic abstract data type inference.
+ In <em>Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT
+  Symposium on Principles of Programming Languages, POPL 2016, St.
+  Petersburg, FL, USA, January 20 - 22, 2016</em>, pages 513--525. ACM, 2016.
+[&nbsp;<a href="ref_bib.html#DBLP:conf/popl/EmmiE16">bib</a>&nbsp;|
+<a href="http://doi.acm.org/10.1145/2837614.2837645">http</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:conf/atva/EneaSW15">13</a>]
 </td>
 <td class="bibtexitem">
@@ Line 39: / Line 233: @@
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="DBLP:conf/icalp/BouajjaniEEH15">2</a>]
+[<a name="DBLP:conf/icalp/BouajjaniEEH15">14</a>]
 </td>
 <td class="bibtexitem">
@@ Line 58: / Line 252: @@
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="DBLP:conf/pldi/EmmiEH15">3</a>]
+[<a name="DBLP:conf/pldi/EmmiEH15">15</a>]
 </td>
 <td class="bibtexitem">
@@ Line 76: / Line 270: @@
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="DBLP:conf/aplas/EneaLSV14">4</a>]
+[<a name="DBLP:conf/aplas/EneaLSV14">16</a>]
 </td>
 <td class="bibtexitem">
@@ Line 95: / Line 289: @@
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="DBLP:conf/atva/IosifRV14">5</a>]
+[<a name="DBLP:conf/atva/IosifRV14">17</a>]
 </td>
 <td class="bibtexitem">
@@ Line 114: / Line 308: @@
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="DBLP:conf/tacas/IosifRV16">6</a>]
+[<a name="DBLP:conf/tacas/IosifRV16">18</a>]
 </td>
 <td class="bibtexitem">
@@ Line 133: / Line 327: @@
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="dross2016rssr">7</a>]
+[<a name="dross2016rssr">19</a>]
 </td>
 <td class="bibtexitem">
@@ Line 148: / Line 342: @@
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="DBLP:journals/corr/ReynoldsI016">8</a>]
+[<a name="blazy:hal-01242077">20</a>]
-</td>
-<td class="bibtexitem">
-Andrew Reynolds, Radu Iosif, and Tim King.
- A decision procedure for separation logic in SMT.
- <em>CoRR</em>, abs/1603.06844, 2016.
-[&nbsp;<a href="ref_bib.html#DBLP:journals/corr/ReynoldsI016">bib</a>&nbsp;|
-<a href="http://arxiv.org/abs/1603.06844">http</a>&nbsp;]
-</td>
-</tr>
-<tr valign="top">
-<td align="right" class="bibtexnumber">
-[<a name="blazy:hal-01242077">9</a>]
 </td>
 <td class="bibtexitem">
@@ Line 174: / Line 353: @@
 [&nbsp;<a href="ref_bib.html#blazy:hal-01242077">bib</a>&nbsp;|
 <a href="https://hal.inria.fr/hal-01242077">http</a>&nbsp;]
+<blockquote><font size="-1">
+</font></blockquote>
 </td>
+</tr>
 <tr valign="top">
 <td align="right" class="bibtexnumber">
-[<a name="SighireanuC14">10</a>]
+[<a name="SighireanuC14">21</a>]
 </td>
 <td class="bibtexitem">
@@ Line 187: / Line 371: @@
 [&nbsp;<a href="ref_bib.html#SighireanuC14">bib</a>&nbsp;]
+</td>
+</tr>
+<tr valign="top">
+<td align="right" class="bibtexnumber">
+[<a name="DBLP:conf/vmcai/BlazyBY17">22</a>]
+</td>
+<td class="bibtexitem">
+Sandrine Blazy, David B&uuml;hler, and Boris Yakobowski.
+ Structuring abstract interpreters through state and value
+  abstractions.
+ In Ahmed Bouajjani and David Monniaux, editors, <em>Verification,
+  Model Checking, and Abstract Interpretation - 18th International Conference,
+  VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings</em>, volume 10145
+  of <em>Lecture Notes in Computer Science</em>, pages 112--130. Springer, 2017.
+[&nbsp;<a href="ref_bib.html#DBLP:conf/vmcai/BlazyBY17">bib</a>&nbsp;|
+<a href="http://dx.doi.org/10.1007/978-3-319-52234-0_7">DOI</a>&nbsp;|
+<a href="https://doi.org/10.1007/978-3-319-52234-0_7">http</a>&nbsp;]
+</td>
 </tr>
 </table><hr><p><em>This file was generated by
 <a href="http://www.lri.fr/~filliatr/bibtex2html/">bibtex2html</a> 1.98.</em></p>
 </body>
 </html>