11. ICFEM 2009: Rio de Janeiro, Brazil

Invited Papers

• Manfred Broy:
  Seamless Model Driven Systems Engineering Based on Formal Models. 1-19
  
• Augusto Sampaio, Sidney Nogueira, Alexandre Mota:
  Compositional Verification of Input-Output Conformance via CSP Refinement Checking. 20-48
  

Testing I

• Margus Veanes, Pavel Grigorenko, Peli de Halleux, Nikolai Tillmann:
  Symbolic Query Exploration. 49-68
  
• Svetoslav R. Ganov, Chip Killmar, Sarfraz Khurshid, Dewayne E. Perry:
  Event Listener Analysis and Symbolic Execution for Testing GUI Applications. 69-87
  
• Junaid Haroon Siddiqui, Sarfraz Khurshid:
  An Empirical Study of Structural Constraint Solving Techniques. 88-106
  

Protocols

• Xihui Chen, Ton van Deursen, Jun Pang:
  Improving Automatic Verification of Security Protocols with XOR. 107-126
  
• Suriadi Suriadi, Chun Ouyang, Jason Smith, Ernest Foo:
  Modeling and Verification of Privacy Enhancing Protocols. 127-146
  
• Péter Bokor, Marco Serafini, Neeraj Suri, Helmut Veith:
  Role-Based Symmetry Reduction of Fault-Tolerant Distributed Protocols with Language Support. 147-166
  

Testing II

• Maximiliano Cristiá, Pablo Rodríguez Monetti:
  Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing. 167-185
  
• Mercedes G. Merayo, Iksoon Hwang, Manuel Núñez, Ana R. Cavalli:
  A Statistical Approach to Test Stochastic and Probabilistic Systems. 186-205
  
• Bernhard K. Aichernig, Harald Brandl, Willibald Krenn:
  Qualitative Action Systems. 206-225
  

Verification

• Paul Taverne, Cornelis Pronk:
  RAFFS: Model Checking a Robust Abstract Flash File Store. 226-245
  
• André Platzer, Jan-David Quesel:
  European Train Control System: A Case Study in Formal Verification. 246-265
  
• David S. Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas Wagner, Michael W. Whalen:
  Development of Security Software: A High Assurance Methodology. 266-285
  

Model Checking I

• Wenhui Zhang:
  Bounded Semantics of CTL and SAT-Based Verification. 286-305
  
• Alessandro Ferrante, Margherita Napoli, Mimmo Parente:
  Graded-CTL: Satisfiability and Symbolic Model Checking. 306-325
  
• Samik Basu, Arka P. Ghosh, Ru He:
  Approximate Model Checking of PCTL Involving Unbounded Path Properties. 326-346
  

Object-Orientation

• Wei Ke, Zhiming Liu, Shuling Wang, Liang Zhao:
  A Graph-Based Operational Semantics of OO Programs. 347-366
  
• Frank S. de Boer, Immo Grabe, Mohammad Mahdi Jaghoori, Andries Stam, Wang Yi:
  Modeling and Analysis of Thread-Pools in an Industrial Communication Platform. 367-386
  
• Wolfgang Ahrendt, Maximilian Dylla:
  A Verification System for Distributed Objects with Asynchronous Method Calls. 387-406
  

Model checking II

• Jiri Barnat, Lubos Brim, Petr Rockai:
  A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. 407-425
  
• Yang Liu, Jun Sun, Jin Song Dong:
  Scalable Multi-core Model Checking Fairness Enhanced Systems. 426-445
  
• Anil Madhavapeddy:
  Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language. 446-465
  

Event-B

• Renato Silva, Michael Butler:
  Supporting Reuse of Event-B Developments through Generic Instantiation. 466-484
  
• Paulo J. Matos, Bernd Fischer, João P. Marques Silva:
  A Lazy Unbounded Model Checker for Event-B. 485-503
  
• Jens Bendisposto, Michael Leuschel:
  Proof Assisted Model Checking for B. 504-520
  

Compilation

• Nassima Izerrouken, Marc Pantel, Xavier Thirioux:
  Machine-Checked Sequencer for Critical Embedded Code Generator. 521-540
  
• Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet:
  Implementing a Direct Method for Certificate Translation. 541-560
  

Process Algebra

• Antti Siirtola, Juha Kortelainen:
  Algorithmic Verification with Multiple and Nested Parameters. 561-580
  
• Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang:
  Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction. 581-600
  

Refinement

• Fernando Luís Dotti, Alexei Iliasov, Leila Ribeiro, Alexander Romanovsky:
  Modal Systems: Specification, Refinement and Realisation. 601-619
  
• Thomas Ruhroth, Heike Wehrheim:
  Refinement-Preserving Co-evolution. 620-638
  

Algebraic Specifications

• Dorel Lucanu, Grigore Rosu:
  Circular Coinduction with Special Contexts. 639-659
  
• Mihai Codescu, Bruno Langenstein, Christian Maeder, Till Mossakowski:
  The VSE Refinement Method in Hets. 660-678
  

Real-Time Systems

• Nathalie Bertrand, Axel Legay, Sophie Pinchinat, Jean-Baptiste Raclet:
  A Compositional Approach on Modal Specifications for Timed Systems. 679-697
  
• Joakim Byg, Kenneth Yrke Jørgensen, Jirí Srba:
  An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata. 698-716
  
• Kyungmin Bae, Peter Csaba Ölveczky, Thomas Huining Feng, Stavros Tripakis:
  Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude. 717-736
  
• Germán Regis, Nazareno Aguirre, T. S. E. Maibaum:
  Specifying and Verifying Business Processes Using PPML. 737-756
  

Last update Fri May 24 02:54:34 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page