Difference between revisions of "Publications"

From vecolib
Jump to: navigation, search
Line 12: Line 12:
 
     (see http://www.lri.fr/~filliatr/bibtex2html/),
 
     (see http://www.lri.fr/~filliatr/bibtex2html/),
 
     with the following command:
 
     with the following command:
−
     /usr/bin/bibtex2html -d ref.bib  -->
+
     bibtex2html ref.bib  -->
  
  
Line 19: Line 19:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="SighireanuC14">1</a>]
+
[<a name="DBLP:conf/vmcai/ReynoldsIS17">1</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
−
Mihaela Sighireanu and David&nbsp;R. Cok.
+
Andrew Reynolds, Radu Iosif, and Cristina Serban.
−
  Report on sl-comp 2014.
+
  Reasoning in the bernays-sch&ouml;nfinkel-ramsey fragment of
−
  <em>Journal on Satisfiability, Boolean Modeling and Computation</em>,
+
  separation logic.
−
   2014.
+
  In <em>Proceedings of VMCAI'17, Paris, France, January 15-17</em>,
−
[&nbsp;<a href="ref_bib.html#SighireanuC14">bib</a>&nbsp;]
+
   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>
 
</td>
Line 34: Line 35:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/atva/IosifRV14">2</a>]
+
[<a name="DBLP:journals/corr/IosifX17">2</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
−
Radu Iosif, Adam Rogalewicz, and Tom&aacute;s Vojnar.
+
Radu Iosif and Xiao Xu.
−
  Deciding entailments in inductive separation logic with tree
+
  The impact of alternation.
−
  automata.
+
  <em>CoRR</em>, abs/1705.05606, 2017.
−
  In <em>Automated Technology for Verification and Analysis - 12th
+
[&nbsp;<a href="ref_bib.html#DBLP:journals/corr/IosifX17">bib</a>&nbsp;|  
−
  International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7,
+
<a href="http://arxiv.org/abs/1705.05606">http</a>&nbsp;]
−
  2014, Proceedings</em>, pages 201--218, 2014.
+
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/atva/IosifRV14">bib</a>&nbsp;|  
+
−
<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_15">DOI</a>&nbsp;|
+
−
<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_15">http</a>&nbsp;]
+
  
 
</td>
 
</td>
Line 53: Line 50:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/aplas/EneaLSV14">3</a>]
+
[<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
 +
  68--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,
 +
  2017. 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>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
Line 59: Line 134:
 
   Vojnar.
 
   Vojnar.
 
  Compositional entailment checking for a fragment of separation logic.
 
  Compositional entailment checking for a fragment of separation logic.
−
  In <em>Programming Languages and Systems - 12th Asian Symposium,
+
  <em>Form Methods Syst Des</em>, 2017.
−
  APLAS 2014, Singapore, November 17-19, 2014, Proceedings</em>, pages 314--333,
+
[&nbsp;<a href="ref_bib.html#EneaLSV17">bib</a>&nbsp;|  
−
  2014.
+
<a href="http://dx.doi.org/10.1007/s10703-017-0289-4">DOI</a>&nbsp;]
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/aplas/EneaLSV14">bib</a>&nbsp;|  
+
−
<a href="http://dx.doi.org/10.1007/978-3-319-12736-1_17">DOI</a>&nbsp;|
+
−
<a href="http://dx.doi.org/10.1007/978-3-319-12736-1_17">http</a>&nbsp;]
+
  
 
</td>
 
</td>
Line 72: Line 144:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/pldi/EmmiEH15">4</a>]
+
[<a name="DBLP:conf/nfm/EneaLSV17">9</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
−
Michael Emmi, Constantin Enea, and Jad Hamza.
+
Constantin Enea, Ondrej Leng&aacute;l, Mihaela Sighireanu, and Tom&aacute;s
−
  Monitoring refinement via symbolic reasoning.
+
  Vojnar.
−
  In <em>Proceedings of the 36th ACM SIGPLAN Conference on
+
  SPEN: A solver for separation logic.
−
  Programming Language Design and Implementation, Portland, OR, USA, June
+
  In <em>Proceedings of NFM</em>, volume 10227 of <em>Lecture Notes in
−
   15-17, 2015</em>, pages 260--269. ACM, 2015.
+
   Computer Science</em>, pages 302--309, 2017.
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/pldi/EmmiEH15">bib</a>&nbsp;|  
+
[&nbsp;<a href="ref_bib.html#DBLP:conf/nfm/EneaLSV17">bib</a>&nbsp;|  
−
<a href="http://dx.doi.org/10.1145/2737924.2737983">DOI</a>&nbsp;|  
+
<a href="http://dx.doi.org/10.1007/978-3-319-57288-8_22">DOI</a>&nbsp;|  
−
<a href="http://doi.acm.org/10.1145/2737924.2737983">http</a>&nbsp;]
+
<a href="https://doi.org/10.1007/978-3-319-57288-8_22">http</a>&nbsp;]
  
 
</td>
 
</td>
Line 90: Line 162:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/icalp/BouajjaniEEH15">5</a>]
+
[<a name="DBLP:conf/iwmm/FangS17">10</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
−
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza.
+
Bin Fang and Mihaela Sighireanu.
−
  On reducing linearizability to state reachability.
+
  A refinement hierarchy for free list memory allocators.
−
  In <em>Automata, Languages, and Programming - 42nd International
+
  In <em>Proceedings of ISMM</em>, pages 104--114. ACM, 2017.
−
  Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part
+
[&nbsp;<a href="ref_bib.html#DBLP:conf/iwmm/FangS17">bib</a>&nbsp;|
−
   II</em>, volume 9135 of <em>Lecture Notes in Computer Science</em>, pages 95--107.
+
<a href="http://dx.doi.org/10.1145/3092255.3092275">DOI</a>&nbsp;|
−
  Springer, 2015.
+
<a href="http://doi.acm.org/10.1145/3092255.3092275">http</a>&nbsp;]
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/icalp/BouajjaniEEH15">bib</a>&nbsp;|
+
 
−
<a href="http://dx.doi.org/10.1007/978-3-662-47666-6_8">DOI</a>&nbsp;|  
+
</td>
−
<a href="http://dx.doi.org/10.1007/978-3-662-47666-6_8">http</a>&nbsp;]
+
</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">
 +
Keywords: iconf,nodblp
 +
</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>
 
</td>
Line 109: Line 214:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/atva/EneaSW15">6</a>]
+
[<a name="DBLP:conf/atva/EneaSW15">13</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
Line 129: Line 234:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="blazy:hal-01242077">7</a>]
+
[<a name="DBLP:conf/icalp/BouajjaniEEH15">14</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
−
Sandrine Blazy, David B&uuml;hler, and Boris Yakobowski.
+
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza.
−
  Improving static analyses of C programs with conditional
+
  On reducing linearizability to state reachability.
−
  predicates.
+
  In <em>Automata, Languages, and Programming - 42nd International
−
  <em>Science of Computer Programming</em>, January 2016.
+
  Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part
−
Accepted manuscript. Available online 30 November 2015.Extended
+
  II</em>, volume 9135 of <em>Lecture Notes in Computer Science</em>, pages 95--107.
−
  version of the FMICS 2014 paper.
+
  Springer, 2015.
−
[&nbsp;<a href="ref_bib.html#blazy:hal-01242077">bib</a>&nbsp;|  
+
[&nbsp;<a href="ref_bib.html#DBLP:conf/icalp/BouajjaniEEH15">bib</a>&nbsp;|  
−
<a href="https://hal.inria.fr/hal-01242077">http</a>&nbsp;]
+
<a href="http://dx.doi.org/10.1007/978-3-662-47666-6_8">DOI</a>&nbsp;|
 +
<a href="http://dx.doi.org/10.1007/978-3-662-47666-6_8">http</a>&nbsp;]
  
 
</td>
 
</td>
Line 147: Line 253:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:journals/corr/ReynoldsI016">8</a>]
+
[<a name="DBLP:conf/pldi/EmmiEH15">15</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
−
Andrew Reynolds, Radu Iosif, and Tim King.
+
Michael Emmi, Constantin Enea, and Jad Hamza.
−
  A decision procedure for separation logic in SMT.
+
  Monitoring refinement via symbolic reasoning.
−
  <em>CoRR</em>, abs/1603.06844, 2016.
+
  In <em>Proceedings of the 36th ACM SIGPLAN Conference on
−
[&nbsp;<a href="ref_bib.html#DBLP:journals/corr/ReynoldsI016">bib</a>&nbsp;|  
+
  Programming Language Design and Implementation, Portland, OR, USA, June
−
<a href="http://arxiv.org/abs/1603.06844">http</a>&nbsp;]
+
  15-17, 2015</em>, pages 260--269. ACM, 2015.
 +
[&nbsp;<a href="ref_bib.html#DBLP:conf/pldi/EmmiEH15">bib</a>&nbsp;|  
 +
<a href="http://dx.doi.org/10.1145/2737924.2737983">DOI</a>&nbsp;|
 +
<a href="http://doi.acm.org/10.1145/2737924.2737983">http</a>&nbsp;]
  
 
</td>
 
</td>
Line 162: Line 271:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="dross2016rssr">9</a>]
+
[<a name="DBLP:conf/aplas/EneaLSV14">16</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
−
Claire Dross and Yannick Moy.
+
Constantin Enea, Ondrej Leng&aacute;l, Mihaela Sighireanu, and Tom&aacute;s
−
  Abstract software specifications and automatic proof of refinement.
+
  Vojnar.
−
  In <em>1st International Conference on Reliability, Safety and
+
  Compositional entailment checking for a fragment of separation logic.
−
   Security of Railway Systems (RSSR)</em>, 2016.
+
  In <em>Programming Languages and Systems - 12th Asian Symposium,
−
[&nbsp;<a href="ref_bib.html#dross2016rssr">bib</a>&nbsp;]
+
  APLAS 2014, Singapore, November 17-19, 2014, Proceedings</em>, pages 314--333,
 +
  2014.
 +
[&nbsp;<a href="ref_bib.html#DBLP:conf/aplas/EneaLSV14">bib</a>&nbsp;|
 +
<a href="http://dx.doi.org/10.1007/978-3-319-12736-1_17">DOI</a>&nbsp;|
 +
<a href="http://dx.doi.org/10.1007/978-3-319-12736-1_17">http</a>&nbsp;]
 +
 
 +
</td>
 +
</tr>
 +
 
 +
 
 +
<tr valign="top">
 +
<td align="right" class="bibtexnumber">
 +
[<a name="DBLP:conf/atva/IosifRV14">17</a>]
 +
</td>
 +
<td class="bibtexitem">
 +
Radu Iosif, Adam Rogalewicz, and Tom&aacute;s Vojnar.
 +
Deciding entailments in inductive separation logic with tree
 +
   automata.
 +
In <em>Automated Technology for Verification and Analysis - 12th
 +
  International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7,
 +
  2014, Proceedings</em>, pages 201--218, 2014.
 +
[&nbsp;<a href="ref_bib.html#DBLP:conf/atva/IosifRV14">bib</a>&nbsp;|
 +
<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_15">DOI</a>&nbsp;|
 +
<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_15">http</a>&nbsp;]
  
 
</td>
 
</td>
Line 177: Line 309:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/tacas/IosifRV16">10</a>]
+
[<a name="DBLP:conf/tacas/IosifRV16">18</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
Line 196: Line 328:
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/popl/EmmiE16">11</a>]
+
[<a name="dross2016rssr">19</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
−
Michael Emmi and Constantin Enea.
+
Claire Dross and Yannick Moy.
−
  Symbolic abstract data type inference.
+
  Abstract software specifications and automatic proof of refinement.
−
  In <em>Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT
+
  In <em>1st International Conference on Reliability, Safety and
−
   Symposium on Principles of Programming Languages, POPL 2016, St.
+
  Security of Railway Systems (RSSR)</em>, 2016.
−
   Petersburg, FL, USA, January 20 - 22, 2016</em>, pages 513--525. ACM, 2016.
+
[&nbsp;<a href="ref_bib.html#dross2016rssr">bib</a>&nbsp;]
−
[&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="blazy:hal-01242077">20</a>]
 +
</td>
 +
<td class="bibtexitem">
 +
Sandrine Blazy, David B&uuml;hler, and Boris Yakobowski.
 +
Improving static analyses of C programs with conditional
 +
   predicates.
 +
<em>Science of Computer Programming</em>, January 2016.
 +
Accepted manuscript. Available online 30 November 2015.Extended
 +
  version of the FMICS 2014 paper.
 +
[&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">
 +
Keywords: Static analysis ;  Abstract interpretation ;  Dataflow analysis ;  Path sensitivity
 +
</font></blockquote>
 +
 
 +
</td>
 +
</tr>
 +
 
 +
 
 +
<tr valign="top">
 +
<td align="right" class="bibtexnumber">
 +
[<a name="SighireanuC14">21</a>]
 +
</td>
 +
<td class="bibtexitem">
 +
Mihaela Sighireanu and David&nbsp;R. Cok.
 +
Report on sl-comp 2014.
 +
<em>Journal on Satisfiability, Boolean Modeling and Computation</em>,
 +
  2014.
 +
[&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>
 
</td>
Line 211: Line 397:
 
</table><hr><p><em>This file was generated by
 
</table><hr><p><em>This file was generated by
 
<a href="http://www.lri.fr/~filliatr/bibtex2html/">bibtex2html</a> 1.98.</em></p>
 
<a href="http://www.lri.fr/~filliatr/bibtex2html/">bibtex2html</a> 1.98.</em></p>
 +
 
</body>
 
</body>
 
</html>
 
</html>

Revision as of 12:00, 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 ]
Keywords: iconf,nodblp
[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 ]
Keywords: Static analysis ; Abstract interpretation ; Dataflow analysis ; Path sensitivity
[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.

Retrieved from "http://vecolib.imag.fr/index.php?title=Publications&oldid=10405"