Invited Talks
ICLP 2005 will include the following three invited talks:
OWL:
a Description Logic Based Ontology Language
Ian
Horrocks
Preference
Reasoning
Francesca
Rossi
The
G12 Project: Mapping Solver Independent Models to Efficient Solutions
PeterStuckey
ICLP 2005 will include the following tutorial:
Challenges
in Learning Logic Programs: From Inductive Logic Programming (ILP) to
Statistical
Relational Learning (SRL)
Vitor
Santos Costa
Use of Logic Programming for Complex Business RulesAccepted Posters:
Walter Wilson
Semantics of Framed Temporal Logic Programs
Zhenhua Duan, Xiaoxiao Yang and Maciej Koutny.
On the relation between Answer Set and SAT procedures (or, between smodels and cmodels)
Enrico Giunchiglia and Marco Maratea.
HYPROLOG: a new logic programming language with assumptions and abduction
Henning Christiansen and Veronica Dahl.
A Generator of Efficient Abstract Machine Implementations and its Application to Emulator Minimization
Jose Morales, Manuel Carro, German Puebla and Manuel Hermenegildo.
Nondeterminism Analysis of Functional Logic Programs
Bernd Brabel and Michael Hanus.
Testing for Termination with Size Change Graphs
Michael Codish, Vitaly Lagoon and Peter Stuckey.
Towards an Integration of Answer Set and Constraint Solving
Sabrina Baselice, Piero A. Bonatti and Michael Gelfond.
Symbolic Support Graph: A Space Efficient Data Structure For Incremental Tabled Evaluation
Diptikalyan Saha and C. R. Ramakrishnan.
Towards Implementations for Advanced Equivalence Checking in Answer-Set Programming
Hans Tompits and Stefan Woltran.
Hybrid Probabilistic Logic Programs With Non-monotonic Negation
Emad Saad and Enrico Pontelli.
Reducing Inductive Definitions to Propositional Satisfiability
Nikolay Pelov and Eugenia Ternovska.
A Comparison of CLP(FD) and ASP Solutions to NP-Complete Problems
Agostino Dovier, Andrea Formisano and Enrico Pontelli.
A Well-Founded Semantics with Disjunction
Joao Alcantara, Carlos Damasio and Luis Moniz Pereira.
An optimised Semantic Web query language implementation in Prolog
Jan Wielemaker.
Practical Higher-Order Pattern Unification via On-the-Fly Raising
Gopalan Nadathur and Natalie Linnell.
Dynamic Mixed-Strategy Evaluation of Tabled Logic Programs
Ricardo Rocha, Fernando Silva and Vitor Santos Costa.
Small proof witnesses for LF
Susmit Sarkar, Brigitte Pientka and Karl Crary.
Guard and Continuation Optimization for Occurrence Representations of CHR
Jon Sneyers, Tom Schrijvers and Bart Demoen.
Abduction of Linear Arithmetic Constraints
Michael Maher.
Coordination of Many Agents
Joxan Jaffar, Roland Yap and Kenny Zhu.
Parallelizing Union-Find in Constraint Handling Rules Using Confluence
Thom Fruehwirth.
Luca Bortolussi and Herbert Wiklicky.
A Distributed and Probabilistic Concurrent Constraint Programming Language
Deductive Multi-valued Model Checking
Ajay Mallya.
Techniques for Scaling Up Analyses Based on Pre-Interpretations
John P. Gallagher, Kim Henriksen and Gourinath Banda.
Polynomial Interpretations as a Basis for Termination An
Manh Thang Nguyen and Danny De Schreye.
Inconsistency-based Strategy For Clarifying Vague Software Requirements
Kedian Mu, Zhi Jin and Ruqian Lu.
A Type System for CHR
Emmanuel Coquery and Francois Fages.
Decision Support for Personalization on Mobile Devices
Thomas Kleemann and Alex Sinner.
Algorithms for FO(ID) model generation
Maarten Marikn, Rudradeb Mitra and Marc Denecker.
Abstract Interpretation with Specialized Definitions
German Puebla, Elvira Albert and Manuel Hermenegildo.
Induction of causal ramifications for action descriptions in ASP
Ramon Otero.
The need for Ancestor Resolution when answering queries in Horn Clause Logic
Oliver Ray.
Modeling Systems in CLP with Coinductive Tabling
Joxan Jaffar, Andrew Edward Santosa and Razvan Voicu.
A Sufficient Condition for Strong Equivalence under the Well-Founded Semantics
Chistos Nomikos, Panos Rondogiannis and William Wadge.
Analyses, Optimizations and Extensions of Constraint Handling Rules: Ph.D. Summary
Tom Schrijvers.
IMPACT: Innovative Models for Prolog with Advanced Control and Tabling
Ricardo Rocha, Ricardo Lopes, Fernando Silva and Vitor Santos Costa.
Using CLP to characterise linguistic lattice boundaries in a text mining process
Alexandre Saidi.
Hybridization of Genetic Algorithms and Constraint Propagation for the BACP
Tony Lambert, Carlos Castro, Eric Monfroy, Maria Cristina Riff and Fridiric Saubion.
The MYDDAS Project: Using a Deductive Database for Traffic Characterization
Michel Ferreira.
Open World Reasoning in Datalog
Gergely Lukacsy and Zsolt Nagy.
Optimizing Queries for Heterogeneous Information Sources
Andras Gyvrgy Bikis.
Denotational semantics using Horn Concurrent Transaction Logic
Marcus Santos.
Gentra4cp: a Generic Trace Format for Constraint Programming
Ludovic Langevine and The OADymPPaC team.
Invited Talks
CP 2005 will include the following four invited talks:
Inference
and Search in AI Planning
Hector
Geffner
OWL:
a Description Logic Based Ontology Language
Ian
Horrocks
Preference
Reasoning
Francesca
Rossi
The
G12 Project: Mapping Solver Independent Models to Efficient Solutions
PeterStuckey
The last three talks will be shared with the ICLP 2005 conference.
Tutorial Program
CP 2005 will include the following tutorials:
SAT
solving and its relationship to CSPs
Fahiem
Bacchus
Advances
in Search, Inference and Hybrids for Solving Combinatorial Optimization
Tasks
Rina
Dechter
Constraint
Handling Rules: Programming with a Chinese Horse
Thom
Fruehwirth
Complete
Randomized Backtrack Search Methods: Connections to Fat and
Heavy-tailed
distribution and Restart Strategies
Carla
Gomes
Accepted Papers
2-way vs D-way Branching for CSP
Joey Hwang and David G. Mitchell
A Linear-Logic Semantics for Constraint Handling Rules
Hariolf BETZ, Thom Fruhwirth
AC-*: A Configurable, Generic and Adaptive Arc Consistency Algorithm
Jean-Charles Regin
Ad-hoc Global Constraints for Life
Kenil C.K. Cheng, Roland H.C. Yap
Advances in Polytime Isomorph Elimination for Configuration
Laurent Henocque, Mathias Kleiner and Nicolas Prcovic
Allocation and Scheduling for MPSoCs via decomposition and no-good generation
L. Benini, D. Bertozzi, A. Guerri, M. Milano
Applying Constraint Programming to Rigid Body Protein Docking
Ludwig Krippahl and Pedro Barahona
Assumption-Based Pruning in Conditional CSP
Felix Geller and Michael Veksler
Automatic detection of variable and value symmetries
Jean-Francois Puget
Beyond Hypertree Width: Decomposition Methods Without Decompositions
Hubie Chen and Victor Dalmau
Boosting Distributed Constraint Satisfaction
Georg Ringwelski and Youssef Hamadi
Breaking All Value Symmetries in Surjection Problems
Jean-Francois Puget
Caching Search States in Permutation Problems
Barbara M. Smith
Conditional Symmetry Breaking
Ian P. Gent Tom Kelsey Steve A. Linton Iain McDonald Ian Miguel Barbara Smith
CP(Graph): Introducing a Graph Computation Domain in Constraint Programming
Gregoire Dooms, Yves Deville and Pierre Dupont
Depth-First Mini-Bucket Elimination
Emma Rollon and Javier Larrosa
Distributed stable matching problems
Ismel Brito, Pedro Meseguer
Dynamic Ordering for Asynchronous Backtracking on DisCSPs
Roie Zivan and Amnon Meisels
Eplex: An Interface to Mathematical Programming Solvers for Constraint Logic Programming Languages
Kish Shen, Joachim Schimpf
Exploiting Unit Propagation in Max-SAT
Chu Min Li, Felip Manya and Jordi Planes
Factor analytic studies of CSP heuristics
Richard J. Wallace
Generalized Conflict Learning for Hybrid Discrete/Linear Optimization
Hui Li and Brian Williams
Generating Corrective Explanations for Interactive Constraint Satisfaction
Barry O'Callaghan, Barry O'Sullivan, and Eugene C. Freuder
Graph Invariants as Necessary Conditions for Global Constraints
Nicolas Beldiceanu, Mats Carlsson, Jean-Xavier Rampon, Charlotte Truchet
Handling Implication and Universal Quantification Constraints in FLUX
Michael Thielscher
Incremental Algorithms for Local Search from Second-Order Logic
Magnus Agren, Pierre Flener, and Justin Pearson
Inter-Distance Constraint: An Extension of the All-Different Constraint for Scheduling Equal Length Jobs
Konstantin Artiouchine and Philippe Baptiste
Interval analysis in scheduling
Jerome Fortin, Pawel Zielinski, Didier Dubois, Helene Fargier
Maintaining arc consistency algorithms during the search without additional cost
Jean-Charles Regin
Maintaining Longest Paths In Cyclic Graphs
Irit Katriel and Pascal Van Hentenryck
Maximum constraint satisfaction on diamonds
Andrei Krokhin and Benoit Larose
Mind The Gaps: A New Splitting Strategy for Consistency Techniques
Heikel Batnini, Claude Michel and Michel Rueher
Nonlinear Constrained Optimization through Constraint Partitioning
Benjamin W. Wah and Yixin Chen
On Solving Soft Temporal Constraints using SAT Techniques
Hossein M. Sheini, Bart Peintner, Karem A. Sakallah and Martha E. Pollack
Parallel Local Search in Comet
Laurent Michel and Pascal Van Hentenryck
Planning and Scheduling to Minimize Tardiness
J. N. Hooker
Repair-based Methods for Quantified CSPs
Kostas Stergiou
Search Heuristics and Heavy-Tailed Behaviour
Tudor Hulubei and Barry O'Sullivan
Solving Simple Planning Problems with More Inference and No Search
Vincent Vidal and Hector Geffner
Solving the MOLR and Social Golfers Problems
Warwick Harvey and Thorsten Winterer
Spread: A Balancing Constraint Based on Statistics
Gilles Pesant and Jean-Charles Regin
Sub-Optimality Approximations
Russell Bent, Irit Katriel, and Pascal Van Hentenryck
Symmetry and Consistency
I.P. Gent, Tom Kelsey, Steve Linton, Colva Roney-Dougal
Symmetry Definitions for Constraint Satisfaction Problems
David Cohen, Peter Jeavons, Christopher Jefferson, Karen E. Petrie, Barbara M. Smith
Tractable Clones of Polynomials over Semigroups
Victor Dalmau, Ricard Gavalda, Pascal Tesson, and Denis Therien
Tree decomposition with function filtering
Marti Sanchez, Javier Larrosa, Pedro Meseguer
Using SAT in QBF
Horst Samulowitz and Fahiem Bacchus
Weak Composition for Qualitative Spatial and Temporal Reasoning
Jochen Renz, Gerard Ligozat
Accepted Posters
A Different Round Robin Constraint for Sports Scheduling
Laurent Perron
A Generic Framework for Learning Implied Constraints
Christian Bessiere, Remi Coletta and Thierry Petit
Approximate Constrained Pattern Matching
Zampelli Stephane, Yves Deville and Pierre Dupont
Approximated Consistency for the Automatic Recording Constraint
Meinolf Sellmann
Approximations in Distributed Optimization
Adrian Petcu and Boi Faltings
Benders decomposition in Constraint Programming
Hadrien Cambazard and Narendra Jussien
Beyond Finite Domains: the All Different and Global Cardinality Constraints
Claude-Guy Quimper and Toby Walsh
Bounds of Graph Characteristics
Nicolas Beldiceanu, Thierry Petit, Guillaume Rochart
Computing and exploiting tree-decompositions for solving constraint networks
Philippe Jegou and Samba Ndojh Ndiaye and Cyril Terrioux
Consistency for Quantified Constraint Satisfaction Problems
Peter Nightingale
Encoding Requests to Web Service Compositions as Constraints
Alexander Lazovik, Marco Aiello, Rosella Gennari
Evolving Variable-Ordering Heuristics for Constrained Optimisation
Stuart Bain, John Thornton, Abdul Sattar
Extending Systematic Local Search for Job Shop Scheduling Problems
Bistra Dilkina, Lei Duan and William S. Havens
Extremal CSPs
Nicolas Prcovic
Interactive Reconfiguration in Power Supply Restoration
Tarik Hadzic, Henrik Reif Andersen
Lookahead Saturation with Restriction for SAT
Anbulagan and John Slaney
Multi-Point Constructive Search
J. Christopher Beck
Neighbourhood Clause Weight Redistribution in Local Search for SAT
Abdelraouf Ishtaiwi, John Thornton, Abdul Sattar and Duc Nghia Pham
Test Instance Generation for MAX 2SAT
Mitsuo Motoki
Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
Carsten Sinz
Using Boolean Constraint Propagation for Sub-clause Deduction
S. Darras, G. Dequen, L. Devendeville, B. Mazure, R. Ostrowski, L. Sais
Views and Iterators for Generic Constraint Implementations
Christian Schulte and Guido Tack
Pruning
Extensional Predicates in Deductive Databases
Tiago Soares, Ricardo Rocha and
Michel Ferreira
Functional
Notation and Lazy Evaluation in Ciao
Amadeo Casas, Daniel Cabeza and
Manuel Hermenegildo
Views
and Iterators for Generic Constraint Implementations
Christian Schulte and Guido Tack
Closures
for Closed Module Systems
Rémy
Haemmerlé and François Fages
Speeding
up constrained path solvers with a reachability propagator
Luis Quesada, Peter Van
Roy,Yves Deville
| 9:30 | Opening Comments | Jim Lipton |
| 10:00 | Invited Talk: Abstract Interpretation-based Verification/Certification in the CiaoPP System | German Puebla Elvira Albert Manuel Hermenegildo |
| 10:45 | Break | |
| 11:15 | Contributed Talk: Mixing Finite Success and Finite Failure in an Automatic Prover | Alwen Tiu Dale Miller Gopalan Nadathur |
| 12:00 | Contributed Talk: Snapshots Generation via Constructive Logic | Mario Ornaghi Camillo Fiorentini Alberto Momigliano |
| 12:45 14:00 | Lunch | |
| 14:00 | Invited Talk: Tabled Higher-Order Logic Programming. | Brigitte Pientka |
| 15:00 | Invited Talk: TBA | Gopalan Nadathur |
| 15:45 | Invited Talk: TBA | Dale Miller |
| Sergei Odintsov and David Pearce. Routley Semantics for Answer Sets |
| Paolo Ferraris. Answer Sets for Propositional Theories |
| Francesco Buccafurri and Gianluca Caminiti. A Social Semantics for Multi-Agent Systems |
| Martin Gebser and Torsten Schaub. Loops: Relevant or Redundant? |
| Federico Banti, José Alferes, Antonio Brogi and Pascal Hitzler. A well supported semantics for multidimensional dynamic logic programs |
| Marek Sergot and Robert Craven. Some logical properties of nonmonotonic causal theories |
| Wolfgang Faber. Unfounded Sets for Disjunctive Logic Programs with Arbitrary Aggregates |
| Victor W. Marek, Inna Pivkina and Miroslaw Truszczynski. Approximating answer sets of unitary Lifschitz-Woo programs |
| Joost Vennekens and Marc Denecker. An Algebraic Account of Modularity in ID-logic |
| Paolo Ferraris. On Modular Translations and Strong Equivalence |
| Alberto Finzi and Thomas Lukasiewicz. Game-Theoretic Reasoning about Actions in Nonmonotonic Causal Theories |
| Jean Gressmann, Tomi Janhunen, Robert Mercer, Torsten Schaub, Richard Tichy and Sven Thiele. Platypus: A platform for distributed answer set solving |
| Tran Cao Son, Phan Huy Tu, Michael Gelfond and A. Ricardo Morales. An Approximation of Action Theories of AL and its Application to Conformant Planning |
| Antonis Kakas, Loizos Michael and Rob Miller. Modular-E: an Elaboration Tolerant Approach to the Ramification and Qualification Problems |
| Wolfgang Faber and Francesco Ricca. Solving Hard ASP Programs Efficiently |
| Alex Dekhtyar and Michael I. Dekhtyar. Revisiting the Semantics of Interval Probabilistic Logic Programs |
| Jia-Huai You, Guohua Liu, Li Yuan Yuan and Curtis Onuczko. Lookahead in Smodels Compared to Local Consistencies in CSP |
| Francesco Calimeri and Giovambattista Ianni. External sources of computation for Answer Set Solvers |
| Alvaro Cortes-Calabuig, Marc Denecker, Ofer Arieli, Bert Van Nuffelen and Maurice Bruynooghe. On the Local Closed-World Assumption of Data-Sources |
| Iseline Engan, Tore Langholm, Espen Lian and Arild Waaler. Default Reasoning with Preference within Only Knowing Logic |
| Bert Van Nuffelen, Ofer Arieli, Alvaro Cortes-Calabuig and Maurice Bruynooghe. An ID-Logic Formalization of the Composition of Autonomous Databases |
| Hai-Feng Guo. Mode-Directed Fixed Point Computation |
| Stijn Heymans, Davy Van Nieuwenborgh and Dirk Vermeir. Guarded Open Answer Set Programming |
| Carlos Iván Chesñevar, Guillermo Ricardo Simari and Lluis Godo. Computing Dialectical Trees Efficiently in Possibilistic Defeasible Logic Programming |
| Kewen Wang and Yan Zhang. Nested Epistemic Logic Programs |
9-10:30 Session 1: Keynote Address Session Chair: Simon Thompson (University of Kent)
Invited Talk: How to Design Class Hierarchies Matthias Felleisen, Northeastern University
11:00-12:30 Session 2: Submitted papers Session Chair: Michael Hanus (University of Kiel)
From Functional to Object-oriented Programming -- A Smooth Transition for Beginners, Rudolf Berghammer, Frank Huch
Laziness Without All the Hard Work: Combining Lazy and Strict Languages for Teaching, Eli Barzilay, John Clements
Word Puzzles in Haskell, Sharon A. Curtis
2:30-4:00 Session 3: Submitted papers Session Chair: Robby Findler (University of Chicago)
Teaching of Image Synthesis in Functional Style, Jerzy Karczmarczuk
MinCaml: A Simple and Efficient Compiler for a Minimal Functional Language, Eijiro Sumii
Engineering Software Correctness, Rex Page
4:30-6:00 Session 4: Discussions and 'Tips and Tricks' Session Chairs: The organisers
'Tips and Tricks' session: contributions from attendees.
Round table discussion on links between FDPE and CUFP.
List of Accepted Papers:
| Thursday, September 29 | |
| Session 1 (Chair: Michael Hanus) | |
| 9.15-9.30 | Opening |
| 9.30-10.30 | Claudio Ochoa, Josep Silva and Germán Vidal Lightweight Program Specialization via Dynamic Slicing |
| Rafael Caballero A Declarative Debugger of Incorrect Answers for Constraint Functional-Logic Programs |
|
| 10.30-11.00 | Coffee |
| Session 2 (Chair: Germán Vidal) | |
| 11.00-12.30 | Julio Mariño and Jose Maria Rey Adding Constraints to Curry via Flat Guards |
| Sonia Estevez Martin and Rafael del Vado Virseda Designing an Efficient Computation Strategy in CFLP(FD) Using Definitional Trees |
|
| Jesus M. Almendros-Jimenez Constraint Logic Programming over Sets of Spatial Objects |
|
| 12.30-14.30 | Lunch |
| Session 3 (Chair: Julio Mariño) | |
| 14.30-16.00 | Michael Hanus A Generic Analysis Environment for Declarative Programs |
| J. Guadalupe Ramos, Josep Silva and Germán Vidal An Offline Partial Evaluator for Curry Programs |
|
| Sebastian Fischer A Functional Logic Database Library |
|
| 16.00-16.30 | Coffee |
| Session 4 (Chair: Francisco J. López-Fraguas) | |
| 16.30-18.00 | Bernd Braßel and Frank Huch Translating Curry To Haskell |
| Emilio Gallego and Julio Mariño An Overview of the Sloth2005 Curry System |
|
| Individual system demonstrations, closing | |
K. Subramani, D. Desovski
A New Verification Procedure for Partially Clairvoyant Scheduling
Flavio Corradini, Walter Vogler
Performance of Pipelined Asynchronous Systems
Martijn Hendriks
Model Checking the Time to Reach Agreement
Wan Fokkink, Jun Pang, Anton Wijs
Is Timed Branching Bisimilarity an Equivalence Indeed?
Thomas Chatain, Claude Jard
Time Supervision of Concurrent Systems using Symbolic Unfoldings of
Time Petri Nets
Laurent Doyen, Thomas Henzinger, Jean-François Raskin
Automatic Rectangular Refinement of Affine Hybrid Systems
Hongping Lim, Dilsun Kaynar, Nancy Lynch, Sayan Mitra
Translating Timed I/O Automata Specifications for Theorem Proving in
PVS
Patricia Bouyer, François Laroussinie, Pierre-Alain Reynier
Diagonal Constraints in Timed Automata - Forward Analysis of Timed
Systems
Thomas Brihaye, Véronique Bruyère,
Jean-François Raskin
On Optimal Timed Strategies
Husain Aljazzar, Holger Hermanns, Stefan Leue
Counterexamples for Timed Probabilistic Reachability
Oded Maler, Dejan Nickovic, Amir Pnueli
Real-time Temporal Logic: Past, Present, Future
Karine Altisen, Stavros Tripakis
Implementation of Timed Automata: An Issue of Semantics or Modeling?
Gerd Behrmann, Kim Larsen, Jacob Rasmussen
Beyond Liveness - Efficient Parameter Synthesis for Time Bounded
Liveness
Raffaella Gentilini
Reachability Problems on Extended o-minimal Hybrid Automata
Roberto Giacobazzi, Isabella Mastroeni
Timed Abstract Non-Interference
Beatrice Berard, Franck Cassez, Serge Haddad, Didier Lime, Olivier
H. Roux
Comparison of the Expressiveness of Timed Automata and Time Petri
Nets
Thomas Henzinger, Rupak Majumdar, Vinayak Prabhu
Quantifying Similarities Between Timed Systems
Atle Refsdal, Knut Husa, Ketil Stølen
Specification and Refinement of Soft Real-time Requirements Using
Sequence Diagrams
Bo Adler, Luca de Alfaro, Marco Faella
Average Reward Timed Games
HIGHLIGHTS
. Co-location with FORTE 2005
. Three Keynote Speeches:
. Amir Pnueli (joint with FORTE 2005)
. Zohar Manna
. Wolfgang Thomas
. Three Two-Hour Tutorials, given also by the keynote speakers
. 33 Contributed Papers
. Proceedings as LNCS 3707 of Springer
. Early Registration: Friday September 1
Please visit the conference Web site for details.
PRELIMINARY PROGRAM
-----
Tutorial Day
Tuesday, October 4, 2005
(Barry Lam Hall, read "Bo Li Guan" in Chinese, Conference Room 201)
0830-1000: Registration and Refreshment
1000-1200: Tutorial I
Title: TBA
Speaker: Amir Pnueli
1200-1330: Lunch
1330-1530: Tutorial II
Title: Decision Procedure: Classical Techniques
Speaker: Zohar Manna
1530-1600: Coffee Break
1600-1800: Tutorial III
Title: TBA
Speaker: Wolfgang Thomas
1830-1900: Bus ride to the Reception
1900-2130: Opening and Reception (joint with FORTE 2005 Banquet)
-----
Day One of Main Symposium
Wednesday, October 5, 2005
(Barry Lam Hall, Auditorium 101)
0830-0930: Keynote Speech I (joint with FORTE 2005)
Title: Ranking Abstraction as a Companion to Predicate Abstraction
Speaker: Amir Pnueli
0930-1000: Coffee Break
1000-1200: Model Checking
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond
Authors: Limor Fix, Orna Grumberg, Amnon Heyman, Tamir Heyman, and Assaf Schuster
A New Reachability Algorithm for Symmetric Multi-processor Architecture
Authors: Debashis Sahoo, Jawahar Jain, Subramanian Iyer, and David Dill
Comprehensive Verification Framework for Dependability of Self-optimizing Systems
Authors: Y. Zhao and M. Kardos and S. Oberthuer and F.J. Rammig
Exploiting Hub States in Automatic Verification
Authors: Giuseppe Della Penna, Igor Melatti, Benedetto Intrigila, and Enrico Tronci
1200-1230: Coffee Break (quick lunch now or after the next short session)
1230-1330: Combined Methods
An Approach for the Verification of SystemC Designs using AsmL
Authors: Ali Habibi and Sofiene Tahar
Decomposition-Based Verification of Cyclic Workflows
Authors: Yongsun Choi and J. Leon Zhao
1400-1800: Excursion (joint with FORTE 2005)
1830-2030: Committees Meeting
-----
Day Two of Main Symposium
Thursday, October 6, 2005
(Barry Lam Hall, Auditorium 101)
0830-0930: Keynote Speech II
Title: Termination and Invariance Analysis of Loops
Speaker: Zohar Manna
0930-1000: Coffee Break
1000-1200: Timed, Embedded, and Hybrid Systems (I)
Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust
Discrete Time Hybrid Systems
Authors: Werner Damm, Guilherme Pinto, and Stefan Ratschan
Computation Platform for Automatic Analysis of Embedded Software Systems Using
Model Based Approach
Authors: A. Dubey, X. Wu, H. Su, and T.J. Koo
Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities
Authors: Andrei Voinikonis
Automatic Test Case Generation with Region-Related Coverage Annotations for
Real-time Systems
Authors: Geng-Dian Huang and Farn Wang
1200-1330: Lunch
1330-1530: Abstraction and Reduction Techniques
Selective Search in Bounded Model Checking of Reachability Properties
Authors: Maciej Szreter
Predicate Abstraction of RTL Verilog Descriptions using Constraint Logic Programming
Authors: Tun Li, Yang Guo, SiKun Li, and GongJie Liu
State Space Exploration of Object-Based Systems using Equivalence Reduction and the
Sweepline Method
Authors: Charles A. Lakos and Lars M. Kristensen
Title: Syntactical Colored Petri Nets Reductions
Authors: S. Evangelista, S.Haddad, J.-F. Pradat-Peyre
1530-1600: Coffee Break
1600-1800: Decidability and Complexity (Parallel Session)
Algorithmic Algebraic Model Checking II: Decidability of Semi-Algebraic Model Checking
and its Applications to Systems Biology
Authors: V. Mysore, C. Piazza, and B. Mishra
A Static Analysis using Tree Automata for XML Access Control
Authors: Isao Yagi, Yoshiaki Takata, and Hiroyuki Seki
Reasoning about Transfinite Sequences
Authors: Stephane Demri and David Nowak
Semi-Automatic Distributed Synthesis
Authors: Bernd Finkbeiner and Sven Schewe
1600-1800: Established Formalisms and Standards (Parallel Session)
A New Graph of Classes for the Preservation of Quantitative Temporal Constraints
Authors: Xiaoyu Mao, Janette Cardoso, and Robert Valette
Comparison of Different Semantics for Time Petri Nets
Authors: B. Berard, F. Cassez, S. Haddad, Didier Lime, and O.H. Roux
Introducing Dynamic Properties with Past Temporal Operators in the B Refinement
Authors: Mouna Saad and Leila Jemni Ben Ayed
Approximate Reachability for Dead Code Elimination in Esterel*
Authors: Olivier Tardieu and Stephen A. Edwards
1830-1900: Bus ride to the Banquet
1900-2130: Banquet
-----
Day Three of Main Symposium
Friday, October 7, 2005
(Barry Lam Hall, Auditorium 101)
0830-0930: Keynote Speech III
Title: Some Perspectives of Infinite-State Verification
Authors: Wolfgang Thomas
0930-1000: Coffee Break
1000-1100: Compositional Verification and Games
Synthesis of Interface Automata
Authors: Purandar Bhaduri
Multi-Valued Model Checking Games
Authors: Sharon Shoham and Orna Grumberg
1100-1200: Timed, Embedded, and Hybrid Systems (II)
Model Checking Prioritized Timed Automata
Authors: Shang-Wei Lin, Pao-Ann Hsiung, Chun-Hsian Huang, and Yean-Ru Chen
An MTBDD-based Implementation of Forward Reachability for Probabilistic Timed Automata
Authors: Fuzhi Wang and Marta Kwiatkowska
1200-1330: Lunch
1330-1530: Protocols Analysis, Case Studies, and Tools
An EFSM-based Intrusion Detection System for Ad Hoc Networks
Authors: Jean-Marie Orset, Baptiste Alcalde, and Ana Cavalli
Modeling and Verification of a Telecommunication Application using Live Sequence Charts
and the Play-Engine Tool
Authors: Pierre Combes, David Harel, and Hillel Kugler
Formal Construction and Verification of Home Service Robots: A Case Study
Authors: Moonzoo Kim and Kyo Chul Kang
Model Checking Real Time Java Using Java PathFinder
Authors: Gary Lindstrom, Peter C. Mehlitz, and Willem Visser
1530-1600: Coffee Break
1600-1730: Infinite-State and Parameterized Systems
Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols
Authors: Guy Edward Gallasch and Jonathan Billington
Flat Acceleration in Symbolic Model Checking
Authors: Sebastien Bardin, Alain Finkel, Jerome Leroux, and Philippe Schnoebelen
Flat Counter Automata Almost Everywhere!
Authors: Jerome Leroux and Gregoire Sutre
1730-1800: Closing