Klaus Havelund, Jan Peleska 0001, Bill Roscoe, Erik P. de Vink
Proceedings of the 22nd International Symposium of Formal Methods
FM, 2018.

@proceedings{FM-2018,
	doi           = "10.1007/978-3-319-95582-7",
	editor        = "Klaus Havelund and Jan Peleska 0001 and Bill Roscoe and Erik P. de Vink",
	isbn          = "['978-3-319-95581-0', '978-3-319-95582-7']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 22nd International Symposium of Formal Methods}",
	volume        = 10951,
	year          = 2018,
}

Contents (46 items)

FM-2018-FernandesDM #data flow #perspective #privacy

Processing Text for Privacy: An Information Flow Perspective (NF, MD, AM), pp. 3–21.

FM-2018-LarsenLN #realtime #validation

20 Years of Real Real Time Model Validation (KGL, FL, BN), pp. 22–36.

FM-2018-AzadbakhtBV #concurrent #detection

Deadlock Detection for Actor-Based Coroutines (KA, FSdB, EPdV), pp. 39–54.

FM-2018-AmericoAM #algebra #approach #data flow #reasoning

An Algebraic Approach for Reasoning About Information Flow (AA, MSA, AM), pp. 55–72.

FM-2018-Wang0JQX #towards #verification

Towards 'Verifying' a Water Treatment System (JW, JS0, YJ, SQ, ZX), pp. 73–92.

FM-2018-AvellanedaP #automaton

FSM Inference from Long Traces (FA, AP), pp. 93–109.

FM-2018-CavezzaAG

A Weakness Measure for GR(1) Formulae (DGC, DA, AG), pp. 110–128.

FM-2018-BusardP #logic

Producing Explanations for Rich Logics (SB, CP), pp. 129–146.

FM-2018-Ferrere

The Compound Interest in Relaxing Punctuality (TF), pp. 147–164.

FM-2018-RuchkinSISG #cyber-physical #integration #multi #named

IPL: An Integration Property Language for Multi-model Cyber-physical Systems (IR, JS, GI, BRS, DG), pp. 165–184.

FM-2018-PardoSS #knowledge base #network #social

Timed Epistemic Knowledge Bases for Social Networks (RP, CS, GS), pp. 185–202.

FM-2018-0001BFLMR #automaton #energy #nondeterminism #robust #synthesis #using

Optimal and Robust Controller Synthesis - Using Energy Timed Automata with Uncertainty (GB0, PB, UF, KGL, NM, PAR), pp. 203–221.

FM-2018-HayesM #algebra #concurrent #encoding

Encoding Fairness in a Synchronous Concurrent Program Algebra (IJH, LAM), pp. 222–239.

FM-2018-ColvinS #memory management #modelling #source code #verification

A Wide-Spectrum Language for Verification of Programs on Weak Memory Models (RJC, GS), pp. 240–257.

FM-2018-FavaSS #memory management #semantics

Operational Semantics of a Weak Memory Model with Channel Synchronization (DSF, MS, VS), pp. 258–276.

FM-2018-GeislerH #development #distributed #model checking #using

Stepwise Development and Model Checking of a Distributed Interlocking System - Using RAISE (SG, AEH), pp. 277–293.

FM-2018-YanZZLYH #design #multi #reliability #resource management

Resource-Aware Design for Reliable Autonomous Applications with Multiple Periods (RY, DZ, FZ, YL, JY, KH0), pp. 294–311.

FM-2018-BergerKAWR #c #case study #experience #verification

Verifying Auto-generated C Code from Simulink - An Experience Report in the Automotive Domain (PB, JPK, EÁ, MTBW, TR), pp. 312–328.

FM-2018-VandinBLL #analysis #configuration management #named

QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (AV, MHtB, AL, ALL), pp. 329–337.

FM-2018-LetanRCH #composition #coq #source code #verification

Modular Verification of Programs with Effects and Effect Handlers in Coq (TL, YRG, PC, GH), pp. 338–354.

