Maurice H. ter Beek, Annabelle McIver, José N. Oliveira
Third World Congress on Formal Methods: The Next 30 Years
FM, 2019.

@proceedings{FM-2019,
	doi           = "10.1007/978-3-030-30942-8",
	editor        = "Maurice H. ter Beek and Annabelle McIver and José N. Oliveira",
	isbn          = "['978-3-030-30941-1', '978-3-030-30942-8']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Third World Congress on Formal Methods: The Next 30 Years}",
	volume        = 11800,
	year          = 2019,
}

Contents (46 items)

FM-2019-KrishnamurthiN #formal method

The Human in Formal Methods (SK, TN), pp. 3–10.

FM-2019-Andronick #social

Successes in Deployed Verified Software (and Insights on Key Social Factors) (JA), pp. 11–17.

FM-2019-MoscatoTFM #algorithm #float #implementation

Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm (MMM, LT, MAF, CAM), pp. 21–37.

FM-2019-BardBD #fault #smt #using

Formally Verified Roundoff Errors Using SMT-based Certificates and Subdivisions (JB, HB, ED), pp. 38–44.

FM-2019-BodeveixBCF #liveness #protocol #verification

Mechanically Verifying the Fundamental Liveness Property of the Chord Protocol (JPB, JB, DC, MF), pp. 45–63.

FM-2019-BoerB #execution #on the #symbolic computation

On the Nature of Symbolic Execution (FSdB, MMB), pp. 64–80.

FM-2019-AmramMP #specification

GR(1)*: GR(1) Specifications Extended with Existential Guarantees (GA, SM, OP), pp. 83–100.

FM-2019-CeskaHJK #probability #sketching #synthesis

Counterexample-Driven Synthesis for Probabilistic Program Sketches (MC0, CH, SJ, JPK), pp. 101–120.

FM-2019-LutebergetJS #capacity #layout #specification #synthesis

Synthesis of Railway Signaling Layout from Local Capacity Specifications (BL, CJ, MS), pp. 121–137.

FM-2019-SogokonMTCP #framework #generative #invariant #named

Pegasus: A Framework for Sound Continuous Invariant Generation (AS, SM, YKT, KC, AP), pp. 138–157.

FM-2019-ZhaoSZ0 #concurrent #framework #parametricity #reasoning

A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems (YZ, DS, FZ, YL0), pp. 161–178.

FM-2019-DerrickDDSW #concurrent #correctness #data type #persistent #verification

Verifying Correctness of Persistent Concurrent Data Structures (JD, SD, BD, GS, HW), pp. 179–195.

FM-2019-Lang0M #bisimulation #composition #concurrent #verification

Compositional Verification of Concurrent Systems by Combining Bisimulations (FL, RM0, FM), pp. 196–213.

FM-2019-GomesB #model checking #towards

Towards a Model-Checker for Circus (AOG, AB), pp. 217–234.

FM-2019-GomesB19a #csp #model checking #named #using

Circus2CSP: A Tool for Model-Checking Circus Using FDR (AOG, AB), pp. 235–242.

FM-2019-Ehlers #how #model checking #question

How Hard Is Finding Shortest Counter-Example Lassos in Model Checking? (RE), pp. 245–261.

FM-2019-Jantsch0B0 #ambiguity #automaton #ltl

From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata (SJ, DM0, CB, JK0), pp. 262–279.

FM-2019-DeifelMSW #automaton #refinement

Generic Partition Refinement and Weighted Tree Automata (HPD, SM, LS, TW), pp. 280–297.

FM-2019-KwiatkowskaN0S #concurrent #game studies #model checking #probability

Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games (MK, GN, DP0, GS), pp. 298–315.

FM-2019-SteinhofelH #execution

Abstract Execution (DS, RH), pp. 319–336.

FM-2019-SinghPDD #detection #kernel #static analysis

Static Analysis for Detecting High-Level Races in RTOS Kernels (AS, RP, DD, MD), pp. 337–353.

FM-2019-LunelMBT #composition #difference #logic #parallel #verification

Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic (SL, SM, BB, JPT), pp. 354–370.

