4. ICTAC 2007: Macau, China

• Dines Bjørner:
  Domain Theory: Practice and Theories A Discussion of Possible Research Topics. 1-17
  
• Jifeng He:
  Linking Semantic Models. 18-33
  
• Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, Chaochen Zhou:
  Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. 34-49
  
• Bogdan Aman, Gabriel Ciobanu:
  Mobile Ambients with Timers and Types. 50-63
  
• Damián Barsotti, Javier O. Blanco:
  Automatic Refinement of Split Binary Semaphore. 64-78
  
• Pontus Boström, Lionel Morel, Marina A. Waldén:
  Stepwise Development of Simulink Models Using the Refinement Calculus Framework. 79-93
  
• Zining Cao:
  Bisimulations for a Distributed Higher Order pi -Calculus. 94-108
  
• Pablo F. Castro, T. S. E. Maibaum:
  A Complete and Compact Propositional Deontic Logic. 109-123
  
• Robert Colvin, Brijesh Dongol:
  Verifying Lock-Freedom Using Well-Founded Orders. 124-138
  
• Pascal Coupey, Christophe Fouqueré, Jean-Vincent Loddo:
  Tree Components Programming: An Application to XML. 139-153
  
• Fredrik Degerlund, Kaisa Sere:
  A Framework for Incorporating Trust into Formal Systems Development. 154-168
  
• Rafael del Vado Vírseda:
  A Higher-Order Demand-Driven Narrowing Calculus with Definitional Trees. 169-184
  
• Catalin Dima, Ruggero Lanotte:
  Distributed Time-Asynchronous Automata. 185-200
  
• John Fisher, Marc Bezem:
  Skolem Machines and Geometric Logic. 201-215
  
• Christophe Fouqueré:
  A Logical Calculus for Modelling Interferences. 216-230
  
• Ignacio Fábregas, Miguel Palomino, David de Frutos-Escrig:
  Reflection and Preservation of Properties in Coalgebraic (bi)Simulations. 231-245
  
• Takashi Kitamura, Huimin Lin:
  Controlling Process Modularity in Mobile Computing. 246-259
  
• Brian Randell, Maciej Koutny:
  Failures: Their Definition, Modelling and Analysis. 260-274
  
• Alessandro Lapadula, Rosario Pugliese, Francesco Tiezzi:
  C-clock-WS: A Timed Service-Oriented Calculus. 275-290
  
• Martin Leucker, César Sánchez:
  Regular Linear Temporal Logic. 291-305
  
• Jing Li, Huibiao Zhu, Jifeng He:
  Algebraic Semantics for Compensable Transactions. 306-321
  
• Wanwei Liu, Ji Wang, Wei Dong, Huowang Chen:
  Axiomatizing Extended Temporal Logic Fragments Via Instantiation. 322-336
  
• Xinxin Liu, Haiyan Chen:
  Deciding Weak Bisimilarity of Normed Context-Free Processes Using Tableau. 337-350
  
• Roussanka Loukanova:
  Linear Context Free Languages. 351-365
  
• Andrea Matta, Matteo Rossi, Paola Spoletini, Dino Mandrioli, Quirico Semeraro, Tullio Tolio:
  FM for FMS: Lessons Learned While Applying Formal Methods to the Study of Flexible Manufacturing Systems. 366-380
  
• Masaki Nakamura, Kokichi Futatsugi:
  On Equality Predicates in Algebraic Specification Languages. 381-395
  
• Virginia Niculescu:
  Data-Distributions in PowerList Theory. 396-409
  
• Guillaume Bonfante, Jean-Yves Marion, Romain Péchoux:
  Quasi-interpretation Synthesis by Decomposition. 410-424
  
• Thomas Noll, Stefan Rieger:
  Composing Transformations to Optimize Linear Code. 425-439
  
• Silvio Ranise, Christelle Scharff:
  Building Extended Canonizers by Graph-Based Deduction. 440-454
  
• K. Subramani:
  A Randomized Algorithm for BBCSPs in the Prover-Verifier Model. 455-466
  
• Zhilin Wu:
  On the Expressive Power of QLTL. 467-481