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
Last revision Both sides next revision
tallinn12 [2012/03/10 14:55]
vkuncak
tallinn12 [2012/03/14 23:57]
keijo.heljanko
Line 12: Line 12:
 Campus of the Tallinn University of Technology, the building of the Tallinn School of Economics and Business Administration,​ Akadeemia tee 3.  Campus of the Tallinn University of Technology, the building of the Tallinn School of Economics and Business Administration,​ Akadeemia tee 3. 
  
-====== Organizers ​======+===== 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. [[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.
  
-===== Preliminary ​Program =====+=====Program ​======
  
-** Sat 31.AIPA+SVARM ​**+[[http://​pauillac.inria.fr/​~herbelin/​aipa2012/​program.html|Link to the AIPA+SVARM ​joint program page 
 +]]
  
-  * 9:00- 9:30 Philip Ruemmer (Software Verification Using k-Induction) +====== Registration =====
-  *  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