menu 简单麦麦
account_circle

正式方法——未来30年:第三届世界大会,FM 2019,葡萄牙波尔图,2019年10月7日至11日,会议记录-Formal Methods – The Next 30 Years: Third Wor

帮助2571人找到了他们想要的文件
上传于 2020-03-02 20次下载 852次围观
文件编号:6460
文件详情
标题(title):Formal Methods – The Next 30 Years: Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings
正式方法——未来30年:第三届世界大会,FM 2019,葡萄牙波尔图,2019年10月7日至11日,会议记录
作者(author):Maurice H. ter Beek, Annabelle McIver, José N. Oliveira
出版社(publisher):Springer International Publishing
大小(size):36 MB (37358216 bytes)
格式(extension):pdf
注意:如果文件下载完成后为无法打开的格式,请修改后缀名为格式对应后缀



This book constitutes the refereed proceedings of the 23rd Symposium on Formal Methods, FM 2019, held in Porto, Portugal, in the form of the Third World Congress on Formal Methods, in October 2019.
The 44 full papers presented together with 3 invited presentations were carefully reviewed and selected from 129 submissions. The papers are organized in topical sections named: Invited Presentations; Verification; Synthesis Techniques; Concurrency; Model Checking Circus; Model Checking; Analysis Techniques; Specification Languages; Reasoning Techniques; Modelling Languages; Learning-Based Techniques and Applications; Refactoring and Reprogramming; I-Day Presentations.









