Formal Methods: Foundations and Applications: 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers

Description

This book constitutes the thoroughly refereed post-conference proceedings of the 13th Brazilian Symposium on Formal Methods, SBMF 2010, held in Natal, Brazil, in November 2010. The 18 revised full papers were carefully reviewed and selected from 55 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. Front Matter....Pages - Directed Model Checking for B: An Evaluation and New Techniques....Pages 1-16 Midlet Navigation Graphs in JML....Pages 17-32 Runtime Verification for Generic Classes with ConGu 2....Pages 33-48 A High-Level Language for Modeling Algorithms and Their Properties....Pages 49-63 A Formal Environment Model for Multi-Agent Systems....Pages 64-79 A Modal Interface Theory with Data Constraints....Pages 80-95 Synchronizing Model and Program Refactoring....Pages 96-111 A Type-Theoretic Framework for Certified Model Transformations....Pages 112-127 Simulating Truly Concurrent CSP....Pages 128-143 Statistical Verification of Probabilistic Properties with Unbounded Until....Pages 144-160 Reasoning about Assignments in Recursive Data Structures....Pages 161-176 Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned....Pages 177-193 A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence....Pages 194-209 Formal Development of a Cardiac Pacemaker: From Specification to Code....Pages 210-225 A Decision Procedure for Bisimilarity of Generalized Regular Expressions....Pages 226-241 Normalization of Linear Horn Clauses....Pages 242-257 A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs....Pages 258-273 Automating Refinement of Circus Programs....Pages 274-290 Back Matter....Pages -