Electronic Notes in Theoretical Computer Science, Volume 240

Volume 240, July 2009

• Patrícia D. L. Machado:
  Preface. 1-3
  
• Néstor Cataño, Fernando Barraza, Daniel García, Pablo Ortega, Camilo Rueda:
  A Case Study in JML-Assisted Software Development. 5-21
  
• Ana Cavalcanti:
  Stateflow Diagrams in Circus. 23-41
  
• Simone André da Costa, Leila Ribeiro:
  Formal Verification of Graph Grammars using Mathematical Induction. 43-60
  
• Umberto Souza da Costa, Anamaria Martins Moreira, Martin A. Musicante, Plácido A. Souza Neto:
  Specification and Runtime Verification of Java Card Programs. 61-78
  
• Bartira Dantas, David Déharbe, Stephenson Galvão, Anamaria Martins Moreira, Valério Medeiros Júnior:
  Verified Compilation and the B Method: A Proposal and a First Appraisal. 79-96
  
• Paulo Salem da Silva, Ana Cristina Vieira de Melo:
  Model Checking Merged Program Traces. 97-112
  
• Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine:
  Combining Decision Procedures by (Model-)Equality Propagation. 113-128
  
• André Didier, Adalberto Farias, Alexandre Mota:
  Checking Z Data Refinements Using Traces Refinement. 129-148
  
• Flávia Falcão, Juliano Iyoda, Augusto Sampaio:
  Multiple Synchrony in MSC. 149-166
  
• Thierry Jéron:
  Symbolic Model-based Test Selection. 167-184
  
• Magnus O. Myreen, Michael J. C. Gordon:
  Transforming Programs into Recursive Functions. 185-200
  
• Juan Ignacio Perna, Jim Woodcock:
  Mechanised Wire-wise Verification of Handel-C Synthesis. 201-219
  
• Paul Regnier, George Lima, Aline Maria Santos Andrade:
  A TLA+ Formal Specification and Verification of a New Real-Time Communication Protocol. 221-238
  
• Frank Zeyda, Ana Cavalcanti:
  Mechanical Reasoning about Families of UTP Theories. 239-257