Accepted Papers

FM 2015 Main Track: Accepted Papers

Cornelius Diekmann, Lars Hupel and Georg Carle.
Semantics-Preserving Simplification of Real-World Firewall Rule Sets
Nadia Polikarpova, Julian Tschannen and Carlo A. Furia.
A Fully Verified Container Library
Alexey Solovyev, Charlie Jacobsen, Zvonimir Rakamaric and Ganesh Gopalakrishnan.
Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
Shin Nakajima.
Using Real-Time Maude to Model Check Energy Consumption Behavior
Li Li, Jun Sun, Yang Liu and Jin Song Dong.
Verifying Parameterized Timed Security Protocols
Jiang Liu, Naijun Zhan, Hengjun Zhao and Liang Zou.
Abstraction of Elementary Hybrid Systems by Variable Transformation
Tommaso Dreossi, Thao Dang and Carla Piazza.
Parameter Synthesis through Temporal Logic Specifications
Peter Schmitt and Mattias Ulbrich.
Typed First-Order Logic
Jesus Mauricio Chimento, Wolfgang Ahrendt, Gerardo Schneider and Gordon Pace.
A Specification Language for Static and Runtime Verification of Data and Control Properties
Karam Abdelkader, Orna Grumberg, Corina Pasareanu and Sharon Shoham.
Automated Circular Assume-Guarantee Reasoning
Xue-Yang Zhu, Rongjie Yan, Yu-Lei Gu, Jian Zhang, Wenhui Zhang and Guangquan Zhang.
Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
Tim Nelson, Andrew D. Ferguson and Shriram Krishnamurthi.
Static Differential Program Analysis for Software-Defined Networks
Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz.
Automated Verification of RPC Stub Code
Yuan Feng, Ernst Moritz Hahn, Andrea Turrini and Lijun Zhang.
QPMC: A Model Checker for Quantum Programs and Protocols
Julien Bringer, Hervé Chabanne, Daniel Le Métayer and Roch Lescuyer.
Privacy by design in practice: reasoning about privacy properties of biometric system architectures
Musab A. Alturki and Omar Alzuhaibi.
Towards Formal Verification of Orchestration Computations Using the K Framework
Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns, Lei Song and Lijun Zhang.
Probabilistic Bisimulation for Realistic Schedulers
Temesghen Kahsai, Falk Howar, Dimitra Giannakopoulou, Guillaume Brat and Misty Davies.
Verifying the Safety of a Flight-Critical System
Gianluca Amato, Simone Di Nardo Di Maio, Maria Chiara Meo and Francesca Scozzari.
Narrowing operators on template abstract domains
Xiaoning Du, Yang Liu and Alwen Tiu.
Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
David Schneider, Michael Leuschel and Tobias Witt.
Model-Based Problem Solving for University Timetable Validation and Improvement
Søren Debois, Thomas Hildebrandt and Tijs Slaats.
Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
Saurabh Joshi and Daniel Kroening.
Property-Driven Fence Insertion using Reorder Bounded Model Checking
Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen and Bernd Becker.
Counterexamples for Expected Rewards
Daniel Kroening, Matt Lewis and Georg Weissenbacher.
Proving Safety with Trace Automata and Bounded Model Checking
John Derrick and Graeme Smith.
A framework for correctness criteria on weak memory models
John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin and Heike Wehrheim.
Verifying Opacity of a Transactional Mutex Lock
Aliakbar Safilian, Tom Maibaum and Zinovy Diskin.
The Semantics of Cardinality-based Feature Models via Formal Languages
Sylvain Conchon, Alain Mebsout and Fatiha Zaidi.
Certificates for Parameterized Model Checking
Hamid Bagheri, Eunsuk Kang, Sam Malek and Daniel Jackson.
Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
Andrew Sogokon and Paul Jackson.
Direct formal verification of liveness properties in continuous and hybrid dynamical systems
Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor and Wei-Ngan Chin.
Certified Reasoning with Infinity

FM 2015 Industry Track: Accepted Papers

Rodrigo Reis, Henrique Masini and Bruno Miranda.
Using Simulink Design Verifier for automatic generation of requirements-based testing
Ralf Huuck and Tao Liu.
Case Study: Static Security Analysis of the Android Goldfish Kernel
Stefan Hauck-Stattelmann, Sebastian Biallas, Bastian Schlich, Stefan Kowalewski and Raoul Jetley.
Analyzing the Restart Behavior of Industrial Control Applications
Bharti Chimdyalwar, Priyanka Darke, Anooj Chavda, Sagar Vaghani and Avriti Chauhan.
Eliminating static analysis false positives using loop abstraction and bounded model checking
Mathijs Schuts and Jozef Hooman.
Formalizing the Concept Phase of Product Development at Philips Healthcare
Neil Evans.
Software Development and Authentication for Arms Control Information Barriers
William Durand and Sébastien Salva.
Autofunk: an inference-based formal model generation framework for production systems.
Taro Kurita, Fuyuki Ishikawa and Keijiro Araki.
Practices for Formal Models as Documents: Evolution of VDM Application to Mobile FeliCa IC Chip Firmware
Thierry Lecomte.
Formal Virtual Modelling and Data Verification for Supervision Systems

FM 2015 Doctoral Symposium: Accepted Papers

Mohamed Mahdi Benmoussa.
Specification and verification of real-time systems
Andreas Müller.
Component-based CPS Verification: A Recipe for Reusability
José Dihego.
Inheritance and refinement of trustworthy component-based systems
Florian Lorber.
Test-Case Generation via Language Inclusion for Non-Deterministic Networks of Timed Automata
Miran Hasanagic.
A Code Generator for VDM-RT models
Matthew Luckcuck.
A Formal Model for the Safety-Critical Java Level 2 Paradigm
Raúl Pardo.
Privacy-Preserving Social Networks
Maike Schwammberger.
Properties of Communicating Controllers for Safe Traffic Manoeuvres
Aliakbar Safilian.
A Novel and Faithful Semantics for Feature Modeling
Xiaoning Du.
Trace-length Independent Runtime Monitoring

20th International Symposium on Formal Methods