Keijiro Araki, Stefania Gnesi, Dino Mandrioli
Proceedings of the 12th International Symposium of Formal Methods Europe
FME, 2003.

@proceedings{FME-2003,
	address       = "Pisa, Italy",
	editor        = "Keijiro Araki and Stefania Gnesi and Dino Mandrioli",
	isbn          = "3-540-40828-2",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 12th International Symposium of Formal Methods Europe}",
	volume        = 2805,
	year          = 2003,
}

Contents (49 items)

8 ×#model checking
6 ×#verification
5 ×#composition
4 ×#proving
4 ×#specification
3 ×#analysis
3 ×#approach
3 ×#correctness
3 ×#protocol
3 ×#semantics

FME-2003-Kishida #development #paradigm #roadmap

Looking Back to the Future: Thoughts on Paradigm Shift in Software Development (KK), pp. 1–6.

FME-2003-SawadaKF #future of #implementation #past present future

Past, Present, and Future of SRA Implementation of CafeOBJ: Annex (TS, KK, KF), pp. 7–17.

FME-2003-Randell #fault #on the

On Failures and Faults (BR), pp. 18–39.

FME-2003-Holzmann #roadmap #verification

Trends in Software Verification (GJH), pp. 40–50.

FME-2003-Abrial #development #pointer

Event Based Sequential Program Development: Application to Constructing a Pointer Program (JRA), pp. 51–74.

FME-2003-MillerTH #proving

Proving the Shalls (SPM, ACT, MPEH), pp. 75–93.

FME-2003-BertBPRV #adaptation #c #embedded #source code #specification

Adaptable Translator of B Specifications to Embedded C Programs (DB, SB, MLP, AR, LV), pp. 94–113.

FME-2003-CompareIPS #analysis #architecture #lifecycle #model checking #validation

Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle (DC, PI, PP, AS), pp. 114–132.

FME-2003-WassyngL #formal method #implementation #industrial #lessons learnt

Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project (AW, ML), pp. 133–153.

FME-2003-HayesJJ #specification

Determining the Specification of a Control System from That of Its Environment (IJH, MAJ, CBJ), pp. 154–169.

FME-2003-StidolphW #formal method #using

Managerial Issues for the Consideration and Use of Formal Methods (DCS, EJWJ), pp. 170–186.

FME-2003-Fidge #legacy #verification

Verifying Emulation of Legacy Mission Computer Systems (CJF), pp. 187–207.

FME-2003-BozzanoCCVV #assessment #case study #industrial #safety

Improving Safety Assessment of Complex Systems: An Industrial Case Study (MB, AC, MC, LV, AV), pp. 208–222.

FME-2003-Rusu #composition #protocol #verification

Compositional Verification of an ATM Protocol (VR), pp. 223–243.

FME-2003-Henderson #correctness #proving #using

Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method (NH), pp. 244–263.

FME-2003-BoyerS #constraints #protocol #synthesis #verification

Synthesis and Verification of Constraints in the PGM Protocol (MB, MS), pp. 264–281.

FME-2003-QinC #hardware

Mapping Statecharts to Verilog for Hardware/Software Co-specification (SQ, WNC), pp. 282–300.

FME-2003-DuranCS #compilation #inheritance

A Strategy for Compiling Classes, Inheritance, and Dynamic Binding (AD, AC, AS), pp. 301–320.

FME-2003-QinDC #programming #semantics

A Semantic Foundation for TCOZ in Unifying Theories of Programming (SQ, JSD, WNC), pp. 321–340.

FME-2003-KouchnarenkoL #component #refinement #verification

Refinement and Verification of Synchronized Component-Based Systems (OK, AL), pp. 341–358.

FME-2003-RosuELM #equation #proving

Certifying and Synthesizing Membership Equational Proofs (GR, SE, PL, JM), pp. 359–380.

FME-2003-BeekK #automaton #composition

Team Automata Satisfying Compositionality (MHtB, JK), pp. 381–400.

