Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
tallinn12 [2012/03/09 23:38] keijo.heljanko |
tallinn12 [2014/05/07 22:48] (current) vkuncak |
||
---|---|---|---|
Line 8: | Line 8: | ||
additional invited talks, contributed talks from IC0901 Action participants, and informal technical discussion session and our usual MC meeting on 1st of April 2012. | additional invited talks, contributed talks from IC0901 Action participants, and informal technical discussion session and our usual MC meeting on 1st of April 2012. | ||
- | **Speakers will include, among others: Jean-Christophe Filliātre, Jasmin Blanchette, Chad E. Brown, Serdar Tasiran** | + | ===== Venue ===== |
+ | |||
+ | Campus of the Tallinn University of Technology, the building of the Tallinn School of Economics and Business Administration, Akadeemia tee 3. | ||
+ | |||
+ | ===== Organizers ===== | ||
+ | |||
+ | [[http://users.ics.tkk.fi/~kepa|Keijo Heljanko]] and [[http://yquem.inria.fr/~herbelin/index-eng.html|Hugo Herbelin]] are the program organizers. [[http://cs.ioc.ee/~tarmo/|Tarmo Uustalu]] and [[http://ati.ttu.ee/~jaan/|Jaan Raik]] as local organizers on behalf of the IC0901 Action. | ||
- | COST Management Committee Meeting will start on Sunday, April 1st, at **11:00** (NOTE THE TIME CHANGE) | + | ====== Program ====== |
- | ===== Call for Technical Contributions ===== | + | {{:tallinn.pdf|Archived PDF Page}}; original link: [[http://pauillac.inria.fr/~herbelin/aipa2012/program.html|Link to the AIPA+SVARM joint program page |
+ | ]] | ||
+ | |||
+ | ====== Registration ===== | ||
+ | |||
+ | The **invited IC0901 participants** will be required to register and pay 40 Euros for two lunches | ||
+ | and coffees by **9th of March 2012** through a Web based payment system provided by the local organizers: | ||
+ | |||
+ | [[https://purchase.ioc.ee/svarm12/|SVARM12 Electronic Payment of Lunch Fees]] | ||
+ | |||
+ | These fees can be later claimed from COST as lunch fees. | ||
+ | For the invited IC0901 participants there will be no other registration fees, and **NO need to register | ||
+ | to AIPA2012 through the ETAPS2012 system** for the two Workshop days. | ||
+ | |||
+ | The participants who are **NOT invited IC0901 participants should register to AIPA2012 | ||
+ | Workshop through the ETAPS2012 registration**, and pay the ETAPS fees for the two Workshop days. | ||
+ | |||
+ | |||
+ | ===== (EXPIRED) Call for Technical Contributions ===== | ||
We are planning to have a program including: | We are planning to have a program including: | ||
Line 50: | Line 74: | ||
(This deadline is for finalizing the technical program; COST invitations | (This deadline is for finalizing the technical program; COST invitations | ||
are generated automatically for MC members and you'll receive one sooner.) | are generated automatically for MC members and you'll receive one sooner.) | ||
- | |||
- | ===== Registration ===== | ||
- | |||
- | The **invited IC0901 participants** will be required to register and pay 40 Euros for two lunches | ||
- | and coffees by **9th of March 2012** through a Web based payment system provided by the local organizers: | ||
- | |||
- | [[https://purchase.ioc.ee/svarm12/|SVARM12 Electronic Payment of Lunch Fees]] | ||
- | |||
- | These fees can be later claimed from COST as lunch fees. | ||
- | For the invited IC0901 participants there will be no other registration fees, and **NO need to register | ||
- | to AIPA2012 through the ETAPS2012 system** for the two Workshop days. | ||
- | |||
- | The participants who are **NOT invited IC0901 participants should register to AIPA2012 | ||
- | Workshop through the ETAPS2012 registration**, and pay the ETAPS fees for the two Workshop days. | ||
- | |||
- | ===== Venue ===== | ||
- | |||
- | Campus of the Tallinn University of Technology, the building of the Tallinn School of Economics and Business Administration, Akadeemia tee 3. | ||
- | |||
- | ===== Program ===== | ||
- | |||
- | Preliminary Program | ||
- | |||
- | |||
- | ** Sat 31.3 AIPA+SVARM ** | ||
- | |||
- | * 9:00- 9:30 Philip Ruemmer (Software Verification Using k-Induction) | ||
- | * 9:30-10:00 Cesar Sanchez (A Decision Procedure for Skiplists with Unbounded Height and Length) | ||
- | * 10:00-10:30 Maria Paola Bonacina (Interpolation for resolution, superposition and DPLL(Gamma+T)) | ||
- | |||
- | * 10:30-11:00 coffee | ||
- | |||
- | * 11:00-12:00 Jean-Christophe Filliâtre (Combining Interactive and Automated Theorem Proving in Why3) [invited talk] | ||
- | * 12:00-12:30 Jesper Bengtson (A framework for higher-order separation logic in Coq) | ||
- | |||
- | * 12:30-14:00 lunch | ||
- | |||
- | * 14:00-15:00 Jasmin Blanchette (Sharing the Burden of (Dis)proof with Nitpick, Quickcheck, and Sledgehammer) [invited talk] | ||
- | * 15:00-15:30 Corneliu Popeea (Synthesizing Software Verifiers from Proof Rules) | ||
- | |||
- | * 15:30-16:00 coffee | ||
- | |||
- | * 16:00-16:30 Tuomas Launiainen (Building a modern concolic tester) | ||
- | * 16:30-17:00 Predrag Janicic (Automated Synthesis of Geometric Construction Procedures) | ||
- | * 17:00-17:30 Fu Song (Efficient CTL Model-Checking for Pushdown Systems) | ||
- | |||
- | |||
- | ** Sun 1.4 SVARM ** | ||
- | |||
- | * 9:00-10:00 Chad E. Brown (Using Satallax to Generate Proof Terms for Conjectures in Coq) [invited talk] | ||
- | * 10:00-10:30 Jasmin Blanchette (TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism) | ||
- | |||
- | * 10:30-11:00 coffee | ||
- | |||
- | * 11:00-12:30 **COST action IC0901 Management Committee meeting** | ||
- | |||
- | * 12:30-14:00 lunch | ||
- | |||
- | * 14:00-15:00 Serdar Tasiran (Generalizing Reduction and Abstraction to Simplify Concurrent Programs: The QED Approach) [invited talk] | ||
- | * 15:00-15:30 Jean-Francois Raskin (Strategy synthesis for quantitative games) | ||
- | |||
- | * 15:30-16:00 coffee | ||
- | |||
- | * 16:00-16:30 Stefan Ratschan (Physical/Software Systems and their Formal Safety Verification) | ||
- | * 16:30-17:00 Julian Samborski-Forlese (Translation of RLTL into Buchi Automata) | ||
- | |||
- | |||
- | ** Sun 1.4 AIPA ** | ||
- | |||
- | * 9:00-10:00 Chad E. Brown (Using Satallax to Generate Proof Terms for Conjectures in Coq) [invited talk] | ||
- | * 10:00-10:30 Jasmin Blanchette (TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism) | ||
- | |||
- | * 10:30-11:00 coffee | ||
- | |||
- | * 11:00-12:30 break for COST people to attend action meeting | ||
- | |||
- | * 12:30-14:00 lunch | ||
- | |||
- | * 14:00-14:30 Rob Arthan (Now f is continuous (exercise!)) | ||
- | * 14:30-15:00 David Pereira (Deciding Regular Expression (In-)Equivalence in Coq) | ||
- | * 15:00-15:30 Claudio Sacerdoti (Unification in the Matita ITP) | ||
- | |||
- | * 15:30-16:00 coffee | ||
- | |||
- | * 16:00-16:30 Pierre Boutillier (Heterogeneous-equality-free compilation of dependent pattern-matching) | ||
- | |||
- | |||
- | ====== Organizers ====== | ||
- | |||
- | [[http://users.ics.tkk.fi/~kepa|Keijo Heljanko]] and [[http://yquem.inria.fr/~herbelin/index-eng.html|Hugo Herbelin]] are the program organizers and [[http://cs.ioc.ee/~tarmo/|Tarmo Uustalu]] and [[http://ati.ttu.ee/~jaan/|Jaan Raik]] as local organizers on behalf of the IC0901 Action. | ||