default search action
FM 2015: Oslo, Norway
- Nikolaj S. Bjørner, Frank S. de Boer:
FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. Lecture Notes in Computer Science 9109, Springer 2015, ISBN 978-3-319-19248-2
Invited Presentations
- Elvira Albert, Puri Arenas, Jesús Correas
, Samir Genaim
Resource Analysis: From Sequential to Concurrent and Distributed Programs. 3-17 - Werner Damm:
AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned. 18-19
Main Track
- Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham
Automated Circular Assume-Guarantee Reasoning. 23-39 - Musab A. AlTurki
Towards Formal Verification of Orchestration Computations Using the 핂 Framework. 40-56 - Gianluca Amato
Narrowing Operators on Template Abstract Domains. 57-72 - Hamid Bagheri, Eunsuk Kang, Sam Malek, Daniel Jackson:
Detection of Design Flaws in the Android Permission Protocol Through Bounded Verification. 73-89 - Julien Bringer, Hervé Chabanne, Daniel Le Métayer, Roch Lescuyer:
Privacy by Design in Practice: Reasoning about Privacy Properties of Biometric System Architectures. 90-107 - Wolfgang Ahrendt
A Specification Language for Static and Runtime Verification of Data and Control Properties. 108-125 - Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi:
Certificates for Parameterized Model Checking. 126-142 - Søren Debois
Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes. 143-160 - John Derrick
Verifying Opacity of a Transactional Mutex Lock. 161-177 - John Derrick
A Framework for Correctness Criteria on Weak Memory Models. 178-194 - Cornelius Diekmann
Semantics-Preserving Simplification of Real-World Firewall Rule Sets. 195-212 - Thao Dang, Tommaso Dreossi, Carla Piazza
Parameter Synthesis Through Temporal Logic Specifications. 213-230 - Xiaoning Du, Yang Liu
Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL. 231-247 - Christian Eisentraut, Jens Chr. Godskesen, Holger Hermanns, Lei Song, Lijun Zhang:
Probabilistic Bisimulation for Realistic Schedulers. 248-264 - Yuan Feng
QPMC: A Model Checker for Quantum Programs and Protocols. 265-272 - Matthew Fernandez, June Andronick, Gerwin Klein
Automated Verification of RPC Stub Code. 273-290 - Saurabh Joshi, Daniel Kroening
Property-Driven Fence Insertion Using Reorder Bounded Model Checking. 291-307 - Guillaume Brat, David H. Bushnell, Misty D. Davies
Verifying the Safety of a Flight-Critical System. 308-324 - Daniel Kroening
Proving Safety with Trace Automata and Bounded Model Checking. 325-341 - Li Li, Jun Sun
Verifying Parameterized Timed Security Protocols. 342-359 - Jiang Liu, Naijun Zhan, Hengjun Zhao, Liang Zou:
Abstraction of Elementary Hybrid Systems by Variable Transformation. 360-377 - Shin Nakajima:
Using Real-Time Maude to Model Check Energy Consumption Behavior. 378-394 - Tim Nelson
Static Differential Program Analysis for Software-Defined Networks. 395-413 - Nadia Polikarpova, Julian Tschannen, Carlo A. Furia:
A Fully Verified Container Library. 414-434 - Tim Quatmann
Counterexamples for Expected Rewards. 435-452 - Aliakbar Safilian, Tom Maibaum, Zinovy Diskin:
The Semantics of Cardinality-Based Feature Models via Formal Languages. 453-469 - Peter H. Schmitt, Mattias Ulbrich
Axiomatization of Typed First-Order Logic. 470-486 - David Schneider, Michael Leuschel, Tobias Witt:
Model-Based Problem Solving for University Timetable Validation and Improvement. 487-495 - Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, Wei-Ngan Chin:
Certified Reasoning with Infinity. 496-513 - Andrew Sogokon, Paul B. Jackson
Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems. 514-531 - Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan:
Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. 532-550 - Xueyang Zhu
Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking. 551-569
Industry Track
- Bharti Chimdyalwar, Priyanka Darke, Anooj Chavda, Sagar Vaghani, Avriti Chauhan:
Eliminating Static Analysis False Positives Using Loop Abstraction and Bounded Model Checking. 573-576 - William Durand, Sébastien Salva:
Autofunk: An Inference-Based Formal Model Generation Framework for Production Systems. 577-580 - Neil Evans:
Software Development and Authentication for Arms Control Information Barriers. 581-584 - Stefan Hauck-Stattelmann, Sebastian Biallas, Bastian Schlich, Stefan Kowalewski, Raoul Jetley:
Analyzing the Restart Behavior of Industrial Control Applications. 585-588 - Tao Liu, Ralf Huuck:
Case Study: Static Security Analysis of the Android Goldfish Kernel. 589-592 - Taro Kurita, Fuyuki Ishikawa, Keijiro Araki:
Practices for Formal Models as Documents: Evolution of VDM Application to "Mobile FeliCa" IC Chip Firmware. 593-596 - Thierry Lecomte
Formal Virtual Modelling and Data Verification for Supervision Systems. 597-600 - Bruno Miranda, Henrique Masini, Rodrigo Reis:
Using Simulink Design Verifier for Automatic Generation of Requirements-Based Tests. 601-604 - Mathijs Schuts, Jozef Hooman:
Formalizing the Concept Phase of Product Development. 605-608
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-26 00:35 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: