September 1st September 10
- Notification September 26
- Final version
October 1st October 7
October 1st October 7
- Workshop October 24-26
Topics of interest include, but are not limited to:
- semantics of programming languages
- programming language design and programming methodology
- programming logics
- formal specification of programs
- program verification
- program construction
- tools for program verification and construction
- program transformation and refinement
- real-time and hybrid systems
- models of concurrency and distributed computing
- language-based security
Authors wishing to give a talk at the workshop are requested to submit abstracts of 2-3 pages (pdf, printable on A4 paper, using easychair.cls) through EasyChair. Work in progress as well as abstracts of manuscripts submitted for formal publication elsewhere are permitted.
As with earlier NWPT workshops, we have arranged a special issue of the Journal of Logical and Algebraic Methods in Programming (JLAMP) devoted to the best contributions to the workshop. The contributions will be selected by the PC. They will be invited after the workshop and will undergo a rigorous, journal-strength review process according to the standards of JLAMP.
We are pleased to have three invited speakers for NWPT’18.
Erika Ábrahám RWTH Aachen University, Germany
Title: Symbolic Computation Techniques in SMT Solving:
Mathematical Beauty meets Efficient Heuristics
Checking the satisfiability of quantifier-free real-arithmetic formulas is a practically highly relevant but computationally hard problem. Some beautiful mathematical decision procedures implemented in computer algebra systems are capable of solving such problems, however, they were developed for more general tasks like quantifier elimination, therefore their applicability to satisfiability checking is often restricted. In computer science, recent advances in satisfiability-modulo-theories (SMT) solving led to elegant embeddings of such decision procedures in SMT solvers in a way that combines the strengths of symbolic computation methods and heuristic-driven search techniques. In this talk we discuss such embeddings and show that they might be quite challenging but can lead to powerful synergies and open new lines of research.
Andrei Sabelfeld Chalmers University, Sweden
Title: Breaking and Fixing IoT Apps: from Attacks to Formal Methods for Security
IoT apps empower users by connecting a variety of otherwise unconnected services. Unfortunately, the power of IoT apps can be abused by malicious makers, unnoticeably to users. We demonstrate that popular IoT app platforms are susceptible to several classes of attacks that violate user privacy, integrity, and availability. We estimate the impact of these attacks by an empirical study. We suggest short/medium-term countermeasures based on fine-grained access control and long-term countermeasures based on information flow tracking. Finally, we discuss general trends and challenges for the Web of Things and, in particular, the role of formal methods in securing it.
Parts of the talk are based on joint work with Iulia Bastys and Musard Balliu.
Peter Ölveczky University of Oslo, Norway
Title: Design and Validation of Cloud Storage Systems using Rewriting Logic
To deal with large amounts of data while offering high availability and throughput and low latency, cloud computing systems rely on distributed, partitioned, and replicated data stores. Such cloud storage systems are complex software artifacts that are very hard to design and analyze. We argue that formal specification and model checking should be beneficial during their design and validation. In particular, I propose rewriting logic and its accompanying Maude tools as a suitable framework for formally specifying and analyzing both the correctness and the performance of cloud storage systems. This talk gives an overview of the use of rewriting logic at the University of Illinois’ Assured Cloud Computing center on industrial data stores such as Google’s Megastore and Facebook/Apache’s Cassandra. I also briefly summarize the experiences of the use of a different formal method for similar purposes by engineers at Amazon Web Services.
Here is the program in PDF.
The workshops registration fee is 250€, and it covers:
- Lunches and refreshments for Wednesday, Thursday and Friday
- Welcome reception on Wednesday evening
- Conference dinner on Thursday evening
Click here to register for the workshop.
Oslo is served by the Gardermoen Oslo Airport (OSL). From the airport, you can get to the city center via the Airport express train (Flytoget) or the Norwegian State Rails (NSB). NSB is cheaper than Flytoget, but not as frequent.
For getting around town see Ruter, the transit authority that oversees public transportation via buses, metro (T-banen), trams (trikken), and ferry. Local taxi firms include Oslo Taxi (+47 22 38 8090) and Christiania Taxi (+47 22 57 80 00).
You will need to book your accommodation independently. Most bookings can be made online. See VisitOslo for a selection of options. An inexpensive option is Cochs Pensjonat, near the royal castle. You may also consider booking a small apartment with Frogner House Apartments, Oslo Apartments or Airbnb. We are looking at arranging pre-booked rooms.
The workshop will be held at room Faros on the 5th floor of the Oslo Science Park (Forskningsparken), next to the University of Oslo Informatics building.
We will have a reception with tapas on the 5th floor of the Ole-Johan Dahl’s building. The building is right across from the conference center. The reception is on Wednesday, October 24, at 17:30.
On Thursday, October 25, at 18:30, we will have the workshop dinner at Ekeberg Restaurant.
- Lars Birkedal, Aarhus Univ., Denmark
- Johannes Borgström, Uppsala Univ., Sweden
- Daniel S. Fava, Univ. of Oslo, Norway
- John Gallagher, RUC, Denmark
- Michael R. Hansen, DTU, Denmark
- Magne Haveraaen, Univ. of Bergen, Norway
- Keijo Heljanko, Aalto Univ., Finland
- Fritz Henglein, Univ. of Copenhagen, Denmark
- Thomas T. Hildebrandt, ITU, Denmark
- Anna Ingólfsdóttir, Reykjavík Univ., Iceland
- Einar Broch Johnsen, Univ. of Oslo, Norway
- Jaakko Järvi, Univ. of Bergen, Norway
- Yngve Lamo, Bergen Univ. Col., Norway
- Kim G. Larsen, Aalborg Univ., Denmark
- Alberto Lluch Lafuente, DTU, Denmark
- Fabrizio Montesi, Univ. of Southern Denmark, Denmark
- Wojciech Mostowski, Halmstad Univ., Sweden
- Olaf Owe, Univ. of Oslo, Norway
- Philipp Rümmer, Uppsala Univ., Sweden
- Gerardo Schneider, University of Gothenburg, Sweden
- Cristina Seceleanu, Mälardalen Univ., Sweden
- Jiri Srba, Aalborg Univ., Denmark
- Tarmo Uustalu, Reykjavík Univ., Iceland
- Jüri Vain, Tallinn Univ. of Tech., Estonia
- Antti Valmari, University of Jyväskylä, Finland
- Marina Waldén, Åbo Akademi Univ., Finland
Recent previous years
- Turku, Finland, 2017
- North Jutland, Denmark, 2016
- Reykjavík, Iceland, 2015
- Halmstad, Sweden, 2014
- Tallinn, Estonia, 2013
- Bergen, Norway, 2012
- Västerås, Sweden, 2011
- Turku, Finland, 2010
- Lyngby, Denmark, 2009
- Tallinn, Estonia, 2008
Further information at email@example.com