Cliff B. Jones, Pekka Pihlajasaari, Jun Sun
Proceedings of the 19th International Symposium of Formal Methods
FM, 2014.

@proceedings{FM-2014,
	address       = "19th International Symposium, Singapore",
	doi           = "10.1007/978-3-319-06410-9",
	editor        = "Cliff B. Jones and Pekka Pihlajasaari and Jun Sun",
	isbn          = "978-3-319-06409-3",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 19th International Symposium of Formal Methods}",
	volume        = 8442,
	year          = 2014,
}

Contents (49 items)

11 ×#verification
8 ×#analysis
5 ×#formal method
4 ×#automation
4 ×#composition
4 ×#concurrent
4 ×#performance
4 ×#proving
4 ×#semantics
3 ×#invariant

FM-2014-HuPF #bidirectional #programming

Validity Checking of Putback Transformations in Bidirectional Programming (ZH, HP, SF), pp. 1–15.

FM-2014-Klein #proving

Proof Engineering Considered Essential (GK), pp. 16–21.

FM-2014-Woodcock #semantics

Engineering UToPiA — Formal Semantics for CML (JW), pp. 22–41.

FM-2014-BjornerH #formal method #question

40 Years of Formal Methods — Some Obstacles and Some Possibilities? (DB, KH), pp. 42–61.

FM-2014-AntoninoSW #analysis #concurrent #csp #network #process #refinement

A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes (PRGA, AS, JW), pp. 62–77.

FM-2014-ArmstrongGS #algebra #concurrent #tool support #verification

Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools (AA, VBFG, GS), pp. 78–93.

FM-2014-BaeOM #analysis #multi #semantics

Definition, Semantics, and Analysis of Multirate Synchronous AADL (KB, PCÖ, JM), pp. 94–109.

FM-2014-BaiHWLLM #formal method #model checking #named #platform #towards

TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms (GB, JH, JW, YL, ZL, AM), pp. 110–126.

FM-2014-BlomH #concurrent #source code #verification

The VerCors Tool for Verification of Concurrent Programs (SB, MH), pp. 127–131.

FM-2014-BonakdarpourHK #authentication #automation #knowledge-based #protocol

Knowledge-Based Automated Repair of Authentication Protocols (BB, RH, SSK), pp. 132–147.

FM-2014-BowenR #interactive #modelling #semantics

A Simplified Z Semantics for Presentation Interaction Models (JB, SR), pp. 148–162.

FM-2014-ButinM #analysis

Log Analysis for Data Protection Accountability (DB, DLM), pp. 163–178.

FM-2014-DammF #automation #composition #distributed #synthesis

Automatic Compositional Synthesis of Distributed Systems (WD, BF), pp. 179–193.

FM-2014-DenmanM #automation #proving

Automated Real Proving in PVS via MetiTarski (WD, CAM), pp. 194–199.

FM-2014-DerrickDSTTW #consistency #verification

Quiescent Consistency: Defining and Verifying Relaxed Linearizability (JD, BD, GS, BT, OT, HW), pp. 200–214.

FM-2014-DuggiralaWMVM #modelling #parallel #precedence #protocol

Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol (PSD, LW, SM, MV, CAM), pp. 215–229.

FM-2014-EstlerFNPM #contract

Contracts in Practice (HCE, CAF, MN, MP, BM), pp. 230–246.

FM-2014-FengZ #automaton #bisimulation #equivalence #probability

When Equivalence and Bisimulation Join Forces in Probabilistic Automata (YF, LZ), pp. 247–262.

FM-2014-ForejtKNS #analysis #communication #precise #predict #source code

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs (VF, DK, GN, SS), pp. 263–278.

FM-2014-FreitasW #formal method #proving

Proof Patterns for Formal Methods (LF, IW), pp. 279–295.

FM-2014-GunadiT #android #case study #logic #metric #monitoring #operating system #performance #runtime

Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System (HG, AT), pp. 296–311.

FM-2014-HahnLSTZ #model checking #named #probability

iscasMc: A Web-Based Probabilistic Model Checker (EMH, YL, SS, AT, LZ), pp. 312–317.

FM-2014-HayesM #algebra #invariant #realtime

