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
tallinn12 [2012/03/10 14:56]
vkuncak
tallinn12 [2014/05/07 22:48] (current)
vkuncak
Line 16: Line 16:
 [[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 ​**+{{:tallinn.pdf|Archived PDF Page}}; original link: [[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