Proceedings of the 19th International Symposium of Formal Methods
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

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

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

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.

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.