default search action
FM 2016: Limassol, Cyprus
- John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, Anna Philippou:
FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science 9995, 2016, ISBN 978-3-319-48988-9
Invited Presentations
- Jan Peleska, Wen-ling Huang:
Industrial-Strength Model-Based Testing of Safety-Critical Systems. 3-22
Research Track
- Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep:
Counter-Example Guided Program Verification. 25-42 - Pedro R. G. Antonino, Thomas Gibson-Robinson, A. W. Roscoe:
Tighter Reachability Criteria for Deadlock-Freedom Analysis. 43-59 - Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess:
Compositional Parameter Synthesis. 60-68 - Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews, Thomas Tuerk:
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor. 69-84 - Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safránek:
A Model Checking Approach to Discrete Bifurcation Analysis. 85-101 - Stanislav Böhm, Ondrej Meca, Petr Jancar:
State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI. 102-118 - Saksham Chand, Yanhong A. Liu, Scott D. Stoller:
Formal Verification of Multi-Paxos for Distributed Consensus. 119-136 - Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan:
Validated Simulation-Based Verification of Delayed Differential Dynamics. 137-154 - Yuqi Chen, Christopher M. Poskitt, Jun Sun:
Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation. 155-163 - Alessandro Cimatti, Sergio Mover, Mirko Sessa:
From Electrical Switched Networks to Hybrid Automata. 164-181 - Cristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis:
Danger Invariants. 182-198 - Mahieddine Dellabani, Jacques Combaz, Marius Bozga, Saddek Bensalem:
Local Planning of Multiparty Interactions with Bounded Horizons. 199-216 - Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski:
Finding Suitable Variability Abstractions for Family-Based Analysis. 217-234 - Adel Djoudi, Sébastien Bardin, Éric Goubault:
Recovering High-Level Conditions from Binary Programs. 235-253 - Antonio Flores-Montoya:
Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations. 254-273 - Dimitra Giannakopoulou, Dennis Guck, Johann Schumann:
Exploring Model Quality for ACAS X. 274-290 - Georgios Giantamidis, Stavros Tripakis:
Learning Moore Machines from Input-Output Traces. 291-309 - Victor B. F. Gomes, Georg Struth:
Modal Kleene Algebra Applied to Program Correctness. 310-325 - Gudmund Grov, Yuhui Lin, Vytautas Tumas:
Mechanised Verification Patterns for Dafny. 326-343 - Miran Hasanagic, Peter W. V. Tran-Jørgensen, Kenneth Lausdahl, Peter Gorm Larsen:
Formalising and Validating the Interface Description in the FMI Standard. 344-351 - Ian J. Hayes, Robert J. Colvin, Larissa A. Meinicke, Kirsten Winter, Andrius Velykis:
An Algebra of Synchronous Atomic Steps. 352-369 - Andreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies:
Error Invariants for Concurrent Traces. 370-387 - Zhe Hou, David Sanán, Alwen Tiu, Yang Liu, Koh Chuen Hoa:
An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 Processor. 388-405 - Yusuke Kawamoto, Fabrizio Biondi, Axel Legay:
Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow. 406-425 - Artem Khyzha, Alexey Gotsman, Matthew J. Parkinson:
A Generic Logic for Proving Linearizability. 426-443 - Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden:
Refactoring Refinement Structure of Event-B Machines. 444-459 - Pingfan Kong, Yi Li, Xiaohong Chen, Jun Sun, Meng Sun, Jingyi Wang:
Towards Concolic Testing for Hybrid Systems. 460-478 - Ori Lahav, Viktor Vafeiadis:
Explaining Relaxed Memory Models with Program Transformations. 479-495 - Thomas Letan, Pierre Chifflier, Guillaume Hiet, Pierre Néron, Benjamin Morin:
SpecCert: Specifying and Verifying Hardware-Based Security Enforcement. 496-512 - Li Li, Jun Sun, Jin Song Dong:
Automated Verification of Timed Security Protocols with Clock Drift. 513-530 - Claudio Menghi, Paola Spoletini, Carlo Ghezzi:
Dealing with Incompleteness in Automata-Based Model Checking. 531-550 - Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening, Tom Melham:
Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. 551-558 - Morten Bisgaard, David Gerhardt, Holger Hermanns, Jan Krcál, Gilles Nies, Marvin Stenger:
Battery-Aware Scheduling in Low Orbit: The GomX-3 Case. 559-576 - Heinrich Ody, Martin Fränzle, Michael R. Hansen:
Discounted Duration Calculus. 577-592 - Bat-Chen Rothenberg, Orna Grumberg:
Sound and Complete Mutation-Based Program Repair. 593-611 - Christoph-Simon Senjak, Martin Hofmann:
An Implementation of Deflate in Coq. 612-627 - Andrew Sogokon, Khalil Ghorbal, Taylor T. Johnson:
Decoupling Abstractions of Non-linear Ordinary Differential Equations. 628-644 - Ofer Strichman, Maor Veitsman:
Regression Verification for Unbalanced Recursive Functions. 645-658 - Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei-Ngan Chin:
Automated Mutual Explicit Induction Proof in Separation Logic. 659-676 - Amirhossein Vakili, Nancy A. Day:
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions. 677-693 - Anton Wijs, Thomas Neele, Dragan Bosnacki:
GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking. 694-701 - Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan:
Approximate Bisimulation and Discretization of Hybrid CSP. 702-720 - Zhengfeng Yang, Chao Huang, Xin Chen, Wang Lin, Zhiming Liu:
A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems. 721-738
Industry Track
- Roberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna, Stefano Tonetta:
Model-Based Design of an Energy-System Embedded Controller Using Taste. 741-747 - Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz, Henrik Lönn:
Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems. 748-756 - Yu Jiang, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, Lui Sha:
Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller. 757-763 - Han Liu, Yu Jiang, Huafeng Zhang, Ming Gu, Jiaguang Sun:
Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers. 764-771 - Bjørnar Luteberget, Christian Johansen, Claus Feyling, Martin Steffen:
Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations. 772-778 - Teodor Stoenescu, Alin Stefanescu, Sorina Predut, Florentin Ipate:
RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions. 779-785
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.