Proceedings of the 12th International Symposium of Formal Methods Europe
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

FM
DBLP
Scholar
Full names Links ISxN
@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)

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.