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.