Schedule of talks for the AIPA workshop and SVARM meeting
The program of the AIPA workshop
and
SVARM meeting is
shared on Saturday 31 March and on the first session of Sunday 1 April
Recent changes (25/3/12): Sacerdoti's talk on Sunday 15:00 moved to Saturday 17:30.
Saturday 31 March, joint AIPA and SVARM program
9:00- 9:30 Alastair F. Donaldson, Leopold Haller, Daniel Kroening,
Philipp Rümmer Software Verification Using k-Induction [
abstract]
9:30-10:00
Alejandro Sánchez, César Sánchez
A Decision Procedure for Skiplists with Unbounded Height and Length [
abstract]
10:00-10:30
Maria Paola Bonacina, Moa Johansson
Interpolation for resolution, superposition and DPLL(Gamma+T) [
abstract]
11:00-12:00
Jean-Christophe Filliâtre Combining Interactive and Automated Theorem Proving in Why3 (invited talk) [
abstract]
12:00-12:30
Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal
A framework for higher-order separation logic in Coq [
abstract]
14:00-15:00
Jasmin Blanchette Sharing the Burden of (Dis)proof with Nitpick, Quickcheck, and Sledgehammer (invited talk) [
abstract]
15:00-15:30 Sergey Grebenshchikov, Nuno Lopes,
Corneliu Popeea, Andrey Rybalchenko
Synthesizing Software Verifiers from Proof Rules [
abstract]
16:00-16:30 Keijo Heljanko, Kari Kähkönen,
Tuomas Launiainen Building a modern concolic tester [
abstract]
16:30-17:00
Predrag Janicic, Vesna Marinkovic
Automated Synthesis of Geometric Construction Procedures [
abstract]
17:00-17:30
Fu Song, Tayssir Touili
Efficient CTL Model-Checking for Pushdown Systems [
abstract]
17:30-18:00
Claudio Sacerdoti, Enrico Tassi
Unification in the Matita ITP [
abstract]
Sunday 1 April, AIPA program (first session is joint with SVARM)
9:00-10:00
Chad E. Brown Using Satallax to Generate Proof Terms for Conjectures in Coq (invited talk) [
abstract]
10:00-10:30
Jasmin Blanchette, Andrei Paskevich
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism [
abstract]
14:00-14:30
Rob Arthan Now f is continuous (exercise!) [
abstract]
14:30-15:00 Nelma Moreira,
David Pereira, Simão Melo de Sousa
Deciding Regular Expression (In-)Equivalence in Coq [
abstract]
15:00-15:30
Pierre Boutillier A dependent pattern matching compiler that preserves programmers' intuition [
abstract]
Sun 1 April, SVARM program (first session is joint with AIPA)
9:00-10:00
Chad E. Brown Using Satallax to Generate Proof Terms for Conjectures in Coq (invited talk) [
abstract]
10:00-10:30
Jasmin Blanchette, Andrei Paskevich
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism [
abstract]
14:00-15:00
Serdar Tasiran Generalizing Reduction and Abstraction to Simplify Concurrent Programs: The QED Approach (invited talk) [
abstract]
15:00-15:30
Jean-Francois Raskin Strategy synthesis for quantitative games
16:00-16:30
Stefan Ratschan Physical/Software Systems and their Formal Safety Verification [
abstract]
16:30-17:00
Julian Samborski-Forlese Translation of RLTL into Buchi Automata [
abstract]