Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I

Front Matter ....Pages i-xviii
Front Matter ....Pages 1-3
 Experiences with Streamlining Formal Methods Tools  (Paolo Masci)....Pages 5-11
 The Bourgeois Gentleman, Engineering and Formal Methods  (Thierry Lecomte)....Pages 12-18
 SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B  (Mohammadsadegh Dalvandi, Michael Butler, Asieh Salehi Fathabadi)....Pages 19-29
 Compiling C and C++ Programs for Dynamic White-Box Analysis  (Zuzana Baranová, Petr Ročkai)....Pages 30-45
 Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table  (Petr Ročkai)....Pages 46-60
 Addressing Usability in a Formal Development Environment  (Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene, Patrizia Scandurra)....Pages 61-76
 Formal Modelling and Verification as Rigorous Review Technology: An Inspiration from INSPEX  (Richard Banach, Joseph Razavi, Olivier Debicki, Suzanne Lesecq)....Pages 77-91
Front Matter ....Pages 93-98
 Validation of a Simulation Algorithm for Safety-Critical Human Multitasking  (Giovanna Broccia, Paolo Milazzo, Cristina Belviso, Carmen Berrocal Montiel)....Pages 99-113
 An Ontology-Based Approach to Support Formal Verification of Concurrent Systems  (Natalia Garanina, Igor Anureev, Elena Sidorova, Dmitry Koznov, Vladimir Zyubin, Sergei Gorlatch)....Pages 114-130
 How to Look Next? A Data-Driven Approach for Scanpath Prediction  (Giuseppe Boccignone, Vittorio Cuculo, Alessandro D’Amelio)....Pages 131-145
 “Know Thyself” How Personal Music Tastes Shape the Last.Fm Online Social Network  (Riccardo Guidotti, Giulio Rossetti)....Pages 146-161
 Gender Recognition in the Wild with Small Sample Size - A Dictionary Learning Approach  (Alessandro D’Amelio, Vittorio Cuculo, Sathya Bursic)....Pages 162-169
 An Instrumented Mobile Language Learning Application for the Analysis of Usability and Learning  (Aigerim Aibassova, Antonio Cerone, Mukhtar Tashkenbayev)....Pages 170-185
 Analysis and Visualization of Performance Indicators in University Admission Tests  (Michela Natilli, Daniele Fadda, Salvatore Rinzivillo, Dino Pedreschi, Federica Licari)....Pages 186-199
 Anomaly Detection from Log Files Using Unsupervised Deep Learning  (Sathya Bursic, Vittorio Cuculo, Alessandro D’Amelio)....Pages 200-207
Front Matter ....Pages 209-215
 Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent  (Gleifer Vaz Alves, Louise Dennis, Michael Fisher)....Pages 217-232
 CriSGen: Constraint-Based Generation of Critical Scenarios for Autonomous Vehicles  (Andreas Nonnengart, Matthias Klusch, Christian Müller)....Pages 233-248
 Verification of Fair Controllers for Urban Traffic Manoeuvres at Intersections  (Christopher Bischopink, Maike Schwammberger)....Pages 249-264
 Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs  (Keith Clark, Brijesh Dongol, Peter Robinson)....Pages 265-280
 A Mission Definition, Verification and Validation Architecture  (Louis Viard, Laurent Ciarletta, Pierre-Etienne Moreau)....Pages 281-287
Front Matter ....Pages 289-292
 Smart Contracts: Application Scenarios for Deductive Program Verification  (Bernhard Beckert, Jonas Schiffl, Mattias Ulbrich)....Pages 293-298
 Deductive Proof of Industrial Smart Contracts Using Why3  (Zeinab Nehaï, François Bobot)....Pages 299-311
 Verifying Smart Contracts with Cubicle  (Sylvain Conchon, Alexandrina Korneva, Fatiha Zaïdi)....Pages 312-324
 Call Me Back, I Have a Type Invariant  (M. Anthony Aiello, Johannes Kanig, Taro Kurita)....Pages 325-336
 Statistical Model Checking of RANDAO’s Resilience to Pre-computed Reveal Strategies  (Musab A. Alturki, Grigore Roşu)....Pages 337-349
 A Distributed Blockchain Model of Selfish Mining  (Dennis Eijkel, Ansgar Fehnker)....Pages 350-361
 Towards a Verified Model of the Algorand Consensus Protocol in Coq  (Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña et al.)....Pages 362-367
 Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts  (Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, Julien Tesson)....Pages 368-379
 Smart Contract Interactions in Coq  (Jakob Botsch Nielsen, Bas Spitters)....Pages 380-391
 Formal Specification of a Security Framework for Smart Contracts  (Mikhail Mandrykin, Jake O’Shannessy, Jacob Payne, Ilya Shchepetkov)....Pages 392-403
Front Matter ....Pages 405-407
 Examples of the Application of Formal Methods to Interactive Systems  (Michael D. Harrison)....Pages 409-423
 Modelling Human Reasoning in Practical Behavioural Contexts Using Real-Time Maude  (Antonio Cerone, Peter Csaba Ölveczky)....Pages 424-442
 A Survey of Papers from Formal Methods for Interactive Systems (FMIS) Workshops  (Pascal Béger, Sebastien Leriche, Daniel Prun)....Pages 443-464
 Formal Modelling of Safety-Critical Interactive Devices Using Coloured Petri Nets  (Sapna Jaidka, Steve Reeves, Judy Bowen)....Pages 465-485
 Model-Based Testing of Post-WIMP Interactions Using Object Oriented Petri-Nets  (Alexandre Canny, David Navarre, José Creissac Campos, Philippe Palanque)....Pages 486-502
 Fortune Nets for Fortunettes: Formal, Petri Nets-Based, Engineering of Feedforward for GUI Widgets  (David Navarre, Philippe Palanque, Sven Coppers, Kris Luyten, Davy Vanacken)....Pages 503-519
Back Matter ....Pages 521-523