Nikolaj Bjørner, Frank D. de Boer
Proceedings of the 20th International Symposium of Formal Methods
FM, 2015.

@proceedings{FM-2015,
	address       = "Oslo, Norway",
	doi           = "10.1007/978-3-319-19249-9",
	editor        = "Nikolaj Bjørner and Frank D. de Boer",
	isbn          = "978-3-319-19248-2",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 20th International Symposium of Formal Methods}",
	volume        = 9109,
	year          = 2015,
}

Contents (43 items)

11 ×#verification
6 ×#model checking
5 ×#modelling
5 ×#using
4 ×#automation
4 ×#bound
4 ×#formal method
3 ×#analysis
3 ×#design
3 ×#framework

FM-2015-AlbertACGGMPR #analysis #concurrent #distributed #source code

Resource Analysis: From Sequential to Concurrent and Distributed Programs (EA, PA, JC, SG, MGZ, EMM, GP, GRD), pp. 3–17.

FM-2015-Damm #analysis #automation #lessons learnt #named #verification

AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned (WD), pp. 18–19.

FM-2015-ElkaderGPS #automation #reasoning

Automated Circular Assume-Guarantee Reasoning (KAE, OG, CSP, SS), pp. 23–39.

FM-2015-AlTurkiA #distributed #framework #towards #using #verification #𝕂

Towards Formal Verification of Orchestration Computations Using the 𝕂 Framework (MAA, OA), pp. 40–56.

FM-2015-AmatoMMS #abstract domain

Narrowing Operators on Template Abstract Domains (GA, SDNDM, MCM, FS), pp. 57–72.

FM-2015-BagheriKMJ #android #bound #design #detection #protocol #verification

Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification (HB, EK, SM, DJ), pp. 73–89.

FM-2015-BringerCML #architecture #design #privacy #reasoning

Privacy by Design in Practice: Reasoning about Privacy Properties of Biometric System Architectures (JB, HC, DLM, RL), pp. 90–107.

FM-2015-AhrendtCPS #runtime #specification #verification

A Specification Language for Static and Runtime Verification of Data and Control Properties (WA, JMC, GJP, GS), pp. 108–125.

FM-2015-ConchonMZ #model checking

Certificates for Parameterized Model Checking (SC, AM, FZ), pp. 126–142.

FM-2015-DeboisHS #composition #information management #liveness #process #refinement #runtime #safety

Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes (SD, TTH, TS), pp. 143–160.

FM-2015-DerrickDSTW #transaction #verification

Verifying Opacity of a Transactional Mutex Lock (JD, BD, GS, OT, HW), pp. 161–177.

FM-2015-DerrickS #correctness #framework #memory management #modelling

A Framework for Correctness Criteria on Weak Memory Models (JD, GS), pp. 178–194.

FM-2015-DiekmannHC #semantics #set

Semantics-Preserving Simplification of Real-World Firewall Rule Sets (CD, LH, GC), pp. 195–212.

FM-2015-DangDP #logic #parametricity #specification #synthesis

Parameter Synthesis Through Temporal Logic Specifications (TD, TD, CP), pp. 213–230.

FM-2015-DuLT #independence #ltl #monitoring #policy #runtime

Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL (XD, YL, AT), pp. 231–247.

FM-2015-EisentrautGHS0 #bisimulation #probability

Probabilistic Bisimulation for Realistic Schedulers (CE, JCG, HH, LS, LZ), pp. 248–264.

FM-2015-FengHTZ #model checking #named #protocol #quantum #source code

QPMC: A Model Checker for Quantum Programs and Protocols (YF, EMH, AT, LZ), pp. 265–272.

FM-2015-FernandezAKK #automation #verification

Automated Verification of RPC Stub Code (MF, JA, GK, IK), pp. 273–290.

FM-2015-0001K #bound #model checking #using

Property-Driven Fence Insertion Using Reorder Bounded Model Checking (SJ, DK), pp. 291–307.

FM-2015-BratBDGHK #safety #verification

