John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, Anna Philippou
Proceedings of the 21st International Symposium of Formal Methods
FM, 2016.

@proceedings{FM-2016,
	doi           = "10.1007/978-3-319-48989-6",
	editor        = "John S. Fitzgerald and Constance L. Heitmeyer and Stefania Gnesi and Anna Philippou",
	isbn          = "978-3-319-48988-9",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 21st International Symposium of Formal Methods}",
	volume        = 9995,
	year          = 2016,
}

Contents (50 items)

FM-2016-PeleskaH #modelling #safety #testing

Industrial-Strength Model-Based Testing of Safety-Critical Systems (JP0, WlH), pp. 3–22.

FM-2016-AbdullaAD #verification

Counter-Example Guided Program Verification (PAA, MFA, BPD), pp. 25–42.

FM-2016-AntoninoGR #analysis #reachability

Tighter Reachability Criteria for Deadlock-Freedom Analysis (PRGA, TGR, AWR), pp. 43–59.

FM-2016-AstefanoaeiBBCR #composition #parametricity #synthesis

Compositional Parameter Synthesis (LA, SB, MB, CHC, HR), pp. 60–68.

FM-2016-BeckerCGHHKNSTT #analysis #formal method #modelling #proving #testing

Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor (HB, JMC, JG, UH, YH, CK, KN0, JLS, HT, TT), pp. 69–84.

FM-2016-BenesBDPS #analysis #approach #model checking

A Model Checking Approach to Discrete Bifurcation Analysis (NB, LB, MD, SP, DS), pp. 85–101.

FM-2016-BohmMJ #concurrent #detection #reduction

State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI (SB, OM, PJ), pp. 102–118.

FM-2016-ChandLS #distributed #multi #verification

Formal Verification of Multi-Paxos for Distributed Consensus (SC, YAL, SDS), pp. 119–136.

FM-2016-ChenFLMZ #difference #verification

Validated Simulation-Based Verification of Delayed Differential Dynamics (MC, MF, YL, PNM, NZ), pp. 137–154.

FM-2016-ChenP0 #cyber-physical #invariant #learning #towards #verification

Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation (YC0, CMP, JS0), pp. 155–163.

FM-2016-CimattiMS #automaton #hybrid #network

From Electrical Switched Networks to Hybrid Automata (AC, SM, MS), pp. 164–181.

FM-2016-DavidKKL #invariant

Danger Invariants (CD, PK, DK, ML), pp. 182–198.

FM-2016-DellabaniCBB #bound #interactive #multi

Local Planning of Multiparty Interactions with Bounded Horizons (MD, JC, MB, SB), pp. 199–216.

FM-2016-DimovskiBW #abstraction #analysis #variability

Finding Suitable Variability Abstractions for Family-Based Analysis (ASD, CB, AW), pp. 217–234.

FM-2016-DjoudiBG #source code

Recovering High-Level Conditions from Binary Programs (AD, SB, ÉG), pp. 235–253.

FM-2016-Flores-Montoya #bound #source code

Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations (AFM), pp. 254–273.

FM-2016-GiannakopoulouG #quality

Exploring Model Quality for ACAS X (DG, DG, JS), pp. 274–290.

FM-2016-GiantamidisT #learning

Learning Moore Machines from Input-Output Traces (GG, ST), pp. 291–309.

FM-2016-GomesS #algebra #correctness

Modal Kleene Algebra Applied to Program Correctness (VBFG, GS), pp. 310–325.

FM-2016-GrovLT #verification

Mechanised Verification Patterns for Dafny (GG, YL, VT), pp. 326–343.

FM-2016-HasanagicTLL #formal method #interface #standard #validation

Formalising and Validating the Interface Description in the FMI Standard (MH, PWVTJ, KL, PGL), pp. 344–351.

FM-2016-HayesCMWV #algebra

An Algebra of Synchronous Atomic Steps (IJH, RJC, LAM, KW, AV), pp. 352–369.

FM-2016-HolzerSBWW #concurrent #fault #invariant

Error Invariants for Concurrent Traces (AH, DSN, MTB, GW, TW), pp. 370–387.

FM-2016-HouSTLH #architecture #case study #execution #formal method #set

An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor (ZH, DS, AT, YL0, KCH), pp. 388–405.

