Formal Methods: Foundations and Applications: 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 ― December 1, 2017, Proceedings (Lecture Notes in Computer Science, 10623)

Annotation 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