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

✍ Scribed by Michael Leuschel, Jens Bendisposto (auth.), Jim Davies, Leila Silva, Adenilso Simao (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2011
• Tongue: English
• Leaves: 301
• Series: Lecture Notes in Computer Science 6527
• Edition: 1
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

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 -

✦ Subjects

Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Programming Techniques; Mathematical Logic and Formal Languages; Management of Computing and Information Systems