ISoLA 2004: Paphos, Cyprus - Preliminary proceedings

Thematic session: Program Analysis and Transformation

• Daniel J. Quinlan, Markus Schordan, Qing Yi, Andreas Sæbjørnsen: Classification and Utilization of Abstractions for Optimization. 2-9
• Wolf Zimmermann: On the Correctness of Transformations in Compiler Back-Ends. 10-17
• Byron Cook: Finding API usage rule violations in Windows device drivers using Static Driver Verifier. 18-18

Thematic session: From Processes via Workflows to Services

• Jörg Becker: Project Management for Process Management - a Procedural Model for Process-Oriented Reorganisation Projects. 19-27
• Jens Hündling, Mathias Weske: Modeling Quality of Services in Service Oriented Environments. 28-34
• Kirsten Lenz, Andreas Oberweis: Workflow Services: A Petri Net-Based Approach to Web Services. 35-41
• Rey Abe, Martin Beinhart, Stefan Biffl, eva Kühn, Markus Ly, Bettina Thurnher: Need for Rigorous Methods and Tools in Collaborative Mobile Software Solutions - a Use Case Study on a "Travel Service Application". 42-44

Thematic session: Structured Data Tools

• Pieter J. Toussaint, Leo Wolf: The Narrator System: processing, storing and retrieving medical, narrative data. 45-50
• Joost Jacob: A Rule Markup Language and its application to UML. 51-57
• Dave Clarke, David Costa, Farhad Arbab: Modelling Coordination in Biological Systems. 58-66
• Joost Jacob, Frank S. de Boer, Marcello M. Bonsangue, Andries Stam, Leendert van der Torre: Using XML Transformations for Enterprise Architectures. 67-73

Regular papers: Model Checking and Validation

• Yamine Aït Ameur, Mickaël Baron: Bridging the gap between formal and experimental validation approaches in HCI systems design: use of the event B proof based technique. 74-80
• María Alpuente, Demis Ballis, Moreno Falaschi: Automated Verification of Web Sites Using Partial Rewriting. 81-88
• Shady Copty, Shai Fine, Shmuel Ur, Avi Ziv: Probabilistic Alternative Regression Suites. 89-91
• Tudor Jebelean, Laura Kovács, Nikolaj Popov: Experimental Program Verification in the Theorema System. 92-99

Regular papers: Formal Methods in Industry

• Christopher A. Rouff, Amy Vanderbilt, Walter Truszkowski, James L. Rash, Michael G. Hinchey: Formal Methods for Autonomic and Swarm-based Systems. 100-102
• Jesper Andersen, Ebbe Elsborg, Fritz Henglein, Jakob Grue Simonsen, Christian Stefansen: Compositional Specification of Commercial Contracts. 103-110

Thematic session: Error Analysis and Model-based Testing Tools

• Parosh Aziz Abdulla, Johan Deneaux, Gunnar Stålmarck, Herman Ågren, Ove Åkerlund: Designing Safe, Reliable Systems using Scade. 111-118
• Johan Andersson, Christer Norström, Anders Wall: Decreasing Maintenance Costs by Introducing Formal Models and Analysis of Real-Time Systems in Industrial Settings. 119-125
• Andreas Ermedahl, Jan Gustafsson, Björn Lisper, Daniel Sandell: Static Timing Analysis of Real-Time Operating Systems Code. 126-133

Panel: Formal Approaches to Complex Software Systems

Regular papers: Software Technology

• Doral Lucanu: A Logical Foundation of the OWL Languages. 135-142
• Gabriel Alves, Adilson Arcoverde, Ricardo Massa Ferreira Lima, Paulo Romero Martins Maciel: EZPetri: A Petri net interchange framework for Eclipse based on PNML. 143-149
• eva Kühn, Fabian Schmied: Distributed Peer-to-Peer Application development with Declarative and Aspect-Oriented techniques. 150-156

Regular papers: Model Checking and Validation

• Pranav Ashar, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Zijiang Yang: Efficient SAT-based Bounded Model Checking for Software Verification. 157-164
• Radu Grosu, Scott A. Smolka: Quantitative Model checking. 165-174
• Shoham Ben-David, Dana Fisman, Sitvanit Ruah: Embedding Finite Automata within regular Expressions. 175-180
• Martin Freibothe, Jens Schönherr, Bernd Straube, Jörg Bormann: Semi-formal Verification of the quasi-static behavior of Mixed-Signal Circuits by SAT-based Property Checking. 181-187

