The workshop aims to bring together researchers working in the field of computer-aided validation, programming languages and verification to discuss the connections and interplay between pre- and post-deployment verification techniques. Examples of the topics covered by the workshop are the relationships between classic model checking and testing on the one hand and runtime verification and statistical model checking on the other, and between type systems that may be checked either statically or dynamically through techniques such as runtime monitoring, gradual typing and contracts. Relevant topics also include the synthesis of runtime adaptation and enforcement mechanisms from correctness specifications, as well as the combination of deductive verification with runtime verification. Contributions related to tools and applications of pre- and post-deployment verification will also be welcome.
| Abstract submission | June 5, 2017 | |
| Paper submission | June 12, 2017 | |
| Notification of acceptance | July 10, 2017 | |
| Camera ready version | July 17, 2017 | |
| Conference iFM 2017 | Sep 20-22, 2016 | |
| Workshop PrePost 2017 | Sep 19, 2017 |
10.00 - 10.30 Coffee break
10:30 - 11:00 Giles Reger. A Story of Parametric Trace Slicing, Garbage and Static Analysis.
11:30 - 11:30 Ian Cassar, Adrian Francalanza, Luca Aceto and Anna Ingolfsdottir. A Survey of Runtime Monitoring Instrumentation Techniques.
11:30 - 12:00 Shaun Azzopardi, Christian Colombo and Gordon J. Pace. Control-Flow Residual Analysis for Symbolic Automata.
12:10 - 13:40 Lunch
13:50 - 14:50 Invited talk: Aldrin Seychell Ixaris. OPE: The Journey to Open Payments, Safely.
14:50 - 15:20 Luke Chircop, Christian Colombo and Mark Micallef. Exploring the Link Between Test Suite Quality and Automatic Specification Inference.
15:20 - 15:50 Coffee break
15:50 - 16:20 Oscar Cornejo, Daniela Briola, Daniela Micucci and Leonardo Mariani. Fragmented Monitoring.
16:20 - 16:50 Ian Cassar, Adrian Francalanza, Claudio Antares Mezzina and Emilio Tuosto. Reliability and Fault-Tolerance by Choreographic Design.
16:50 - 17:00 Closing
We solicit the submission of original and unpublished contributions not under review for publication elsewhere. Contributions are expected to comprise research papers (with novel, previously unpublished results), experience reports of real-world applications, tool descriptions, as well as work-in-progress or exploratory ideas. All papers must be prepared in LaTeX using the EPTCS style.
Additional details omitted due to space limitations may be included in a clearly marked appendix. Submissions must describe work unpublished in refereed venues, not submitted elsewhere. Contributions should be submitted in PDF format through the
>>> EasyChair online submission system <<<
Submission of a paper involves a firm commitment that at least one of the authors will attend and participate in the workshop in case the paper is accepted.All contributions will be evaluated by at least three reviewers, chosen by the Program Committee. The PC will select the best papers based on their quality, relevance to the workshop, and potential to instigate discussion. All accepted papers will be included in the workshop proceedings, which will be published as a volume of the EPTCS series.