IFIP TC6 Open Digital Library

33. FORTE / 15. FMOODS 2013: Florence, Italy

Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Techniques, DisCoTec 2013, Florence, Italy, June 3-5, 2013. Proceedings

Dirk Beyer, Michele Boreale

Springer, Lecture Notes in Computer Science 7892, ISBN: 978-3-642-38591-9


Invited Talk

Analyzing Interactions of Asynchronously Communicating Software Components - (Invited Paper).

Tevfik Bultan


Session 1: Verification

Formal Analysis of a Distributed Algorithm for Tracking Progress.

Martín Abadi, Frank McSherry, Derek Gordon Murray, Thomas L. Rodeheffer


A Case Study in Formal Verification Using Multiple Explicit Heaps.

Wojciech Mostowski


Parameterized Verification of Track Topology Aggregation Protocols.

Sergio Feo Arenis, Bernd Westphal


Session 2: Types

Monitoring Networks through Multiparty Session Types.

Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, Nobuko Yoshida


Semantic Subtyping for Objects and Classes.

Ornela Dardha, Daniele Gorla, Daniele Varacca


Polymorphic Types for Leak Detection in a Session-Oriented Functional Language.

Viviana Bono, Luca Padovani, Andrea Tosatto


Session 3: Testing

Passive Testing with Asynchronous Communications.

Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez


Input-Output Conformance Simulation (iocos) for Model Based Testing.

Carlos Gregorio-Rodríguez, Luis Llana, Rafael Martínez-Torres


Session 4: DisCoTec Joint Session

Model Checking Distributed Systems against Temporal-Epistemic Specifications.

Andreas Griesmayer, Alessio Lomuscio


Session 5: Model Checking

Formal Verification of Distributed Branching Multiway Synchronization Protocols.

Hugues Evrard, Frédéric Lang


An Abstract Framework for Deadlock Prevention in BIP.

Paul C. Attie, Saddek Bensalem, Marius Bozga, Mohamad Jaber, Joseph Sifakis, Fadi A. Zaraket


Bounded Model Checking of Graph Transformation Systems via SMT Solving.

Tobias Isenberg 0002, Dominik Steenken, Heike Wehrheim


Session 6: Automata

Verification of Directed Acyclic Ad Hoc Networks.

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine


Transducer-Based Algorithmic Verification of Retransmission Protocols over Noisy Channels.

Jay Thakkar, Aditya Kanade, Rajeev Alur


Asynchronously Communicating Visibly Pushdown Systems.

Domagoj Babic, Zvonimir Rakamaric


Session 7: Distribution and Concurrency

A Timed Component Algebra for Services.

Benoît Delahaye, José Luiz Fiadeiro, Axel Legay, Antónia Lopes


Probabilistic Analysis of the Quality Calculus.

Hanne Riis Nielson, Flemming Nielson


May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects.

Antonio Flores-Montoya, Elvira Albert, Samir Genaim


Session 8: Security

Lintent: Towards Security Type-Checking of Android Applications.

Michele Bugliesi, Stefano Calzavara, Alvise Spanò


Honesty by Typing.

Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, Roberto Zunino