| Description |
1 online resource |
| Series |
Lecture notes in computer science, 0302-9743 ; 7498 |
|
Lecture notes in computer science ; 7498.
|
| Contents |
The Versatile Synchronous Observer / John Rushby -- Thirteen Years of Automated Code Analysis at Microsoft / Wolfram Schulte -- Model Checking Propositional Deontic Temporal Logic via a [mu]-Calculus Characterization / Araceli Acosta, Cecilia Kilmurray, Pablo F. Castro and Nazareno M. Aguirre -- An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting / Haniel Barbosa and David Déharbe -- Palytoxin Inhibits the Sodium-Potassium Pump -- An Investigation of an Electrophysiological Model Using Probabilistic Model Checking / Fernando A.F. Braz, Jader S. Cruz, Alessandra C. Faria-Campos and Sérgio V.A. Campos -- BETA: A B Based Testing Approach / Ernesto C.B. de Matos and Anamaria Martins Moreira -- A Process Algebra Based Strategy for Generating Test Vectors from SCR Specifications / Gustavo Carvalho, Diogo Falcão, Alexandre Mota and Augusto Sampaio -- Specification Patterns for Properties over Reachable States of Graph Grammars / Simone André da Costa Cavalheiro, Luciana Foss and Leila Ribeiro -- Compositionality and Refinement in Model-Driven Engineering / Jim Davies, Jeremy Gibbons, David Milward and James Welch -- Identifying Hardware Failures Systematically / André Didier and Alexandre Mota -- Investigating Time Properties of Interrupt-Driven Programs / Yanhong Huang, Yongxin Zhao, Jianqi Shi, Huibiao Zhu and Shengchao Qin -- Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflows / Germán Regis, Nicolás Ricci, Nazareno M. Aguirre and Tom Maibaum -- Composition of Model Transformations: A Categorical Framework / Christoph Schulz, Michael Löwe and Harald König -- Verification Rules for Exception Handling in Eiffel / Emil Sekerinski and Tian Zhang -- A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications / Subodh Sharma, Ganesh Gopalakrishnan and Greg Bronevetsky -- Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions / Dante Zanarini, Carlos Luna and Luis Sierra |
| Summary |
This book constitutes the refereed proceedings of the 15th Brazilian Symposium on Formal Methods, SBMF 2012, held in Natal, Brazil, in September 2012; co-located with CBSoft 2012, the Third Brazilian Conference on Software: Theory and Practice. 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 |
| Analysis |
Computer science |
|
Software engineering |
|
Logic design |
|
Information Systems |
|
Logics and Meanings of Programs |
|
Mathematical Logic and Formal Languages |
|
Programming Languages, Compilers, Interpreters |
|
Management of Computing and Information Systems |
| Bibliography |
Includes bibliographical references and author index |
| In |
Springer eBooks |
| Subject |
Formal methods (Computer science) -- Congresses
|
|
Management information systems.
|
|
Electronic Data Processing
|
|
Management Information Systems
|
|
Informatique.
|
|
Formal methods (Computer science)
|
|
Formale Methode
|
|
Verifikation
|
|
Softwaretest
|
|
Modellgetriebene Entwicklung
|
|
Fehlertoleranz
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Gheyi, Rohit
|
|
Naumann, David
|
| LC no. |
2012946266 |
| ISBN |
9783642332968 |
|
364233296X |
|
3642332951 |
|
9783642332951 |
|
