|
Published: 2nd January 2014 DOI: 10.4204/EPTCS.139 ISSN: 2075-2180 |
| Preface 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 | 1 |
| Automated Reasoning over Deontic Action Logics with Finite Vocabularies Pablo F. Castro and Thomas S. E. Maibaum | 16 |
| Actions and Events in Concurrent Systems Design Valentin Cassano and Thomas S. E. Maibaum | 31 |
|
Short/Tool papers | |
| Fluent Logic Workflow Analyser: A Tool for The Verification of Workflow Properties Germán Regis, Fernando Villar and Nicolás Ricci | 46 |
| BEval: A Plug-in to Extend Atelier B with Current Verification Technologies Valério Medeiros Jr. and David Déharbe | 53 |
| The DynAlloy Visualizer Pablo Bendersky, Juan Pablo Galeotti and Diego Garbervetsky | 59 |
| HeteroGenius: A Framework for Hybrid Analysis of Heterogeneous Software Specifications Manuel Giménez, Mariano M. Moscato, Carlos G. Lopez Pombo and Marcelo F. Frias | 65 |
| Analyzing Behavioural Scenarios over Tabular Specifications Using Model Checking Gastón Scilingo, María Marta Novaira and Renzo Degiovanni | 71 |
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.