Financé par ANR

RAVAJ


Rewriting and Approximations for Java Applications Verification

Menu

Home Members Meetings Tools Publications

Meetings
Sixth RAVAJ meeting, Loria Nancy, December 8-9, 2009

Workshop notes (restricted)
Participants:
  • Emilie Balland (INRIA, Bordeaux)
  • Yohan Boichut (LIFO, Orléans)
  • Benoît Boyer (IRISA, Rennes)
  • Roméo Courbis (LIFC, Besançon)
  • Aloïs Dreyfus (LIFC, Besançon)
  • Thomas Genet (IRISA, Rennes)
  • Pierre-Cyrille Héam (LIFC, Besançon)
  • Olga Kouchnarenko (LIFC, Besançon)
  • Pierre-Etienne Moreau (LORIA, Nancy)
Events:
  • Tuesday, December 8
    • 15h00, Talk, "Domain Specific Static Analysis", Emilie Balland
    • 15h45, Talk, "Verifying properties on CCS specifications using over-approximations", Roméo Courbis
    • 16h15, Coffee Break
    • 16h45, Talk, "Ensuring termination of completion using Knaster-Tarski theorem", Thomas Genet
    • 20h00, Gala dinner
 
  • Wednesday, December 9
    • 10h00, Talk, "Counter example generation on tree automata completion", Benoît Boyer
    • 10h45, Talk, "TomedTimbuk, the end", Aloïs Dreyfus
    • 11h15, Coffee Break
    • 11h45, "How to Tackle Integer Weighted Automata Positivity", Pierre-Cyrille Héam
    • 12h30 Lunch
    • 14h00, Talk, "To be Announced", Yohan Boichut
    • 14h30 Synchronisation on t0+36 deliverables, final report and final paper
    • 15h00, "Current State of the RAVAJ project", Thomas Genet
    • 15h30 Discussion about the future of the project
    • 17h00, end of Sixth RAVAJ meeting

___
Fith RAVAJ meeting, LIFC Besançon, June 23-24, 2009

Workshop notes (restricted)
Participants:
  • Benoît Boyer (IRISA, Rennes)
  • Roméo Courbis (LIFC, Besançon)
  • Aloïs Dreyfus (LIFC, Besançon)
  • Thomas Genet (IRISA, Rennes)
  • Pierre-Cyrille Héam (LIFC, Besançon)
  • Olga Kouchnarenko (LIFC, Besançon)
  • Pierre-Etienne Moreau (LORIA, Nancy)
Events:
  • Tuesday, June 23
    • 15h00, Talk, "TAGED Approximations for verifying temporal patterns", Pierre-Cyrille Héam
    • 15h45, Talk, "Verifying Temporal Regular Properties on Abstractions of Term Rewriting Systems", Benoît Boyer
    • 16h30, Coffee Break
    • 16h45, Talk, "Approximation refinement in TomedTimbuk", Aloïs Dreyfus
 
  • Wednesday, June 24
    • 10h00, Talk, "A simple encoding of Java Threads in Rewriting", Thomas Genet
    • 10h45, Talk, "What properties to prove on Java with Threads", Yohan Boichut
    • 11h30, Coffee Break
    • 11h45, Synchronisation on t0+30 deliverables. Planning of t0+36 deliverables
    • 12h30, Lunch
    • 14h00, Talk, "Termination of rewriting under strategies", Pierre-Etienne Moreau
    • 14h45, Discussion on the future of the RAVAJ project
    • 15h30, Coffee Break
    • 15h45, Initialization of the RAVAJ paper
    • 17h00, end of fith RAVAJ meeting

___



Fourth RAVAJ meeting, Paris, November13, 2008
Espace ATEAC, 33rd floor, Montparnasse Tower

Workshop notes (restricted)
Participants:
  • Emilie Balland (LORIA, Nancy)
  • Nicolas Barré (IRISA, Rennes)
  • Yohan Boichut (LORIA, Nancy)
  • Benoît Boyer (IRISA, Rennes)
  • Roméo Courbis (LIFC, Besançon)
  • Aloïs Dreyfus (LIFC, Besançon)
  • Thomas Genet (IRISA, Rennes)
  • Pierre-Cyrille Héam (LIFC, Besançon)
  • Olga Kouchnarenko (LIFC, Besançon)
  • Pierre-Etienne Moreau (LORIA, Nancy)

Events: Thursday, November 13th

  • 9h30, Welcome Coffee
  • 10h00, Talk, "Java bytecode to TRS compiler status", Nicolas Barré
  • 10h45, Talk, "Term-graph rewriting via explicit paths", Emilie Balland
  • 11h15, Discussion on heap and reference representation in rewriting semantics of Java
  • 12h30, Lunch
  • 14h00, Talk, "Property based approximation construction", Roméo Courbis
  • 14h45, Discussion on test cases for programs to check and properties to prove
  • 15h45, Coffee Break
  • 16h15, Talk, "Equational Approximations for Tree Automata Completion", Thomas Genet
  • 17h00, end of Fourth RAVAJ meeting

___




Third RAVAJ meeting, LORIA Nancy, June 16-18, 2008

Workshop notes (restricted)
Participants:
  • Emilie Balland (LORIA, Nancy)
  • Yohan Boichut (LORIA, Nancy)
  • Benoît Boyer (IRISA, Rennes)
  • Roméo Courbis (LIFC, Besançon)
  • Thomas Genet (IRISA, Rennes)
  • Pierre-Cyrille Héam (LIFC, Besançon)
  • Olga Kouchnarenko (LIFC, Besançon)
  • Pierre-Etienne Moreau (LORIA, Nancy)