Thematic session: Industrial use of tools for formal analysis

• Mirko Conrad: Formal Techniques for Analysing and Testing Automotive Control Software developed in a Model-based Way. 188-188
• Limor Fix: Abstract for the ISOLA Special Session on "Industrial use of tools for Formal Analysis". 189-189
• Yaron Wolfsthal: Abstract for the ISOLA Special Session on "Industrial use of tools for Formal Analysis". 190-190
• Jianli Xu: Application of formal methods in Nokia mobile terminal and network software system development. 190-190

Thematic session: Dependable component-based and networked applications

• Henrik Eichenhardt, Elke Franz, Simone Röttger, Ute Wappler: Adapting Component Models to Support Responsibility. 191-193
• Ramesh Rharadwaj: Development of Dependable Component-Based Distributed Applications. 194-200

Thematic session: Scheduling and Performance of Real-time Embedded Systems

• Martijn Hendriks, Barend van den Nieuwelaar, Frits W. Vaandrager: Model Checker Aided Design of a Controller for a Wafer Scanner. 201-208
• Marcel Verhoef, Ernesto Wandeler, Lothar Thiele, Paul Lieverse: System Architecture Evaluation Using Modular Performance Analysis - A Case Study. 209-219
• Oana Florescu, Jeroen Voeten, Henk Corporaal: A Unified Model for Analysis of Real-Time Properties. 220-226

Thematic session: Parametrised model-checking

• Muffy Calder, Alice Miller: Verifying parametrized, featured networks by abstraction. 227-234
• Michael Huth, Altaf Hussain: On model checking multiple hybrid views. 235-242
• Saddek Bensalem, Doron Peled, Hongyang Qu, Stavros Tripakis: Automatic Generation of Path Conditions for Timed Systems. 243-249

Thematic session: Analysis and Verification of Component-Based Systems

• Harini Srinivasan, Darrell Reimer, Aaron Kershenbaum, Edith Schonberg, Kavitha Srinivas: Static validation of resource management in large Java applications. 250-252
• Jakob Rehof, Sriram K. Rajamani: Models for Contract Conformance. 253-260
• Matthew Hoosier, John Hatcliff, Robby, Matthew B. Dwyer: A Case Study in Domain-customized Model Checking for Real-time Component Software. 261-267

Thematic session: Formal Methods for Quantitative Analysis of Systems

• Marie Duflot, Marta Z. Kwiatkowska, Gethin Norman, David Parker: A Formal Analysis of Bluetooth Device Discovery. 268-275
• Simona Bernardi, Susanna Donatelli, Giovanna Dondossola: A class Diagram framework for collecting dependability requirements in automation systems. 276-283
• Henrik C. Bohnenkamp, Holger Hermanns, David N. Jansen, Joost-Pieter Katoen, Yaroslav S. Usenko: An industrial-strength formal method -- A Modest survey. 284-295

Regular papers: Case Studies

• Erwan Jahier, Pascal Raymond, Philippe Baufreton: Case Studies with Lurette V2. 296-303
• Søren Christensen, Jens Bæk Jørgensen, Antti-Pekka Tuovinen, Jianli Xu: Estimation of Memory Usage of Mobile Phone Software Using UML and Coloured Petri Nets. 304-310

Thematic session: Model Based Testing og Large-scale and Real-Time Systems

• Victor V. Kuliamin: Model Based Testing of Large-scale Software: How Can Simple Models Help to Test Complex System. 311-316
• Daniel Mika, Josef Strnadel, Zdenik Kotásek: The Identification of registers in RTL Structures for the Test Application. 317-319

Thematic session: Formal Methods for Quantitative Analysis of Systems

• Joern Ploennigs, Mario Neugebauer, Klaus Kabitzsch: Automated Model Generation from Design Databases at the Example of Building Automation Networks. 320-327
• Peter Buchholz, Falko Bause, Carsten Tepper: The ProC/B-Approach from informal descriptions to formal models. 328-334

Thematic session: Adaption of Formal Methods for Industry

• Francois Carcenac, Frédéric Boniol: Verification of an avionic system using timed model checking. 335-342
• Dmitrij Koznov, Maxim Katrashov, Goman Gagarsky, Vera A. Zvereva, Alexey Barsov: Round-trip engineering of reactive systems. 343-347

Last update Tue May 21 17:31:40 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page