Invariants, Well-Founded Statements and Real-Time Program Algebra (IJH, LM), pp. 318–334.

FM-2014-LakshmiAK #analysis #liveness #reachability #using

Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis (KVL, AA, RK), pp. 335–350.

FM-2014-KordyLMP #algorithm #analysis #automaton #robust

A Symbolic Algorithm for the Analysis of Robust Timed Automata (PK, RL, SM, JWP), pp. 351–366.

FM-2014-KrkaDMU

Revisiting Compatibility of Input-Output Modal Transition Systems (IK, ND, NM, SU), pp. 367–381.

FM-2014-LeinoM #automation #induction #proving #verification

Co-induction Simply — Automatic Co-inductive Proofs in a Program Verifier (KRML, MM), pp. 382–398.

FM-2014-LiTC #component #requirements

Management of Time Requirements in Component-Based Systems (YL, THT, MC), pp. 399–415.

FM-2014-LinH #composition #concurrent #learning #model checking #synthesis

Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning (SWL, PAH), pp. 416–431.

FM-2014-LiuXZS #verification

Formal Verification of Operational Transformation (YL, YX, SJZ, CS), pp. 432–448.

FM-2014-MaricS #hardware #memory management #transaction #verification

Verification of a Transactional Memory Manager under Hardware Failures and Restarts (OM, CS), pp. 449–464.

FM-2014-MarriottC #named

SCJ: Memory-Safety Checking without Annotations (CM, AC), pp. 465–480.

FM-2014-MitschQP #hybrid #logic #reasoning #refactoring #refinement

Refactoring, Refinement, and Reasoning — A Logical Characterization for Hybrid Systems (SM, JDQ, AP), pp. 481–496.

FM-2014-NistorABM

Object Propositions (LN, JA, SB, HM), pp. 497–513.

FM-2014-PolikarpovaTFM #collaboration #flexibility #invariant #semantics

Flexible Invariants through Semantic Collaboration (NP, JT, CAF, BM), pp. 514–530.

FM-2014-PonzioRAF #bound #performance

Efficient Tight Field Bounds Computation Based on Shape Predicates (PP, NR, NA, MFF), pp. 531–546.

FM-2014-RinastSG #graph #performance #reduction

A Graph-Based Transformation Reduction to Reach UPPAAL States Faster (JR, SS, DG), pp. 547–562.

FM-2014-RouxG #comparison #invariant #polynomial

Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison (PR, PLG), pp. 563–578.

FM-2014-SchebenS #calculus #composition #performance #self

Efficient Self-composition for Weakest Precondition Calculi (CS, PHS), pp. 579–594.

FM-2014-WenMM #analysis #formal method #information management #towards

Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections (RW, AM, CM), pp. 595–610.

FM-2014-SanatiMM #decidability #guidelines #logic #metric #using

Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal Logic (MYS, WM, TSEM), pp. 611–626.

FM-2014-ZeydaSCS #composition #higher-order #object-oriented

A Modular Theory of Object Orientation in Higher-Order UTP (FZ, TLVLS, AC, AS), pp. 627–642.

FM-2014-ChristakisLS #formal method #verification

Formalizing and Verifying a Modern Build Language (MC, KRML, WS), pp. 643–657.

FM-2014-ArenisWDMA #consistency #industrial #standard #verification

The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification (SFA, BW, DD, MM, ASA), pp. 658–672.

FM-2014-GuptaKG #experience #verification

Formally Verifying Graphics FPU — An Intel® Experience (AG, VMAK, RG), pp. 673–687.

FM-2014-LiuGL #analysis #reliability

MDP-Based Reliability Analysis of an Ambient Assisted Living System (YL, LG, YL), pp. 688–702.

FM-2014-RoySS #case study #experience #industrial #process

Diagnosing Industrial Business Processes: Early Experiences (SR, ASMS, SS), pp. 703–717.

FM-2014-ShanWFZZWQC #using #verification

Formal Verification of Lunar Rover Control Software Using UPPAAL (LS, YW, NF, XZ, LZ, LW, LQ, JC), pp. 718–732.

FM-2014-ZhaoYZGZC #verification

Formal Verification of a Descent Guidance Control Program of a Lunar Lander (HZ, MY, NZ, BG, LZ, YC), pp. 733–748.