09:00-09:15
Opening
09:15-10:00
John Gallagher (Roskilde University, Denmark and IMDEA Software Institute, Spain).
Finite Tree Automata in Horn Clause Transformations.
(slides:
)
(Invited talk)
10:00-10:30
Dániel Horpácsi, Judit Kőszegi and Simon Thompson.
Towards Trustworthy Refactoring in Erlang.
(preprint
,
slides:
,
pptx
)
10:30-11:00
Coffee Break
11:00-11:30
Geoff Hamilton.
Generating Counterexamples for Model Checking by Transformation.
(preprint
,
slides:
)
11:30-12:00
Bishoksan Kafle and John P. Gallagher.
Interpolant Tree Automata and their Application in Horn Clause Verification.
(preprint
,
slides:
)
12:00-12:30
Antonina Nepeivoda.
Turchin's Relation for Call-by-Name Computations: a Formal Approach.
(preprint
,
slides:
)
12:30-14:00
Lunch
14:00-14:45
Igor Walukiewicz (CNRS Bordeaux University, France).
Model Based Approach to Verification of Higher-Order Programs.
(slides:
)
(Invited talk)
14:45-15:15
Amir M. Ben-Amram and Aviad Pineles.
Flowchart Programs, Regular Expressions, and Decidability of Polynomial Growth-Rate.
(preprint
,
slides:
)
15:15-15:45
Coffee Break
15:45-16:15
Gergö Barany.
Hybrid Information Flow Analysis for Programs with Arrays.
(preprint
,
slides:
)
16:15-16:45
Julien Cohen.
Renaming Global Variables in C Mechanically Proved Correct.
(preprint
,
slides:
)
16:45-17:15
Venkatesh Kannan and Geoff Hamilton.
Program Transformation to Identify List-Based Parallel Skeletons.
(preprint
,
slides:
)
17:15-18:00
Discussion and Closing