Formal Methods: Foundations and Applications: 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 — December 1, 2017, Proceedings

Description

This book constitutes the refereed proceedings of the 20th Brazilian Symposium on Formal Methods, SBMF 2017, which took place in Recifel, Brazil, in November/December 2017.The 16 papers presented together with three invited talks were carefully reviewed and selected from 37 submissions. They are organized in the following topical sections: formal methods integration and experience reports; model checking; refinement and verification; and semantics and languages. The chapter 'Rapidly Adjustable Non-Intrusive Online Monitoring for Multi-core Systems' is published open access under a CC BY 4.0 license. Front Matter ....Pages I-X Front Matter ....Pages 1-1 Formal Methods for Robotics: RoboChart, RoboSim, and More (Ana Cavalcanti)....Pages 3-6 Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract) (Christoph Benzmüller)....Pages 7-11 Front Matter ....Pages 13-13 Abstract State Machines and System Theoretic Process Analysis for Safety-Critical Systems (Farah Al-Shareefi, Alexei Lisitsa, Clare Dixon)....Pages 15-32 From Scenarios to Timed Automata (Neda Saeedloei, Feliks Kluźniak)....Pages 33-51 Graph Grammar Extraction from Source Code (Lucio Mauro Duarte, Leila Ribeiro)....Pages 52-69 Applying a Formal Method in Industry: A 25-Year Trajectory (Thierry Lecomte, David Deharbe, Etienne Prun, Erwan Mottin)....Pages 70-87 Front Matter ....Pages 89-89 Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks (Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole)....Pages 91-106 Local Analysis of Determinism for CSP (Rodrigo Otoni, Ana Cavalcanti, Augusto Sampaio)....Pages 107-124 OptCE: A Counterexample-Guided Inductive Optimization Solver (Higo F. Albuquerque, Rodrigo F. Araújo, Iury V. Bessa, Lucas C. Cordeiro, Eddie B. de Lima Filho)....Pages 125-141 Formal Analysis of the Information Leakage of the DC-Nets and Crowds Anonymity Protocols (Arthur Américo, Artur Vaz, Mário S. Alvim, Sérgio V. A. Campos, Annabelle McIver)....Pages 142-158 Front Matter ....Pages 159-159 A Refinement Relation for Families of Timed Automata (Guillermina Cledou, José Proença, Luís S. Barbosa)....Pages 161-178 Rapidly Adjustable Non-intrusive Online Monitoring for Multi-core Systems (Normann Decker, Philip Gottschling, Christian Hochberger, Martin Leucker, Torben Scheffel, Malte Schmitz et al.)....Pages 179-196 Sound Transpilation from Binary to Machine-Independent Code (Roberto Metere, Andreas Lindner, Roberto Guanciale)....Pages 197-214 Using Linear Logic to Verify Requirement Scenarios in Composite Web Service (Kênia Santos de Oliveira, Stéphane Julia)....Pages 215-232 Checking Static Properties Using Conservative SAT Approximations for Reachability (Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe)....Pages 233-250 Front Matter ....Pages 251-251 UTCP: Compositional Semantics for Shared-Variable Concurrency (Andrew Butterfield)....Pages 253-270 On Kleene Algebras for Weighted Computation (Leandro Gomes, Alexandre Madeira, Luís S. Barbosa)....Pages 271-286 Capturing Stochastic and Real-Time Behavior in Reo Connectors (Yi Li, Xiyue Zhang, Yuanyi Ji, Meng Sun)....Pages 287-304 Back Matter ....Pages 305-305