


default search action
FME 2003: Pisa, Italy
- Keijiro Araki, Stefania Gnesi, Dino Mandrioli:

FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings. Lecture Notes in Computer Science 2805, Springer 2003, ISBN 3-540-40828-2
Invited Speakers
- Kouichi Kishida:

Looking Back to the Future: Thoughts on Paradigm Shift in Software Development. 1-6 - Toshimi Sawada, Kouichi Kishida, Kokichi Futatsugi:

Past, Present, and Future of SRA Implementation of CafeOBJ: Annex. 7-17 - Brian Randell:

On Failures and Faults. 18-39 - Gerard J. Holzmann:

Trends in Software Verification. 40-50 - Jean-Raymond Abrial:

Event Based Sequential Program Development: Application to Constructing a Pointer Program. 51-74
I-Day
- Steven P. Miller, Alan C. Tribble, Mats Per Erik Heimdahl:

Proving the Shalls. 75-93 - Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin:

Adaptable Translator of B Specifications to Embedded C Programs. 94-113 - Daniele Compare, Paola Inverardi, Patrizio Pelliccione

, Alessandra Sebastiani:
Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle. 114-132 - Alan Wassyng, Mark Lawford:

Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project. 133-153
Control Systems and Industrial Applications
- Ian J. Hayes

, Michael A. Jackson, Cliff B. Jones
:
Determining the Specification of a Control System from That of Its Environment. 154-169 - Donna C. Stidolph, E. James Whitehead Jr.:

Managerial Issues for the Consideration and Use of Formal Methods. 170-186 - Colin J. Fidge

:
Verifying Emulation of Legacy Mission Computer Systems. 187-207 - Marco Bozzano, Antonella Cavallo, Massimo Cifaldi, Laura Valacca, Adolfo Villafiorita:

Improving Safety Assessment of Complex Systems: An Industrial Case Study. 208-222
Communications System Verification
- Vlad Rusu:

Compositional Verification of an ATM Protocol. 223-243 - Neil Henderson:

Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method. 244-263 - Marc Boyer

, Mihaela Sighireanu:
Synthesis and Verification of Constraints in the PGM Protocol. 264-281
Co-specification and Compilers
- Shengchao Qin

, Wei-Ngan Chin:
Mapping Statecharts to Verilog for Hardware/Software Co-specification. 282-300 - Adolfo Duran, Ana Cavalcanti, Augusto Sampaio:

A Strategy for Compiling Classes, Inheritance, and Dynamic Binding. 301-320
Composition
- Shengchao Qin

, Jin Song Dong, Wei-Ngan Chin:
A Semantic Foundation for TCOZ in Unifying Theories of Programming. 321-340 - Olga Kouchnarenko

, Arnaud Lanoix:
Refinement and Verification of Synchronized Component-Based Systems. 341-358 - Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer:

Certifying and Synthesizing Membership Equational Proofs. 359-380 - Maurice H. ter Beek, Jetty Kleijn:

Team Automata Satisfying Compositionality. 381-400 - Michel Charpentier:

Composing Invariants. 401-421
Java, Object Orientation and Modularity
- Lilian Burdy, Antoine Requet, Jean-Louis Lanet:

Java Applet Correctness: A Developer-Oriented Approach. 422-439 - Patrice Chalin:

Improving JML: For a Safer and More Effective Language. 440-461 - Marc Lettrari:

Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems. 462-481 - Maria-Cristina V. Marinescu, Martin C. Rinard:

A Formal Framework for Modular Synchronous System Design. 482-502
Model Checking
- Arie Gurfinkel

, Marsha Chechik:
Generating Counterexamples for Multi-valued Model-Checking. 503-521 - Andreas Schäfer:

Combining Real-Time Model-Checking and Fault Tree Analysis. 522-541 - Angelo Morzenti

, Matteo Pradella
, Pierluigi San Pietro, Paola Spoletini:
Model-Checking TRIO Specifications in SPIN. 542-561 - Julien Musset, Michaël Rusinowitch:

Computing Meta-transitions for Linear Transition Systems with Polynomials. 562-581 - Fei Xie, James C. Browne, Robert P. Kurshan:

Translation-Based Compositional Reasoning for Software Systems. 582-599 - Michael Goldsmith, Nick Moffat, Bill Roscoe, Tim Whitworth, Irfan Zakiuddin:

Watchdog Transformations for Property-Oriented Model-Checking. 600-616
Parallel Process
- Diyaa-Addein Atiya, Steve King, Jim Woodcock

:
A Circus Semantics for Ravenscar Protected Objects. 617-635 - Pascal Fenkam, Harald C. Gall, Mehdi Jazayeri:

Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach. 636-657 - Alessandro Aldini

, Marco Bernardo:
A General Approach to Deadlock Freedom Verification for Software Architectures. 658-677 - Marcelo F. Frias

, Carlos López Pombo, Gabriel Baum, Nazareno Aguirre, T. S. E. Maibaum:
Taking Alloy to the Movies. 678-697 - Thomas A. Kuhn, David von Oheimb:

Interacting State Machines for Mobility. 698-718 - Jei-Wen Teng, Yih-Kuen Tsay:

Composing Temporal-Logic Specifications with Machine Assistance. 719-738
Program Checking and Testing
- Andreas Thums, Gerhard Schellhorn:

Model Checking FTA. 739-757 - Sabine Glesner:

Program Checking with Certificates: Separating Correctness-Critical Code. 758-777 - Fabrice Bouquet, Bruno Legeard:

Reification of Executable Test Scripts in Formal Specicifation-Based Test Generation: The Java Card Transaction Mechanism Case Study. 778-795 - Jin Song Dong, Jing Sun, Hai H. Wang:

Checking and Reasoning about Semantic Web through Alloy. 796-813
B Method
- Michael Poppleton, Richard Banach:

Structuring Retrenchments in B by Decomposition. 814-833 - Amel Mammar, Régine Laleau:

Design of an Automatic Prover Dedicated to the Refinement of Database Applications. 834-854 - Michael Leuschel, Michael J. Butler:

ProB: A Model Checker for B. 855-874
Security
- Alessandro Armando, Luca Compagna, Pierre Ganty:

SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis. 875-893 - Ewen Denney, Bernd Fischer:

Correctness of Source-Level Safety Policies. 894-913 - Giovanni Vigna:

A Topological Characterization of TCP/IP Security. 914-939

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