Verifying the Safety of a Flight-Critical System (GB, DHB, MD, DG, FH, TK), pp. 308–324.

FM-2015-KroeningLW #automaton #bound #model checking #proving #safety

Proving Safety with Trace Automata and Bounded Model Checking (DK, ML, GW), pp. 325–341.

FM-2015-LiSLD #protocol #security #verification

Verifying Parameterized Timed Security Protocols (LL, JS, YL, JSD), pp. 342–359.

FM-2015-0009ZZZ #abstraction #hybrid

Abstraction of Elementary Hybrid Systems by Variable Transformation (JL, NZ, HZ, LZ), pp. 360–377.

FM-2015-Nakajima #behaviour #energy #maude #realtime #using

Using Real-Time Maude to Model Check Energy Consumption Behavior (SN), pp. 378–394.

FM-2015-NelsonFK #difference #network #program analysis

Static Differential Program Analysis for Software-Defined Networks (TN, ADF, SK), pp. 395–413.

FM-2015-PolikarpovaTF #library

A Fully Verified Container Library (NP, JT, CAF), pp. 414–434.

FM-2015-QuatmannJDWAKB

Counterexamples for Expected Rewards (TQ, NJ, CD, RW, EÁ, JPK, BB), pp. 435–452.

FM-2015-SafilianMD #feature model #formal method #modelling #semantics

The Semantics of Cardinality-Based Feature Models via Formal Languages (AS, TSEM, ZD), pp. 453–469.

FM-2015-SchmittU #axiom #first-order #logic

Axiomatization of Typed First-Order Logic (PHS, MU), pp. 470–486.

FM-2015-SchneiderLW #modelling #problem #validation

Model-Based Problem Solving for University Timetable Validation and Improvement (DS, ML, TW), pp. 487–495.

FM-2015-SharmaWCHC #infinity #reasoning

Certified Reasoning with Infinity (AS, SW, AC, AH, WNC), pp. 496–513.

FM-2015-SogokonJ #hybrid #liveness #verification

Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems (AS, PBJ), pp. 514–531.

FM-2015-SolovyevJRG #estimation #fault #float

Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (AS, CJ, ZR, GG), pp. 532–550.

FM-2015-ZhuYGZZZ #data flow #graph #model checking #scheduling

Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking (XZ, RY, YLG, JZ, WZ, GZ), pp. 551–569.

FM-2015-ChimdyalwarDCVC #abstraction #bound #model checking #static analysis #using

Eliminating Static Analysis False Positives Using Loop Abstraction and Bounded Model Checking (BC, PD, AC, SV, AC), pp. 573–576.

FM-2015-DurandS #formal method #framework #generative #named

Autofunk: An Inference-Based Formal Model Generation Framework for Production Systems (WD, SS), pp. 577–580.

FM-2015-Evans #authentication #development

Software Development and Authentication for Arms Control Information Barriers (NE), pp. 581–584.

FM-2015-Hauck-Stattelmann #behaviour #industrial

Analyzing the Restart Behavior of Industrial Control Applications (SHS, SB, BS, SK, RJ), pp. 585–588.

FM-2015-LiuH #analysis #android #case study #kernel #security

Case Study: Static Security Analysis of the Android Goldfish Kernel (TL, RH), pp. 589–592.

FM-2015-KuritaIA #documentation #evolution #formal method #mobile #modelling

Practices for Formal Models as Documents: Evolution of VDM Application to “Mobile FeliCa” IC Chip Firmware (TK, FI, KA), pp. 593–596.

FM-2015-Lecomte #modelling #verification

Formal Virtual Modelling and Data Verification for Supervision Systems (TL), pp. 597–600.

FM-2015-MirandaMR #automation #design #generative #testing #using #verification

Using Simulink Design Verifier for Automatic Generation of Requirements-Based Tests (BM, HM, RR), pp. 601–604.

FM-2015-SchutsH #concept #development #formal method

Formalizing the Concept Phase of Product Development (MS, JH), pp. 605–608.