Events:
  • Monday, June 16th, 14h00-17h00, room A006
    • Training talk, "RAVAJ project" for ANR, Thomas Genet
    • Talk, "Towards an efficient implementation of tree automata completion", Yohan Boichut
    • Talk, "Abstraction Refinement for Rewriting Approximations", Roméo Courbis

  • Tuesday, June 17th, 10h00-12h00, room A006
    • Talk, "Tree Automata Certification", Benoît Boyer
    • Talk, "New design for the bytecode translator", Emilie Balland

  • Tuesday, June 17th, 14h00-17h00, room A006
    • Discussion on bytecode translator format
  • Wednesday, June 18th, 9h00-11h00, room A006
    • Discussion on deliverables (d2.2: Analysis of Java Programs: user guided approximations), (d5.2: Design of Completion with equations), (d7.1: Completion tool without equations)
    • Discussion on progress report and web-site

17th Dinner.
  • Emilie Balland
  • Yohan Boichut
  • Benoît Boyer
  • Roméo Courbis
  • Thomas Genet
  • Pierre-Cyrille Héam
  • Olga Kouchnarenko
  • Pierre-Etienne Moreau

___
Second RAVAJ meeting, LIFC Besançon, November 7-9, 2007
Workshop notes (restricted)

Participants:
  • Emilie Balland (LORIA, Nancy)
  • Yohan Boichut (LORIA, Nancy)
  • Benoît Boyer (IRISA, Rennes)
  • Roméo Courbis (LIFC, Besançon)
  • Thomas Genet (IRISA, Rennes)
  • Alain Giorgetti (LIFC, Besançon)
  • Pierre-Cyrille Héam (LIFC, Besançon)
  • Olga Kouchnarenko (LIFC, Besançon)
  • Pierre-Etienne Moreau (LORIA, Nancy)
  • Vlad Rusu (IRISA, Rennes)

Events:
  • Wednesday, November 7th, 14h00-18h00, 305 bis
    • Talk, "RAVAJ current state", Thomas Genet
    • Talk, "How to encode completion in Tom", Yohan Boichut
    • Talk, "Progress on Tree Automata Completion Certification", Benoît Boyer
  • Thursday, November 8th, 9h00-12h00, 404 C
    • Talk, "Rewriting Semantics of Java MIDP", Yohan Boichut
    • Talk, "Approximation refinement", Roméo Courbis
    • Talk, "Conformity Testing on Rewriting Semantics", Emilie Balland
  • Thursday, November 8th, 14h00-16h00, 404 C
    • Discussion on deliverables: Completion in Tom and Trex compiler
  • Thursday, November 8th, 16h30, 404 C
    • Talk, "A tool to validate RAVAJ tool", Pierre-Cyrille Héam
  • Friday, November 9th, 9h00-11h00, 404 C
    • Discussion on progress report and web-site (deliverable)
    • Discussion on a survey paper about RAVAJ
    • Discussions on approximation refinement, Tom implementation of completion, conformity testing

8th Dinner.
  • Emilie Balland
  • Yohan Boichut
  • Benoît Boyer
  • Roméo Courbis
  • Thomas Genet
  • Alain Giorgetti
  • Pierre-Cyrille Héam
  • Olga Kouchnarenko
  • Pierre-Etienne Moreau
  • Vlad Rusu

___



First RAVAJ meeting, IRISA Rennes, April 18-20, 2007
Workshop notes (restricted)

Participants:
  • Emilie Balland (LORIA, Nancy)
  • Yohan Boichut (IRISA, Rennes)
  • Benoît Boyer (IRISA, Rennes)
  • Thomas Genet (IRISA, Rennes)
  • Olga Kouchnarenko (LIFC, Besançon)
  • Thomas Jensen (IRISA, Rennes)
  • Laurent Hubert (IRISA, Rennes)
  • Pierre-Etienne Moreau (LORIA, Nancy)
  • Vlad Rusu (IRISA, Rennes)
Events:
  • April 18th, 14h00-18h00, Oléron, A008
    • Talk, "RAVAJ goals", Thomas Genet
    • Talk, "Trex tool and Term Rewriting Semantics for Java", Laurent Hubert
    • Talk, "Manipulating Java Bytecode in Tom", Emilie Balland
    • Talk, "Recent advance on analysis of Java using approximations", Yohan Boichut
    • Discussion on rewriting semantics for Java (deliverable)
  • April 19th 9h00-12h00, Aurigny D165 and 14h00-18h00, Crete F402
    • Talks,"Tree Automata Certification", Benoît Boyer
    • Talk, "Approximation refinement", Olga Kouchnarenko
    • Talk, "Introduction to specification and verification in Maude", Vlad Rusu
    • Discussion on security properties (deliverable)
    • Dinner
  • April 20th 9h00-12h00, Oléron, A008
    • Discussion on progress report and web-site (deliverable)
    • Discussions on approximation refinement and rewriting analyser implementation
    • Lunch at Tournebride

19th Dinner, Léon le cochon, 20h00
  • Yohan Boichut
  • Laurent Hubert
  • Pierre-Etienne Moreau
  • Emilie Balland
  • Olga Kouchnarenko
  • Thomas Genet
  • Thomas Jensen
  • Benoît Boyer
20th Lunch, Tournebride, 12h30
  • Yohan Boichut
  • Vlad Rusu
  • Pierre-Etienne Moreau
  • Emilie Balland
  • Thomas Genet
  • Thomas Jensen
  • Benoît Boyer

Page design borrowed from James Koster via OSWD.