FM-2018-BeckerPDT #analysis #float #optimisation #tool support

Combining Tools for Optimization and Analysis of Floating-Point Computations (HB, PP, ED, ZT), pp. 355–363.

FM-2018-TitoloMMDB #algorithm #float #implementation

A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (LT, MMM, CAM, AD, FB), pp. 364–381.

FM-2018-NellenRWAK #challenge #empirical #evaluation #modelling #recommendation #verification

Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (JN, TR, MTBW, EÁ, JPK), pp. 382–398.

FM-2018-MenghiGPT #ltl #multi #nondeterminism

Multi-robot LTL Planning Under Uncertainty (CM, SG0, PP, JT), pp. 399–417.

FM-2018-SogokonGTP #comparison

Vector Barrier Certificates and Comparison Systems (AS, KG, YKT, AP), pp. 418–437.

FM-2018-ChocklerGK

Timed Vacuity (HC, SG, OK), pp. 438–455.

FM-2018-AkazakiLYDH #cyber-physical #learning #using

Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (TA, SL, YY, YD, JH), pp. 456–465.

FM-2018-KhannaSRP #source code #verification

Dynamic Symbolic Verification of MPI Programs (DK, SS0, CR, RP), pp. 466–484.

FM-2018-PutterW #analysis #composition #generative

To Compose, or Not to Compose, That Is the Question: An Analysis of Compositional State Space Generation (SdP, AW), pp. 485–504.

FM-2018-Lowe #abstraction #component

View Abstraction for Systems with Component Identities (GL), pp. 505–522.

FM-2018-ZhangZSLTLS #composition #concurrent #reasoning #source code

Compositional Reasoning for Shared-Variable Concurrent Programs (FZ, YZ, DS, YL0, AT, SWL, JS0), pp. 523–541.

FM-2018-LegayNPT #model checking #statistics

Statistical Model Checking of LLVM Code (AL, DN, DBP, LMT), pp. 542–549.

FM-2018-AlbertGRS0 #modelling #named #source code #verification

SDN-Actors: Modeling and Verification of SDN Programs (EA, MGZ, AR, MS, AS0), pp. 550–567.

FM-2018-Porncharoenwase #named

CompoSAT: Specification-Guided Coverage for Model Finding (SP, TN, SK), pp. 568–587.

FM-2018-FanHM #approximate #partial order #reduction

Approximate Partial Order Reduction (CF, ZH, SM), pp. 588–607.

FM-2018-Laneve #analysis #concurrent #lightweight #source code #thread

A Lightweight Deadlock Analysis for Programs with Threads and Reentrant Locks (CL), pp. 608–624.

FM-2018-CimattiST #architecture #specification #verification

Formal Specification and Verification of Dynamic Parametrized Architectures (AC, IS, ST), pp. 625–644.

FM-2018-MunozND #requirements

From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (CAM, AN, AD), pp. 647–652.

FM-2018-Boralv #automation #design #proving #using

Interlocking Design Automation Using Prover Trident (AB), pp. 653–656.

FM-2018-BrauerS #modelling #testing

Model-Based Testing for Avionics Systems (JB, US), pp. 657–661.

FM-2018-KastnerMF #abstract interpretation #on the #safety #security

On Software Safety, Security, and Abstract Interpretation (DK, LM, CF), pp. 662–665.

FM-2018-AvgustinovBM #analysis

Variant Analysis with QL (PA, KB, MYM), pp. 666–670.

FM-2018-Cohen #object-oriented #proving #security

Object-Oriented Security Proofs (EC), pp. 671–674.

FM-2018-Bjorner #industrial #smt

Z3 and SMT in Industrial R&D (NB), pp. 675–678.

FM-2018-BeyeneR #integration #tool support #verification

Evidential and Continuous Integration of Software Verification Tools (TAB, HR), pp. 679–685.

FM-2018-Lecomte #deployment #development

Disruptive Innovations for the Development and the Deployment of Fault-Free Software (TL), pp. 686–689.