FME-2003-Charpentier #invariant

Composing Invariants (MC), pp. 401–421.

FME-2003-BurdyRL #approach #correctness #developer #java

Java Applet Correctness: A Developer-Oriented Approach (LB, AR, JLL), pp. 422–439.

FME-2003-Chalin #effectiveness #ml

Improving JML: For a Safer and More Effective Language (PC), pp. 440–461.

FME-2003-Lettrari #abstraction #heuristic #object-oriented #using

Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems (ML), pp. 462–481.

FME-2003-MarinescuR #composition #design #framework

A Formal Framework for Modular Synchronous System Design (MCVM, MCR), pp. 482–502.

FME-2003-GurfinkelC #generative #model checking #multi

Generating Counterexamples for Multi-valued Model-Checking (AG, MC), pp. 503–521.

FME-2003-Schafer #analysis #fault #model checking #realtime

Combining Real-Time Model-Checking and Fault Tree Analysis (AS), pp. 522–541.

FME-2003-MorzentiPPS #model checking #specification

Model-Checking TRIO Specifications in SPIN (AM, MP, PSP, PS), pp. 542–561.

FME-2003-MussetR #linear

Computing Meta-transitions for Linear Transition Systems with Polynomials (JM, MR), pp. 562–581.

FME-2003-XieBK #composition #reasoning

Translation-Based Compositional Reasoning for Software Systems (FX, JCB, RPK), pp. 582–599.

FME-2003-GoldsmithMRWZ #model checking

Watchdog Transformations for Property-Oriented Model-Checking (MG, NM, BR, TW, IZ), pp. 600–616.

FME-2003-AtiyaKW #semantics

A Circus Semantics for Ravenscar Protected Objects (DAA, SK, JW), pp. 617–635.

FME-2003-FenkamGJ #approach #concurrent

Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach (PF, HCG, MJ), pp. 636–657.

FME-2003-AldiniB #approach #architecture #concurrent #verification

A General Approach to Deadlock Freedom Verification for Software Architectures (AA, MB), pp. 658–677.

FME-2003-FriasPBAM #alloy

Taking Alloy to the Movies (MFF, CLP, GB, NA, TSEM), pp. 678–697.

FME-2003-KuhnO #state machine

Interacting State Machines for Mobility (TAK, DvO), pp. 698–718.

FME-2003-TengT #specification

Composing Temporal-Logic Specifications with Machine Assistance (JWT, YKT), pp. 719–738.

FME-2003-ThumsS #model checking

Model Checking FTA (AT, GS), pp. 739–757.

FME-2003-Glesner

Program Checking with Certificates: Separating Correctness-Critical Code (SG), pp. 758–777.

FME-2003-BouquetL #case study #execution #generative #java #testing #transaction

Reification of Executable Test Scripts in Formal Specicifation-Based Test Generation: The Java Card Transaction Mechanism Case Study (FB, BL), pp. 778–795.

FME-2003-DongSW #alloy #reasoning #semantics #web

Checking and Reasoning about Semantic Web through Alloy (JSD, JS, HHW), pp. 796–813.

FME-2003-PoppletonB #composition

Structuring Retrenchments in B by Decomposition (MP, RB), pp. 814–833.

FME-2003-MammarL #automation #database #design #proving #refinement

Design of an Automatic Prover Dedicated to the Refinement of Database Applications (AM, RL), pp. 834–854.

FME-2003-LeuschelB #model checking #named

ProB: A Model Checker for B (ML, MJB), pp. 855–874.

FME-2003-ArmandoCG #analysis #graph #model checking #protocol #satisfiability #security #using

SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis (AA, LC, PG), pp. 875–893.

FME-2003-DenneyF #correctness #policy #safety

Correctness of Source-Level Safety Policies (ED, BF), pp. 894–913.

FME-2003-Vigna #security

A Topological Characterization of TCP/IP Security (GV), pp. 914–939.