Automated Techniques for Higher-Order Program Verification

Icon

Shonan Meeting Seminar 005

Overview

With the increasing importance of software reliability, program
verification has been an important and hot research topic.  Recently,
we have seen some good progress in automated techniques for
verification of higher-order programs. Studies of game semantics have
yielded compositional model checkers and automated program equivalence
checkers for Algol-like programming languages, and studies of
higher-order recursion schemes and pushdown automata have yielded
model checkers for higher-order functional programs. Classical control
flow analysis has been recently revisited to yield more precise and/or
efficient methods than Shivers’ k-CFA.

The aim of the workshop is to bring together researchers on automated
techniques for higher-order program verification and analyses, and
provide them with an opportunity to exchange new research results, and
discuss further extensions. The workshop also aims for
cross-fertilization of different techniques for higher-order program
verification, such as game semantics, type theories, higher-order
grammars and pushdown systems, control flow analyses, and abstract
interpretation.

To participants: please leave your comments here.

Schedule

See also the tentative technical program.

All the technical sessions take place in R209 of Research Wing.

22nd September (Thursday)

15:00 — Hotel Check In (early check-in from 12:00 is negotiable if informed in advance)
19:00 — 21:00: Welcome Reception (Room “Azalea”, 1F)

23rd September (Friday)

7:30 — 9:00: Breakfast (Oak room)
9:45 — 10:00: Welcome and Introduction
10:00 — 12:00: Morning Session
12:00 — 13:30: Lunch (Oak room)
13:30 — 18:00: Afternoon Session
18:00 — 19:30: Dinner (Oak room)
19:30 — Free Time

24th September (Saturday)

7:30 — 9:00: Breakfast (Oak room)
9:00 — 12:00: Morning Session
12:00 — 13:30: Lunch (Oak room)
13:30 — 18:00: Afternoon Session
18:00 — 19:30: Dinner (Oak room)
19:30 — Free Time

25th September (Sunday)

7:30 — 9:00: Breakfast (Oak room)
9:00 — 12:00: Morning Session
12:00-12:15: group photo
12:15 — 13:30: Lunch (Oak room)
13:30 — 18:00: Excursion (Kamakura tour)
18:00 — 19:30: Banquet (Japanese restaurant “Hachinoki”)

26th September (Monday)

7:30 — 9:00: Breakfast (Oak room)
9:00 — 12:00: Morning Session
11:30 — 13:30: Lunch (Oak room)
13:30 — 17:00: Afternoon Session
17:00 — 17:10: Closing
18:00–19:30: Dinner (Oak room, only for those who stay for the night)

27th September (Tuesday)
7:30 — 9:00: Breakfast (Oak room)
9:00 — 10:00 Hotel Check Out

Participants

Fritz Henglein                (University of Copenhagen)
Kazuhiro Inaba              (Google)
Suresh Jagannathan     (Purdue University)
Thomas Jensen               (INRIA)
Ranjit Jhala                      (University of California, San Diego)
Neil D. Jones                    (University of Cophenhagen)
Jean-Pierre Jouannaud     (LIX, Ecole Polytechnique)
Naoki Kobayashi            (Tohoku University)
Martin Lester                   (University of Oxford)
Jan Midtgaard                 (Aarhus University)
Matthew Might               (University of Utah)
Yasuhiko Minamide     (University of Tsukuba)
Andrzej Murawski         (University of Leicester)
Keisuke Nakano             (University of Electro-Communications)
Robin Neatherway       (University of Oxford)
Luke Ong                           (University of Oxford)
Luca Paolini                    (Università di Torino)
Steven Ramsay              (University of Oxford)
Tachio Terauchi             (Nagoya University)
Akihiko Tozawa            (IBM Research, Tokyo)
Takeshi Tsukada           (Tohoku University)
Nikos Tzevelekos          (University of Oxford)
Hiroshi Unno                  (Tohoku University)
David Van Horn              (Northeastern University)
Dimitrios Vardoulakis     (Northeastern University)

Organizer

Naoki Kobayashi        (Tohoku University)
Luke Ong                   (University of Oxford)
David Van Horn          (Northeastern University)

Transportation and Local Information

Accommodation:

Please note that the entrance of Shonan Village Center is closed between 11:00pm — 7:00am. Prior arrangement is required to enter the center after 11:00pm.

You can make the reservation online. You should have received a reservation  instruction from Shonan Village Center.

Access to Shonan Village:

See Shonan Village Home Page

There are several routes from Tokyo area or Narita airport. In general, first move by a train to  either Zushi (JR) or Shin-Zushi (Keikyu), and then take a bus or a taxi. For foreigners, we would recommend sharing a  taxi from Zushi or Shin-Zushi. The train route/schedule can be searched by using the train route finder below.

Train Schedule Search (not for reservation) :

  • Jordan Train Route Finder
  • For destination, enter “Zushi” or “Shin-Zushi”.  As Tokyo area is served by several companies, you will see several choices. Please pick one that seems most convenient. An optimal route depends on the departure time.

  • Narita Airport Access Planner
  • You can search a train schedule from/to Narita Airport.

Recommended routes from Tokyo/Airports to Zushi:

Note: The following may not be the best route, depending on the time of departure.

  • From Tokyo Narita Airport
  • Take JR Narita Express to go to “Ofuna” or “Yokohama”, and then take JR Yokosuka Line to Zushi.

  • From Tokyo Haneda Airport
  • Take Keikyu Haneda Airport Line. Change at Keikyu Kamata station to Keikyu Line, and then change at Kanazawa-Hakkei to Keikyu Zushi Line and get off at Shin-Zushi terminal.

  • From Tokyo Jimbocho area (where ICFP is held)
    • Go to Tokyo station by a taxi (which costs around 1,500 yen) and then take JR Yokosuka Line to Zushi.
    • Go to Shibuya station by Tokyo Metro, and then take JR Shonan-Shinjuku Line.

From Zushi or Shin-Zushi to Shonan Village Center

    At Zushi station, go out from “East Exit”.
    Please take a bus (which leaves once in an hour or half an hour, and takes 30 min from Zushi to Shonan Village Center) or a taxi, which costs 2,500 — 3,000 yen and takes about 20 min.
    As a bus driver is not likely to speak English, we recommend sharing a taxi (or finding a company who speaks Japanese, to take a bus). Here are some Japanese messages to show to a taxi driver.

     

  • Bus Time Table
  • The bus leaves from Bus Stop #1 of the east exit of JR Zushi station, and costs 340 yen.
    There are buses that leave from #1 and  go to other destination. So, make sure that the final destination of the bus is “Shonan Kokusai-mura Center” (the distination sign is in Japanese  but it comes with number “16″ or “26″; if you are not sure, please ask the driver or other passengers before boarding), and get off at the final stop. Shonan Village Center is on the righthand side of the bus stop.

Other Links on Travel Information:

About Earthquake and Radiation:

ICFP page summarizes the recent situation around Tokyo after the big earthquake.
In eastern part of Japan, the frequency of small earthquakes is a bit higher than usual (though no devastating one has happened since the big one). You need not worry too much, but if you have never experienced even a small earthquake, you may wish to check this page, just in case (in the same sense that you should know how to evacuate in case of a fire accident even if the chance to encounter the accident is very small).

Links