Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Next revision Both sides next revision
tallinn12 [2012/01/19 21:39]
keijo.heljanko 		tallinn12 [2012/03/10 14:57]
vkuncak
Line 1: Line 1:
-====== Richmodel Toolkit COST Action Meeting in Tallinn, 2012 ======+====== Richmodel Toolkit COST Action Meeting in Tallinn ​(SVARM ​2012) ======
  
 Meeting of the [[http://​richmodels.epfl.ch|Rich Model Toolkit]] COST Action IC0901, is organized in Tallinn, Estonia, ​ Meeting of the [[http://​richmodels.epfl.ch|Rich Model Toolkit]] COST Action IC0901, is organized in Tallinn, Estonia, ​
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.
  
-The program includes invited talks (speakers to be announced).+===== Venue =====
  
 +Campus of the Tallinn University of Technology, the building of the Tallinn School of Economics and Business Administration,​ Akadeemia tee 3. 
  
-===== Registration =====+===== 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. 
 + 
 +====== 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) 
 + 
 +====== Registration =====
  
 The **invited IC0901 participants** will be required to register and pay 40 Euros for two lunches The **invited IC0901 participants** will be required to register and pay 40 Euros for two lunches
-through a Web based payment system ​(details will be provided ​here later). These fees can be later claimed +and coffees by **9th of March 2012** ​through a Web based payment system provided ​by the local organizers:​ 
-from COST as lunch fees.+ 
 +[[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 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. to AIPA2012 through the ETAPS2012 system** for the two Workshop days.
Line 23: Line 95:
  
  
-====== Organizers ======+===== (EXPIRED) Call for Technical Contributions ​===== 
 + 
 +We are planning to have a program including:​ 
 +  * contributed talks from Action participants 
 +  * invited talks from: Chad E. Brown, Jean-Christophe Filliâtre, Jasmin Blanchette, and Serdar Tasiran 
 +  * informal technical discussion sessions 
 +  * our usual MC meeting 
 + 
 +An informal technical discussion session is meant to be an opportunity 
 +to bring up and discuss a topic that is important for our research 
 +area, and perceived to be key for the success of our Action. The 
 +intention is to encourage us to have some form of technical 
 +interaction beyond talks. ​ As examples of such discussions,​ one may 
 +think of technical discussion sessions at project meetings, or 
 +technical discussion session at workshops such as SMT, where there is 
 +usually such a session on SMT-LIB/​SMT-COMP. 
 + 
 +In order to assemble a program, we need to hear from you! 
 + 
 +Therefore:​ 
 + 
 +(A) If you wish to give a talk, please send title and abstract. 
 +Optionally: Mention if you would prefer to be on the first day which 
 +is mainly focused on topics related to Automation in Proof Assistants. 
 + 
 +(B) If you wish to propose a topic for a technical discussion session, 
 +please send title and paragraph of motivation, and be prepared to chair, 
 +or co-chair, the session you propose. We may help you to find a 
 +co-chair, or one of us may co-chair with you, if need be. 
 + 
 +Please send both kinds of contributions ((A) and (B)) to both addresses 
 +<​keijo.heljanko@aalto.fi>​ and <​hugo.herbelin@inria.fr>​ at your 
 +earliest convenience,​ but no later than 
 + 
 +                      March 1, 2012
  
-[[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.+(This deadline is for finalizing ​the technical ​program; COST invitations 
 +are generated automatically for MC members ​and you'll receive one sooner.)