FME 2003: Pisa, Italy
Keijiro Araki, Stefania Gnesi, Dino Mandrioli (Eds.): FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings. Springer 2003 Lecture Notes in Computer Science 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
- 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
- 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
- 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 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
- Jei-Wen Teng, Yih-Kuen Tsay: Composing Temporal-Logic Specifications with Machine Assistance. 719-738
Program Checking and Testing
- 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
- Amel Mammar, Régine Laleau: Design of an Automatic Prover Dedicated to the Refinement of Database Applications. 834-854
Security
- Alessandro Armando, Luca Compagna, Pierre Ganty: SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis. 875-893
- Giovanni Vigna: A Topological Characterization of TCP/IP Security. 914-939
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T201401 by the dblp team