FM-2019-TanP #approach #axiom #difference #equation #liveness

An Axiomatic Approach to Liveness for Differential Equations (YKT, AP), pp. 371–388.

FM-2019-IroftiD #consistency #data flow #modelling

Local Consistency Check in Synchronous Dataflow Models (DI, PD), pp. 389–405.

FM-2019-StuckiSSB #monitoring

Gray-Box Monitoring of Hyperproperties (SS, CS, GS, BB), pp. 406–424.

FM-2019-Evangelidis0 #verification

Quantitative Verification of Numerical Stability for Kalman Filters (AE, DP0), pp. 425–441.

FM-2019-PhamLP0 #source code #testing

Concolic Testing Heap-Manipulating Programs (LHP, QLL, QSP, JS0), pp. 442–461.

FM-2019-VuO #natural language #semantics #specification

Formal Semantics Extraction from Natural Language Specifications for ARM (AVV, MO), pp. 465–483.

FM-2019-ChargueraudFLP #ml #specification

GOSPEL - Providing OCaml with a Formal Specification Language (AC, JCF, CL, MP), pp. 484–501.

FM-2019-ArusoaieL #logic #unification

Unification in Matching Logic (AA, DL), pp. 502–518.

FM-2019-KornerBDKL #specification

Embedding High-Level Formal Specifications into Applications (PK, JB, JD, SK, ML), pp. 519–535.

FM-2019-SmithCM #data flow #memory management #modelling #security

Value-Dependent Information-Flow Security on Weak Memory Models (GS, NC, TM), pp. 539–555.

FM-2019-BrenasES #database #query #reasoning

Reasoning Formally About Database Queries and Updates (JHB, RE, MS), pp. 556–572.

FM-2019-BeringerA #abstraction #c #composition #source code #verification

Abstraction and Subsumption in Modular Verification of C Programs (LB, AWA), pp. 573–590.

FM-2019-KasampalisGMSZF #ecosystem #named

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain (TK, DG, BMM, TFS, YZ, DF, VNS, RJ, GR), pp. 593–610.

FM-2019-MarmsolerB #architecture #modelling #named #proving

APML: An Architecture Proof Modeling Language (DM, GB), pp. 611–630.

FM-2019-Sheinvald #automaton #infinity #learning

Learning Deterministic Variable Automata over Infinite Alphabets (SS), pp. 633–650.

FM-2019-TapplerA0EL #learning #markov #process

L*-Based Learning of Markov Decision Processes (MT, BKA, GB0, ME, KGL), pp. 651–669.

FM-2019-TranLMYNXJ #analysis #network #reachability

Star-Based Reachability Analysis of Deep Neural Networks (HDT, DML, PM, XY, LVN, WX, TTJ), pp. 670–686.

FM-2019-JongmansLE #problem

SOA and the Button Problem (SSJ, AL, MCJDvE), pp. 689–706.

FM-2019-SuP0 #network #scalability

Controlling Large Boolean Networks with Temporary and Permanent Perturbations (CS, SP, JP0), pp. 707–724.

FM-2019-SilveiraJVJ #formal method #implementation #specification #using

Formal Methods Applicability on Space Applications Specification and Implementation Using MORA-TSP (DS, AJ, MV, TJ), pp. 727–737.

FM-2019-Eschbach #concept #data analysis #industrial #monitoring

Industrial Application of Event-B to a Wayside Train Monitoring System: Formal Conceptual Data Analysis (RE), pp. 738–745.

FM-2019-ComptierDFP #analysis

Property-Driven Software Analysis - (Extended Abstract) (MC, DD, PF, JMP), pp. 746–750.

FM-2019-AielloDRHH

Practical Application of SPARK to OpenUxAS (MAA, CD, PR, LH, JH), pp. 751–761.

FM-2019-BeekBFFGLM #formal method #industrial

Adopting Formal Methods in an Industrial Setting: The Railways Case (MHtB, AB, AF, AF, SG, CL, FM), pp. 762–772.