Table of contents :
Front Matter ....Pages i-xxi
Front Matter ....Pages 1-1
The Human in Formal Methods (Shriram Krishnamurthi, Tim Nelson)....Pages 3-10
Successes in Deployed Verified Software (and Insights on Key Social Factors) (June Andronick)....Pages 11-17
Front Matter ....Pages 19-19
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm (Mariano M. Moscato, Laura Titolo, Marco A. Feliú, César A. Muñoz)....Pages 21-37
Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions (Joachim Bard, Heiko Becker, Eva Darulova)....Pages 38-44
Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol (Jean-Paul Bodeveix, Julien Brunel, David Chemouil, Mamoun Filali)....Pages 45-63
On the Nature of Symbolic Execution (Frank S. de Boer, Marcello Bonsangue)....Pages 64-80
Front Matter ....Pages 81-81
GR(1)*: GR(1) Specifications Extended with Existential Guarantees (Gal Amram, Shahar Maoz, Or Pistiner)....Pages 83-100
Counterexample-Driven Synthesis for Probabilistic Program Sketches (Milan Češka, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen)....Pages 101-120
Synthesis of Railway Signaling Layout from Local Capacity Specifications (Bjørnar Luteberget, Christian Johansen, Martin Steffen)....Pages 121-137
Pegasus: A Framework for Sound Continuous Invariant Generation (Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer)....Pages 138-157
Front Matter ....Pages 159-159
A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems (Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu)....Pages 161-178
Verifying Correctness of Persistent Concurrent Data Structures (John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim)....Pages 179-195
Compositional Verification of Concurrent Systems by Combining Bisimulations (Frédéric Lang, Radu Mateescu, Franco Mazzanti)....Pages 196-213
Front Matter ....Pages 215-215
Towards a Model-Checker for Circus (Artur Oliveira Gomes, Andrew Butterfield)....Pages 217-234
Circus2CSP: A Tool for Model-Checking Circus Using FDR (Artur Oliveira Gomes, Andrew Butterfield)....Pages 235-242
Front Matter ....Pages 243-243
How Hard Is Finding Shortest Counter-Example Lassos in Model Checking? (Rüdiger Ehlers)....Pages 245-261
From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata (Simon Jantsch, David Müller, Christel Baier, Joachim Klein)....Pages 262-279
Generic Partition Refinement and Weighted Tree Automata (Hans-Peter Deifel, Stefan Milius, Lutz Schröder, Thorsten Wißmann)....Pages 280-297
Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games (Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos)....Pages 298-315
Front Matter ....Pages 317-317
Abstract Execution (Dominic Steinhöfel, Reiner Hähnle)....Pages 319-336
Static Analysis for Detecting High-Level Races in RTOS Kernels (Abhishek Singh, Rekha Pai, Deepak D’Souza, Meenakshi D’Souza)....Pages 337-353
Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic (Simon Lunel, Stefan Mitsch, Benoit Boyer, Jean-Pierre Talpin)....Pages 354-370
An Axiomatic Approach to Liveness for Differential Equations (Yong Kiam Tan, André Platzer)....Pages 371-388
Local Consistency Check in Synchronous Dataflow Models (Dina Irofti, Paul Dubrulle)....Pages 389-405
Gray-Box Monitoring of Hyperproperties (Sandro Stucki, César Sánchez, Gerardo Schneider, Borzoo Bonakdarpour)....Pages 406-424
Quantitative Verification of Numerical Stability for Kalman Filters (Alexandros Evangelidis, David Parker)....Pages 425-441
Concolic Testing Heap-Manipulating Programs (Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun)....Pages 442-461
Front Matter ....Pages 463-463
Formal Semantics Extraction from Natural Language Specifications for ARM (Anh V. Vu, Mizuhito Ogawa)....Pages 465-483
GOSPEL—Providing OCaml with a Formal Specification Language (Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço, Mário Pereira)....Pages 484-501
Unification in Matching Logic (Andrei Arusoaie, Dorel Lucanu)....Pages 502-518
Embedding High-Level Formal Specifications into Applications (Philipp Körner, Jens Bendisposto, Jannik Dunkelau, Sebastian Krings, Michael Leuschel)....Pages 519-535
Front Matter ....Pages 537-537
Value-Dependent Information-Flow Security on Weak Memory Models (Graeme Smith, Nicholas Coughlin, Toby Murray)....Pages 539-555
Reasoning Formally About Database Queries and Updates (Jon Haël Brenas, Rachid Echahed, Martin Strecker)....Pages 556-572
Abstraction and Subsumption in Modular Verification of C Programs (Lennart Beringer, Andrew W. Appel)....Pages 573-590
Front Matter ....Pages 591-591
IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain (Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Florin Șerbănuță, Yi Zhang, Daniele Filaretti et al.)....Pages 593-610
APML: An Architecture Proof Modeling Language (Diego Marmsoler, Genc Blakqori)....Pages 611-630
Front Matter ....Pages 631-631
Learning Deterministic Variable Automata over Infinite Alphabets (Sarai Sheinvald)....Pages 633-650
\(L^*\)-Based Learning of Markov Decision Processes (Martin Tappler, Bernhard K. Aichernig, Giovanni Bacci, Maria Eichlseder, Kim G. Larsen)....Pages 651-669
Star-Based Reachability Analysis of Deep Neural Networks (Hoang-Dung Tran, Diago Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang et al.)....Pages 670-686
Front Matter ....Pages 687-687
SOA and the Button Problem (Sung-Shik Jongmans, Arjan Lamers, Marko van Eekelen)....Pages 689-706
Controlling Large Boolean Networks with Temporary and Permanent Perturbations (Cui Su, Soumya Paul, Jun Pang)....Pages 707-724
Front Matter ....Pages 725-725
Formal Methods Applicability on Space Applications Specification and Implementation Using MORA-TSP (Daniel Silveira, Andreas Jung, Marcel Verhoef, Tiago Jorge)....Pages 727-737
Industrial Application of Event-B to a Wayside Train Monitoring System: Formal Conceptual Data Analysis (Robert Eschbach)....Pages 738-745
Property-Driven Software Analysis (Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero-Perez)....Pages 746-750
Practical Application of SPARK to OpenUxAS (M. Anthony Aiello, Claire Dross, Patrick Rogers, Laura Humphrey, James Hamil)....Pages 751-761
Adopting Formal Methods in an Industrial Setting: The Railways Case (Maurice H. ter Beek, Arne Borälv, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi, Christer Löfving et al.)....Pages 762-772
Back Matter ....Pages 773-774
-到底部了哦-
微信扫码支付
正式方法——未来30年:第三届世界大会,FM 2019,葡萄牙波尔图,2019年10月7日至11日,会议记录-Formal Methods – The Next 30 Years: Third Wor
支付金额: 共计:¥0.0

添加收藏

创建新合集