Formal Methods: Foundations and Applications

1. Front Matter

   PDF

2. Meaningful Models

   • Christiano Braga, Cássio Santos

   Pages 1-16

3. Deductive Generalization

   • Kenneth L. McMillan

   Pages 17-17

4. Unifying Theories of Logic and Specification

   • Victor Bandur, Jim Woodcock

   Pages 18-33

5. Institution-Based Semantics for MOF and QVT-Relations

   • Daniel Calegari, Nora Szasz

   Pages 34-50

6. Derivation and Verification of Parallel Components for the Needs of an HPC Cloud

   • Thiago Braga Marcilon, Francisco Heron de Carvalho Junior

   Pages 51-66

7. An Executable Semantics for a Multimedia Authoring Language

   • Joel dos Santos, Christiano Braga, Débora C. Muchaluat-Saade

   Pages 67-82

8. On the Use of SPIN for Studying the Behavior of Nested Petri Nets

   • Mirtha Lina Fernández Venero, Flávio Soares Corrêa da Silva

   Pages 83-98

9. Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking

   • Christoph Gladisch, Shmuel Tyszberowicz

   Pages 99-114

10. Toward the Revision of CTL Models through Kripke Modal Transition Systems

    • Paulo T. Guerra, Aline Andrade, Renata Wassermann

    Pages 115-130

11. Formal Analysis of Information Flow Using Min-Entropy and Belief Min-Entropy

    • Ghassen Helali, Osman Hasan, Sofiène Tahar

    Pages 131-146

12. Theorem Proving Graph Grammars: Strategies for Discharging Proof Obligations

    • Luiz Carlos Lemos Junior, Simone André da Costa Cavalheiro, Luciana Foss

    Pages 147-162

13. A Refinement Framework for Autonomous Agents

    • Qin Li, Graeme Smith

    Pages 163-178

14. A Formal Semantics for SysML Activity Diagrams

    • Lucas Lima, André Didier, Márcio Cornélio

    Pages 179-194

15. Formal Analysis of Memory Contention in a Multiprocessor System

    • Liya Liu, Osman Hasan, Sofiène Tahar

    Pages 195-210

16. Algebraic Graph Transformations with Inheritance

    • Michael Löwe, Harald König, Christoph Schulz, Marius Schultchen

    Pages 211-226

17. Generating Protocol Software from CPN Models Annotated with Pragmatics

    • Kent Inge Fagerland Simonsen, Lars M. Kristensen, Ekkart Kindler

    Pages 227-242

18. Back Matter

    PDF

This book constitutes the refereed proceedings of the 16th Brazilian Symposium on Formal Methods, SBMF 2013, held in Brasilia, Brazil, in September/October 2013. The 14 revised full papers presented together with 2 keynotes were carefully reviewed and selected from 29 submissions. The papers presented cover a broad range of foundational and methodological issues in formal methods for the design and analysis of software and hardware systems as well as applications in various domains.

• formal verification
• model-driven engineering
• probabilistic model checking
• software testing
• temporal logic

• Centro de Informática, UFPE, Recife, Brazil

  Juliano Iyoda

• Microsoft Research, Redmond, USA

  Leonardo Moura

Policies and ethics