Published: 2nd January 2014
DOI: 10.4204/EPTCS.139
ISSN: 2075-2180


Proceedings First
Latin American Workshop on Formal Methods
Buenos Aires, Argentina, August 26th 2013

Edited by: Nazareno Aguirre and Leila Ribeiro

Nazareno Aguirre and Leila Ribeiro

Full papers

On Verifying Resource Contracts using Code Contracts
Rodrigo Castaño, Juan Pablo Galeotti, Diego Garbervetsky, Jonathan Tapicer and Edgardo Zoppi
Automated Reasoning over Deontic Action Logics with Finite Vocabularies
Pablo F. Castro and Thomas S. E. Maibaum
Actions and Events in Concurrent Systems Design
Valentin Cassano and Thomas S. E. Maibaum

Short/Tool papers

Fluent Logic Workflow Analyser: A Tool for The Verification of Workflow Properties
Germán Regis, Fernando Villar and Nicolás Ricci
BEval: A Plug-in to Extend Atelier B with Current Verification Technologies
Valério Medeiros Jr. and David Déharbe
The DynAlloy Visualizer
Pablo Bendersky, Juan Pablo Galeotti and Diego Garbervetsky
HeteroGenius: A Framework for Hybrid Analysis of Heterogeneous Software Specifications
Manuel Giménez, Mariano M. Moscato, Carlos G. Lopez Pombo and Marcelo F. Frias
Analyzing Behavioural Scenarios over Tabular Specifications Using Model Checking
Gastón Scilingo, María Marta Novaira and Renzo Degiovanni


Formal approaches to software development are techniques that aim at developing quality software by employing notations, analysis processes, etc., based on mathematical grounds. Although traditionally they aim at increasing software correctness, formal techniques have been applied to various other aspects of software quality. Moreover, while originally formal methods employed complex "heavyweight" mechanisms for analysis (often manual or semi automated), there has been progress towards embracing "lightweight", many times fully automated, analysis techniques, that broaden the adoption of formal methods in various software engineering contexts. Today, research on formal methods include a great variety of topics, ranging from formal foundations for Computer Science to specific languages, methodologies and techniques for rigorous software development.

The Latin American Workshop on Formal Methods brought together researchers working in formal methods, and related areas such as automated analysis. It provided a venue for Latin American researchers working in these areas, to promote their interaction and collaboration. The workshop was held in August as a satellite event of CONCUR 2013. It took place in Buenos Aires, Argentina's capital and largest city, and one of the most interesting cultural places in South America. The workshop program included an invited talk, given by Marcelo Frias, and both full and short tool papers whose topics included logics for Computer Science, tool support for a variety of formal methods (and covering both analysis techniques and other forms of support such as visualisation), foundations of formal specification languages, and applications of formal methods. A total of 8 submissions have been accepted and are part of this volume, while the workshop also featured accepted talk proposals on recent or ongoing research. Submissions came from Argentina, Brazil, Uruguay and Germany.

We are grateful to the program committee members and additional reviewers for their hard work in evaluating submissions, as well as to the workshop participants, who engaged in interesting and fruitful discussions during the workshop. Special thanks go to Pedro D'Argenio and Hernán Melgratti, co-chairs of CONCUR 2013, and the organising committee of CONCUR 2013, for their support and continuous help in making the workshop a success.