FM-2016-KawamotoBL #data flow #estimation #hybrid #statistics

Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow (YK0, FB, AL), pp. 406–425.

FM-2016-KhyzhaGP #logic #proving

A Generic Logic for Proving Linearizability (AK, AG, MJP), pp. 426–443.

FM-2016-KobayashiIH #refactoring #refinement

Refactoring Refinement Structure of Event-B Machines (TK, FI, SH), pp. 444–459.

FM-2016-KongLCSSW #hybrid #testing #towards

Towards Concolic Testing for Hybrid Systems (PK, YL0, XC0, JS0, MS0, JW), pp. 460–478.

FM-2016-LahavV #memory management #modelling #program transformation

Explaining Relaxed Memory Models with Program Transformations (OL, VV), pp. 479–495.

FM-2016-LetanCHNM #named #security #specification #verification

SpecCert: Specifying and Verifying Hardware-Based Security Enforcement (TL, PC, GH, PN, BM), pp. 496–512.

FM-2016-LiSD #automation #protocol #security #verification

Automated Verification of Timed Security Protocols with Clock Drift (LL0, JS0, JSD), pp. 513–530.

FM-2016-MenghiSG #model checking

Dealing with Incompleteness in Automata-Based Model Checking (CM, PS, CG), pp. 531–550.

FM-2016-Mukherjee0GKM #c #equivalence #float

Equivalence Checking of a Floating-Point Unit Against a High-Level C Model (RM, SJ0, AG, DK, TM), pp. 551–558.

FM-2016-BisgaardGHKNS #scheduling

Battery-Aware Scheduling in Low Orbit: The GomX-3 Case (MB, DG, HH, JK, GN, MS), pp. 559–576.

FM-2016-OdyFH #calculus

Discounted Duration Calculus (HO, MF, MRH), pp. 577–592.

FM-2016-RothenbergG #program repair

Sound and Complete Mutation-Based Program Repair (BCR, OG), pp. 593–611.

FM-2016-SenjakH #coq #implementation

An Implementation of Deflate in Coq (CSS, MH0), pp. 612–627.

FM-2016-SogokonGJ #abstraction #difference #equation

Decoupling Abstractions of Non-linear Ordinary Differential Equations (AS, KG, TTJ), pp. 628–644.

FM-2016-StrichmanV #recursion #verification

Regression Verification for Unbalanced Recursive Functions (OS, MV), pp. 645–658.

FM-2016-TaLKC #automation #induction #logic #proving

Automated Mutual Explicit Induction Proof in Separation Logic (QTT, TCL, SCK, WNC), pp. 659–676.

FM-2016-VakiliD #finite #logic #similarity #using

Finite Model Finding Using the Logic of Equality with Uninterpreted Functions (AV, NAD), pp. 677–693.

FM-2016-WijsNB #gpu #model checking

GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking (AW, TN, DB), pp. 694–701.

FM-2016-YanJLWZ #approximate #bisimulation #csp #hybrid

Approximate Bisimulation and Discretization of Hybrid CSP (GY, LJ, YL, SW, NZ), pp. 702–720.

FM-2016-YangHCL0 #approach #generative #hybrid #linear #programming

A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems (ZY, CH, XC0, WL, ZL0), pp. 721–738.

FM-2016-CavadaCCRT #design #embedded #energy #modelling #using

Model-Based Design of an Energy-System Embedded Controller Using Taste (RC, AC, LC, MR, ST), pp. 741–747.

FM-2016-FilipovikjMMSLL #industrial #model checking #statistics

Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems (PF, NM, RM, CS, OL, HL), pp. 748–756.

FM-2016-JiangLSKGSS #design #formal method #modelling #multi

Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller (YJ0, HL0, HS, HK, MG0, JS, LS), pp. 757–763.

FM-2016-LiuJZGS #industrial #multi #verification

Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers (HL0, YJ0, HZ, MG0, JS), pp. 764–771.

FM-2016-LutebergetJFS #design #incremental #rule-based #tool support #verification

Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations (BL, CJ, CF, MS), pp. 772–778.

FM-2016-StoenescuSPI #analysis #execution #framework #named #symbolic computation #using

RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions (TS, AS, SP, FI), pp. 779–785.