Formal Methods and Software Engineering

1. Front Matter

   PDF

2. Approximations for Stochastic Graph Rewriting

   • Vincent Danos, Tobias Heindel, Ricardo Honorato-Zimmer, Sandro Stucki

   Pages 1-10

3. Computing Maximal Bisimulations

   • Alexandre Boulgakov, Thomas Gibson-Robinson, A. W. Roscoe

   Pages 11-26

4. Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints

   • Simon Busard, Charles Pecheur, Hongyang Qu, Franco Raimondi

   Pages 27-42

5. A Formal Model for Natural-Language Timed Requirements of Reactive Systems

   • Gustavo Carvalho, Ana Carvalho, Eduardo Rocha, Ana Cavalcanti, Augusto Sampaio

   Pages 43-58

6. A Hybrid Model of Connectors in Cyber-Physical Systems

   • Xiaohong Chen, Jun Sun, Meng Sun

   Pages 59-74

7. A Language-Independent Proof System for Mutual Program Equivalence

   • Ştefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roşu

   Pages 75-90

8. PHASE: A Stochastic Formalism for Phase-Type Distributions

   • Gabriel Ciobanu, Armand Stefan Rotaru

   Pages 91-106

9. CASSANDRA: An Online Failure Prediction Strategy for Dynamically Evolving Systems

   • Francesco De Angelis, Maria Rita Di Berardini, Henry Muccini, Andrea Polini

   Pages 107-122

10. Modal Characterisations of Probabilistic and Fuzzy Bisimulations

    • Yuxin Deng, Hengyang Wu

    Pages 123-138

11. Pointer Program Derivation Using Coq: Graphs and Schorr-Waite Algorithm

    • Jean-François Dufourd

    Pages 139-154

12. An LTL Model Checking Approach for Biological Parameter Inference

    • Emmanuelle Gallet, Matthieu Manceny, Pascale Le Gall, Paolo Ballarini

    Pages 155-170

13. SCC-Based Improved Reachability Analysis for Markov Decision Processes

    • Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong

    Pages 171-186

14. Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior

    • Klaus Havelund, Rajeev Joshi

    Pages 187-202

15. Timed Automata Verification via IC3 with Zones

    • Tobias Isenberg, Heike Wehrheim

    Pages 203-218

16. GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems

    • Fatma Jebali, Frédéric Lang, Radu Mateescu

    Pages 219-234

17. A Formal Framework to Prove the Correctness of Model Driven Engineering Composition Operators

    • Mounira Kezadri Hamiaz, Marc Pantel, Benoit Combemale, Xavier Thirioux

    Pages 235-250

18. A Formula-Based Approach for Automatic Fault Localization of Imperative Programs

    • Si-Mohamed Lamraoui, Shin Nakajima

    Pages 251-266

19. A Resource-Based Logic for Termination and Non-termination Proofs

    • Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin

    Pages 267-283

20. Practical Analysis Framework for Software-Based Attestation Scheme

    • Li Li, Hong Hu, Jun Sun, Yang Liu, Jin Song Dong

    Pages 284-299

This book constitutes the refereed proceedings of the 16th International Conference on Formal Engineering Methods, ICFEM 2014, held in Luxembourg, Luxembourg, in November 2014. The 28 revised full papers presented were carefully reviewed and selected from 73 submissions. The papers cover a wide range of topics in the area of formal methods and software engineering and are devoted to advancing the state of the art of applying formal methods in practice. They focus in particular on combinations of conceptual and methodological aspects with their formal foundation and tool support.

• concurrernt systems
• formal approaches to software testing
• formal methods
• formal methods and theory of security
• formal methods in biology and healthcare
• logic and verification
• model checking
• semantics and reasoning
• software certification
• software design and verification
• software reliability
• software safety
• specification languages
• symbolic computations
• system modeling
• algorithm analysis and problem complexity

• Inria Nancy - Grand Est, Villers-lès-Nancy, France

  Stephan Merz

• Université du Luxembourg, Luxembourg, Luxembourg

  Jun Pang

Policies and ethics