Difference between revisions of "Publications"

From vecolib
Jump to: navigation, search
 
(9 intermediate revisions by the same user not shown)
Line 3: Line 3:
 
<head>
 
<head>
 
<title>ref</title>
 
<title>ref</title>
 +
<meta http-equiv="content-type" content="text/html; charset=ANSI_X3.4-1968">
 +
<meta name="generator" content="bibtex2html">
 
</head>
 
</head>
  
 
<body>
 
<body>
  
−
<body>
+
<!-- This document was automatically generated with bibtex2html 1.98
−
 
+
     (see http://www.lri.fr/~filliatr/bibtex2html/),
−
<!-- This document was automatically generated with bibtex2html 1.98                                    
+
     with the following command:
−
     (see http://www.lri.fr/~filliatr/bibtex2html/),                                                    
+
     bibtex2html ref.bib  -->
−
     with the following command:                                                                        
+
−
     /usr/bin/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="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
 +
  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 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>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
Line 25: Line 219:
 
  On automated lemma generation for separation logic with inductive
 
  On automated lemma generation for separation logic with inductive
 
   definitions.
 
   definitions.
−
  In <em>Automated Technology for Verification and Analysis - 13th                                      
+
  In <em>Automated Technology for Verification and Analysis - 13th
−
   International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015,                            
+
   International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015,
 
   Proceedings</em>, volume 9364 of <em>Lecture Notes in Computer Science</em>, pages
 
   Proceedings</em>, volume 9364 of <em>Lecture Notes in Computer Science</em>, pages
 
   80--96. Springer, 2015.
 
   80--96. Springer, 2015.
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/atva/EneaSW15">bib</a>&nbsp;|
+
[&nbsp;<a href="ref_bib.html#DBLP:conf/atva/EneaSW15">bib</a>&nbsp;|  
−
<a href="http://dx.doi.org/10.1007/978-3-319-24953-7_7">DOI</a>&nbsp;|
+
<a href="http://dx.doi.org/10.1007/978-3-319-24953-7_7">DOI</a>&nbsp;|  
 
<a href="http://dx.doi.org/10.1007/978-3-319-24953-7_7">http</a>&nbsp;]
 
<a href="http://dx.doi.org/10.1007/978-3-319-24953-7_7">http</a>&nbsp;]
  
 
</td>
 
</td>
 
</tr>
 
</tr>
 +
  
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/icalp/BouajjaniEEH15">2</a>]
+
[<a name="DBLP:conf/icalp/BouajjaniEEH15">14</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
Line 47: Line 242:
 
   II</em>, volume 9135 of <em>Lecture Notes in Computer Science</em>, pages 95--107.
 
   II</em>, volume 9135 of <em>Lecture Notes in Computer Science</em>, pages 95--107.
 
   Springer, 2015.
 
   Springer, 2015.
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/icalp/BouajjaniEEH15">bib</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;|
+
<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;]
 
<a href="http://dx.doi.org/10.1007/978-3-662-47666-6_8">http</a>&nbsp;]
  
 
</td>
 
</td>
 
</tr>
 
</tr>
 +
  
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/pldi/EmmiEH15">3</a>]
+
[<a name="DBLP:conf/pldi/EmmiEH15">15</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
 
Michael Emmi, Constantin Enea, and Jad Hamza.
 
Michael Emmi, Constantin Enea, and Jad Hamza.
 
  Monitoring refinement via symbolic reasoning.
 
  Monitoring refinement via symbolic reasoning.
−
  In <em>Proceedings of the 36th ACM SIGPLAN Conference on                                              
+
  In <em>Proceedings of the 36th ACM SIGPLAN Conference on
−
   Programming Language Design and Implementation, Portland, OR, USA, June                              
+
   Programming Language Design and Implementation, Portland, OR, USA, June
 
   15-17, 2015</em>, pages 260--269. ACM, 2015.
 
   15-17, 2015</em>, pages 260--269. ACM, 2015.
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/pldi/EmmiEH15">bib</a>&nbsp;|
+
[&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://dx.doi.org/10.1145/2737924.2737983">DOI</a>&nbsp;|  
 
<a href="http://doi.acm.org/10.1145/2737924.2737983">http</a>&nbsp;]
 
<a href="http://doi.acm.org/10.1145/2737924.2737983">http</a>&nbsp;]
  
 
</td>
 
