April 3rd, 2016 · Eindhoven, The Netherlands
|8:55 - 9:00||Welcome|
|9:00 - 10:00||Maurizio Proietti (IASI-CNR, Italy)|
|Invited talk: Transforming Constrained Horn Clauses for Program Verification (slides)|
|10:00 - 10:30||Break|
|10:30 - 11:00||Tewodros A. Beyene, Corneliu Popeea and Andrey Rybalchenko|
|Efficient CTL Verification via Horn Constraints Solving (slides)|
|11:00 - 11:30||Temesghen Kahsai, Xavier Thirioux and Pierre-Loic Garoche|
|Hierarchical state machines as modular Horn clauses|
|11:30 - 12:00||Peter Schrammel|
|Challenges in Decomposing Encodings of Verification Problems (slides)|
|12:00 - 14:00||Lunch break|
|14:00 - 15:00||Tachio Terauchi (Japan Advanced Institute of Science and Technology)|
|Invited talk: On Predicate Refinement Heuristics in Program Verification with CEGAR (slides)|
|15:00 - 15:30||Break|
|15:30 - 16:00||Bishoksan Kafle, John P. Gallagher and Pierre Ganty|
|Solving non-linear Horn clauses using a linear Horn clause solver (slides)|
|16:00 - 16:30||Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti|
|Removing Unnecessary Variables from Horn Verification Conditions (slides)|
|16:30 - 17:00||Gabriele Paganelli|
|Horn Binary Serialization Analysis (slides)|
|17:00 - 18:00||Discussions|
The pdfs of the papers provided here are preliminary and might change in the final post-proceedings of the workshop. Copyright on all papers is retained by the authors.
Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:
We solicit regular papers describing theory and implementation of Horn-clause based analysis and tool descriptions. We also solicit extended abstracts describing work-in-progress, as well as presentations covering previously published results that are of interest to the workshop.
|Paper submission:||February 1, 2016 EXTENDED to February 5, 2016|
|Paper notification:||February 27, 2016|
|Early registration:||March 1, 2016|
|Workshop:||April 3, 2016|
All submitted papers will be refereed by the program committee and will be selected for inclusion in accordance with the referee reports. Accepted regular papers and extended abstracts will be published electronically as a volume in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series, see http://www.eptcs.org/.
Authors of accepted papers are required to ensure that at least one of them will be present at the workshop.
Papers must be submitted through the EasyChair system using the web page: https://www.easychair.org/conferences/?conf=hcvs2016