6. SEFM 2008: Cape Town, South Africa

Tutorial

• Roberto Giacobazzi:
  Abstract Interpretation in Code Security. 3
  

Keynote Speaker 1

• Roberto Giacobazzi:
  Hiding Information in Completeness Holes: New Perspectives in Code Obfuscation and Watermarking. 7-18
  

Abstract Interpretation

• Fausto Spoto:
  Nullness Analysis in Boolean Form. 21-30
  
• Agostino Cortesi:
  Widening Operators for Abstract Interpretation. 31-40
  
• Pietro Ferrara:
  Static Analysis of the Determinism of Multithreaded Programs. 41-50
  

Model Checking

• Henri Hansen, Jaco Geldenhuys:
  Cheap and Small Counterexamples. 53-62
  
• Martin Fränzle, Michael R. Hansen:
  Efficient Model Checking for Duration Calculus Based on Branching-Time Approximations. 63-72
  
• Stefan Edelkamp, Damian Sulewski:
  Flash-Efficient LTL Model Checking with Minimal Counterexamples. 73-82
  

Verification of Embedded Systems

• Peter Höfner, Ridha Khédri, Bernhard Möller:
  Algebraic View Reconciliation. 85-94
  
• Ina Schaefer, Arnd Poetzsch-Heffter:
  Compositional Reasoning in Model-Based Verification of Adaptive Embedded Systems. 95-104
  

Security

• Michael Carl Tschantz, Jeannette M. Wing:
  Extracting Conditional Confidentiality Policies. 107-116
  
• Percy Antonio Pari Salas, Padmanabhan Krishnan:
  Testing Privacy Policies Using Models. 117-126
  
• Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese:
  Preservation of Proof Pbligations for Hybrid Verification Methods. 127-136
  

Testing I

• Adilson Luiz Bonifácio, Arnaldo Vieira Moura, Adenilso da Silva Simão:
  A Generalized Model-Based Test Generation Method. 139-148
  
• Temesghen Kahsai, Markus Roggenbach, Bernd-Holger Schlingloff:
  Specification-Based Testing for Software Product Lines. 149-158
  
• Christoph Gladisch:
  Verification-Based Test Case Generation for Full Feasible Branch Coverage. 159-168
  

Testing II

• Puneet Bhateja, Madhavan Mukund:
  Tagging Make Local Testing of Message-Passing Systems Feasible. 171-180
  
• Kleber S. Xavier, Simone Hanazumi, Ana Cristina Vieira de Melo:
  Using Formal Verification to Reduce Test Space of Fault-Tolerant Programs. 181-190
  
• Prahladavaradan Sampath, A. C. Rajeev, S. Ramesh, K. C. Shashidhar:
  Behaviour Directed Testing of Auto-code Generators. 191-200
  
• Mercedes G. Merayo, Robert M. Hierons, Manuel Núñez:
  Extending Stream X-Machines to Specify and Test Systems with Timeouts. 201-210
  

Keynote Speaker 2

• Markus Roggenbach:
  Tools for CSP. 213-214
  

Aspect-Oriented Development

• Leila Silva, Augusto Sampaio, Zhiming Liu:
  Laws of Object-Orientation with Reference Semantics. 217-226
  
• Simplice Djoko Djoko, Rémi Douence, Pascal Fradet:
  Specialized Aspect Languages Preserving Classes of Properties. 227-236
  
• Valentin Goranko, Dmitry Shkatov:
  Tableau-Based Decision Procedure for the Multi-agent Epistemic Logic with Operators of Common and Distributed Knowledge. 237-246
  

Requirement and Program Analysis

• Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta:
  Object Models with Temporal Constraints. 249-258
  
• Tuan-Hung Pham, Anh-Hoang Truong, Ninh-Thuan Truong, Wei-Ngan Chin:
  A Fast Algorithm to Compute Heap Memory Bounds of Java Card Applets. 259-267
  
• Gogul Balakrishnan, Malay Ganai:
  PED: Proof-Guided Error Diagnosis by Triangulation of Program Error Causes. 268-278
  

Tool Papers

• M. Oliveira, Alessandro Cavalcante Gurgel, Cristiano Gurgel de Castro:
  CRefine: Support for the Circus Refinement Calculus. 281-290
  
• Eduardo Tavares, Bruno Silva, Paulo Romero Martins Maciel:
  An Environment for Measuring and Scheduling Time-Critical Embedded Systems with Energy Constraints. 291-300
  

Coordination Languages

• Mohammad Izadi, Marcello M. Bonsangue, Dave Clarke:
  Modeling Component Connectors: Synchronisation and Context-Dependency. 303-312
  
• Gwen Salaün:
  Generation of Service Wrapper Protocols from Choreography Specifications. 313-322
  
• Ivan Lanese, Claudio Guidi, Fabrizio Montesi, Gianluigi Zavattaro:
  Bridging the Gap between Interaction- and Process-Oriented Choreographies. 323-332
  

Communication, Mobile and Interactive Systems

• Bo Guo, Mahadevan Subramaniam:
  Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover. 335-344
  
• Fatemeh Ghassemi, Wan Fokkink, Ali Movaghar:
  Restricted Broadcast Process Theory. 345-354
  
• Rimvydas Ruksenas, Paul Curzon, Ann Blandford:
  Modelling Rational User Behaviour as Games between an Angel and a Demon. 355-364
  

Short Papers

• Alexander K. Petrenko, Olga L. Petrenko:
  Formal Methods and Innovation Economy: Facing New Challenges. 367-371
  
• Youcef Hammal:
  Behavioral Compatibility of Active Components. 372-376
  
• Sophie Quinton, Susanne Graf:
  Contract-Based Verification of Hierarchical Systems of Components. 377-381
  
• Anh-Hoang Truong, Thanh-Binh Trinh, Dang Van Hung, Viet-Ha Nguyen, Nguyen Thi Thu Trang, Pham Dinh Hung:
  Checking Interface Interaction Protocols Using Aspect-Oriented Programming. 382-386
  
• Kurt Geihs, Philipp A. Baer, Roland Reichle, Jens Wollenhaupt:
  Ontology-Based Automatic Model Transformations. 387-391