09:00-09:15
Opening
09:15-10:00
Arie Gurfinkel (Software Engineering Institute, Carnegie Mellon University, USA).
The SeaHorn Verification Framework.
(slides:
,
pptx
)
(Invited talk)
10:00-10:30
Martin Lester.
Control Flow Analysis for SF Combinator Calculus.
(preprint
,
slides:
)
10:30-11:00
Coffee Break
11:00-11:30
Bishoksan Kafle, John P. Gallagher and Pierre Ganty.
Decomposition by Tree Dimension in Horn Clause Verification.
(preprint
,
slides:
)
11:30-12:00
G.W. Hamilton.
Verifying Temporal Properties of Reactive Systems by Transformation.
(preprint
,
slides:
)
12:00-12:30
Discussion.
12:30-14:00
Lunch
14:00-14:45
David Monniaux (VERIMAG, CNRS - University of Grenoble, France).
Program Transformation and Verification are Interrelated.
(slides:
)
(Invited talk)
14:45-15:15
Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti.
Proving Horn Clause Specifications of Imperative Programs.
(preprint
,
slides:
)
15:15-15:45
Wei Bai and Emmanuel M. Tadjouddine.
Automated Program Translation in Certifying Online Auctions.
(preprint
)
15:45-16:00
Discussion.
16:00-16:30
Coffee Break
16:30-17:00
Alexei P. Lisitsa and Andrei P. Nemytykh.
Finite Countermodel Based Verification for Program Transformation (A Case Study).
(preprint
,
slides:
)
17:00-17:20
Sebastian Schlesinger, Paula Herber, Thomas Gothel and Sabine Glesner.
Towards the Verification of Refactorings of Hybrid Simulink Models.
(Presentation, preprint
,
slides:
)
17:20-17:40
Fouad ben Nasr Omri, Safa Omri and Ralf Reussner.
Incremental and Compositional Probabilistic Analysis of Programs under Uncertainty.
(Presentation, preprint
)
17:40-18:00
Discussion.