ICTAC 2010 banner. 1-3 September 2010, Natal, Brazil.


Satellite events:



Formal Methods Europe



Miranda Computação




ICTAC 2010 - Technical Program

The program of ICTAC 2010 includes technical sessions and invited talks and will extend from September 1st, 2010 to September 3rd, 2010. We invite the participants to register and attend to the ICTAC School and to LSFA 2010.

Ana Cavalcanti & David Déharbe (Program Chairs),
Marie-Claude Gaudel & Jim Woodcock (Special Tracks Chairs).

New! Click here to download the PDF with the preliminary programme of ICTAC 2010.

Accepted papers

Bilal Kanso , Marc AIGUIER, Fréderic Boulanger and Assia Touil
Testing of Abstract Components
Lei Chen and Haiming Chen.
Subtyping Algorithm of Regular Tree Grammars with Disjoint Production Rules
Srinivas Nedunuri, Douglas Smith and William R Cook .
A class of greedy algorithms and its relation to greedoids
Carlos Gustavo Lopez Pombo and Marcelo Fabián Frias .
Complete Calculi for Structured Specifications in Fork Algebra
Andrius Velykis and Leo Freitas .
Formal Modelling of Separation Kernel Components
Bas Basten .
Tracking Down the Origins of Ambiguity in Context-Free Grammars
Jewgenij Botaschanjan and Benjamin Hummel .
Material Flow Abstraction of Manufacturing Systems
Ashish Darbari, Bernd Fischer and Joao Marques-Silva .
Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking
Umberto Souza da Costa, Ivan Soares de Medeiros Júnior and Marcel Vinicius Medeiros Oliveira .
Specification and Verification of a MPI Implementation for a MP-SoC
Bill Stoddart, Frank Zeyda and Steve Dunne.
Preference and Non-deterministic Choice
Reng Zeng and Xudong He .
Analyzing a Formal Specification of Mondex using Model Checking
Jacques Chabin, Mirian Halfeld Ferrari , Martin Musicante and Pierre Rety .
Minimal tree language extensions: a keystone of XML type compatibility and evolution
Gregory Malecha and Greg Morrisett.
Mechanized Verification with Sharing
Marcelo Fabián Frias , Carlos Gustavo Lopez Pombo and Mariano Moscato.
Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements
Pablo Castro , Nazareno Aguirre , Carlos Gustavo Lopez Pombo and Tom Maibaum .
Towards Managing Dynamic Reconfiguration of Software Systems in a Categorical Setting
Pablo Castro and Tom Maibaum .
Characterizing Locality (Encapsulation) with Bisimulation
Paul Tarau .
On Arithmetic Computations with Hereditarily Finite Sets, Functions and Types
Andrew Butterfield and Pawel Gancarski.
Prioritised slotted-Circus
Zhenbang Chen and Zhiming Liu .
An Extended cCSP with Stable Failures Semantics
Yunho Kim, Moonzoo Kim and Nam Dang.
Scalable Distributed Concolic Testing: a Case Study on a Flash Storage Platform
Eduardo Bonelli and Francisco Bavera.
Justification Logic and History Based Computation
Rui Shi, Dengping Zhu and Hongwei Xi .
A Modality for Safe Resource Sharing and Code Reentrancy
Qin Li, Huibiao Zhu and Jifeng He .
A Denotational Semantical Model for Orc Language

Invited talks

Paulo Borba
Associate Professor, Centro de Informática, Universidade Federal de Pernambuco
A Theory of Software Product Line Refinement.
Ian Hayes
Professor, School of Information Technology and Electrical Engineering, University of Queensland
FME Invited Lecturer
Invariants and Well-Foundedness in Program Algebra.
Stephan Merz
Researcher, INRIA Lorraine & LORIA
The TLA+ Proof System: Building a Heterogeneous Verification Platform.
Wolfram Schulte
Research Area Manager, Microsoft Research
Verifying Concurrent C: Theory and Practice.