Publications

[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.