Program

9-10 Invited talk

Marcelo Frias. BLISS: Bounded Lazy Initialization with SAT-Support

10-10:30 Coffee break.

10:30-12:30 Technical session 1 (Foundations)

Pablo Castro and Tom Maibaum, Automated Reasoning over Deontic Action Logics with Finite Vocabularies

Gilles Barthe, Gustavo Betarte, Juan Diego Campo and Carlos Luna, VirtualCert: A certified idealized model of virtualization

Valentin Cassano and Tom Maibaum, Actions and Events in Concurrent System Design

Manuel Giménez, Mariano M. Moscato, Carlos G. López Pombo and Marcelo Frias, HeteroGenius: a framework for hybrid analysis of heterogeneous software specifications

12:30-14 Lunch

14-15:30 Technical session 2 (Software Validation and Verification I)

Gaston Scilingo, Maria Marta Novaira and Renzo Degiovanni, Analyzing Behavioural Scenarios over Tabular Specifications Using Model Checking

Anamaria Martins Moreira and Cleverton Hentz, Grammars for Test Generation

Valério Gutemberg Medeiros Jr and David Deharbe, B-Eval: a plug-in to extend Atelier-B with current verification technologies

15:30-16 Coffee break

16-17:30 Technical session 3 (Software Validation and Verification II)

Pablo Bendersky, Juan Galeotti and Diego Garbervetsky, The DynAlloy Visualizer

Germán Regis, Fernando Villar and Nicolás Ricci, Fluent Logic Workflow Analyser: A tool for The Verification of Workflow Properties

Rodrigo Castaño, Juan Galeotti, Diego Garbervetsky, Jonathan Tapicer and Edgardo Zoppi, On verifying resource contracts using Code Contracts