Third World Congress on Formal Methods: The Next 30 Years
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

FM
DBLP
Scholar
DOI
Full names Links ISxN
@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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.