</td>
 
</tr>
 
</tr>
 +
  
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/aplas/EneaLSV14">4</a>]
+
[<a name="DBLP:conf/aplas/EneaLSV14">16</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
Line 79: Line 276:
 
   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,                                      
+
  In <em>Programming Languages and Systems - 12th Asian Symposium,
 
   APLAS 2014, Singapore, November 17-19, 2014, Proceedings</em>, pages 314--333,
 
   APLAS 2014, Singapore, November 17-19, 2014, Proceedings</em>, pages 314--333,
 
   2014.
 
   2014.
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/aplas/EneaLSV14">bib</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">DOI</a>&nbsp;|  
 
<a href="http://dx.doi.org/10.1007/978-3-319-12736-1_17">http</a>&nbsp;]
 
<a href="http://dx.doi.org/10.1007/978-3-319-12736-1_17">http</a>&nbsp;]
  
 
</td>
 
</td>
 
</tr>
 
</tr>
 +
  
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:conf/atva/IosifRV14">5</a>]
+
[<a name="DBLP:conf/atva/IosifRV14">17</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
Line 97: Line 295:
 
  Deciding entailments in inductive separation logic with tree
 
  Deciding entailments in inductive separation logic with tree
 
   automata.
 
   automata.
−
  In <em>Automated Technology for Verification and Analysis - 12th                                      
+
  In <em>Automated Technology for Verification and Analysis - 12th
−
   International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7,                            
+
   International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7,
 
   2014, Proceedings</em>, pages 201--218, 2014.
 
   2014, Proceedings</em>, pages 201--218, 2014.
−
[&nbsp;<a href="ref_bib.html#DBLP:conf/atva/IosifRV14">bib</a>&nbsp;|
+
[&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">DOI</a>&nbsp;|  
 
<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_15">http</a>&nbsp;]
 
<a href="http://dx.doi.org/10.1007/978-3-319-11936-6_15">http</a>&nbsp;]
  
 
</td>
 
</td>
 
</tr>
 
</tr>
 +
  
 
<tr valign="top">
 
<tr valign="top">
 
<td align="right" class="bibtexnumber">
 
<td align="right" class="bibtexnumber">
−
[<a name="DBLP:journals/corr/IosifRV14a">6</a>]
+
[<a name="DBLP:conf/tacas/IosifRV16">18</a>]
 
</td>
 
</td>
 
<td class="bibtexitem">
 
<td class="bibtexitem">
 
Radu Iosif, Adam Rogalewicz, and Tom&aacute;s Vojnar.
 
Radu Iosif, Adam Rogalewicz, and Tom&aacute;s Vojnar.
−
  Abstraction refinement for trace inclusion of data automata.
+
  Abstraction refinement and antichains for trace inclusion of infinite
−
  <em>CoRR</em>, abs/1410.5056, 2014.
+
  state systems.
−
[&nbsp;<a href="ref_bib.html#DBLP:journals/corr/IosifRV14a">bib</a>&nbsp;|
+
  In <em>Tools and Algorithms for the Construction and Analysis of
−
<a href="http://arxiv.org/abs/1410.5056">http</a>&nbsp;]
+
  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</em>, pages 71--89,
 +
  2016.
 +
[&nbsp;<a href="ref_bib.html#DBLP:conf/tacas/IosifRV16">bib</a>&nbsp;]
 +
 
 +
</td>
 +
</tr>
 +
 
 +
 
 +
<tr valign="top">
 +
<td align="right" class="bibtexnumber">
 +
[<a name="dross2016rssr">19</a>]
 +
</td>
 +
<td class="bibtexitem">
 +
Claire Dross and Yannick Moy.
 +
Abstract software specifications and automatic proof of refinement.
 +
In <em>1st International Conference on Reliability, Safety and
 +
  Security of Railway Systems (RSSR)</em>, 2016.
 +
[&nbsp;<a href="ref_bib.html#dross2016rssr">bib</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">
 +
</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>

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.

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