BliStrTune: Hierarchical Invention of Theorem Proving Strategies (CPP 2017) - POPL 2017

Sun 15 - Sat 21 January 2017

Who

Jan Jakubuv, Josef Urban

Track

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown here reflect the offsets at this moment. These offsets update automatically in case there is a change in daylight saving time.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Mon 16 Jan 2017 14:00 - 14:30 at Auditorium - Automated proof and its verification

Jan Jakubuv

Josef Urban

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown here reflect the offsets at this moment. These offsets update automatically in case there is a change in daylight saving time.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

	14:00 - 15:30: Automated proof and its verificationCPP at Auditorium

	14:00 - 14:30 Talk		BliStrTune: Hierarchical Invention of Theorem Proving Strategies CPP Jan Jakubuv, Josef Urban
	14:30 - 15:00 Talk		Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic CPP Reuben RoweUniversity College London, James Brotherston
	15:00 - 15:30 Talk		Formalization of Karp-Miller Tree Construction on Petri Nets CPP Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto