Abstract is missing.
- Looking Back to the Future: Thoughts on Paradigm Shift in Software DevelopmentKouichi Kishida. 1-6 [doi]
- Past, Present, and Future of SRA Implementation of CafeOBJ: AnnexToshimi Sawada, Kouichi Kishida, Kokichi Futatsugi. 7-17 [doi]
- On Failures and FaultsBrian Randell. 18-39 [doi]
- Trends in Software VerificationGerard J. Holzmann. 40-50 [doi]
- Event Based Sequential Program Development: Application to Constructing a Pointer ProgramJean-Raymond Abrial. 51-74 [doi]
- Proving the ShallsSteven P. Miller, Alan C. Tribble, Mats Per Erik Heimdahl. 75-93 [doi]
- Adaptable Translator of B Specifications to Embedded C ProgramsDidier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin. 94-113 [doi]
- Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-CycleDaniele Compare, Paola Inverardi, Patrizio Pelliccione, Alessandra Sebastiani. 114-132 [doi]
- Lessons Learned from a Successful Implementation of Formal Methods in an Industrial ProjectAlan Wassyng, Mark Lawford. 133-153 [doi]
- Determining the Specification of a Control System from That of Its EnvironmentIan J. Hayes, Michael A. Jackson, Cliff B. Jones. 154-169 [doi]
- Managerial Issues for the Consideration and Use of Formal MethodsDonna C. Stidolph, Jim Whitehead. 170-186 [doi]
- Verifying Emulation of Legacy Mission Computer SystemsColin J. Fidge. 187-207 [doi]
- Improving Safety Assessment of Complex Systems: An Industrial Case StudyMarco Bozzano, Antonella Cavallo, Massimo Cifaldi, Laura Valacca, Adolfo Villafiorita. 208-222 [doi]
- Compositional Verification of an ATM ProtocolVlad Rusu. 223-243 [doi]
- Proving the Correctness of Simpson s 4-Slot ACM Using an Assertional Rely-Guarantee Proof MethodNeil Henderson. 244-263 [doi]
- Synthesis and Verification of Constraints in the PGM ProtocolMarc Boyer, Mihaela Sighireanu. 264-281 [doi]
- Mapping Statecharts to Verilog for Hardware/Software Co-specificationShengchao Qin, Wei-Ngan Chin. 282-300 [doi]
- A Strategy for Compiling Classes, Inheritance, and Dynamic BindingAdolfo Duran, Ana Cavalcanti, Augusto Sampaio. 301-320 [doi]
- A Semantic Foundation for TCOZ in Unifying Theories of ProgrammingShengchao Qin, Jin Song Dong, Wei-Ngan Chin. 321-340 [doi]
- Refinement and Verification of Synchronized Component-Based SystemsOlga Kouchnarenko, Arnaud Lanoix. 341-358 [doi]
- Certifying and Synthesizing Membership Equational ProofsGrigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer. 359-380 [doi]
- Team Automata Satisfying CompositionalityMaurice H. ter Beek, Jetty Kleijn. 381-400 [doi]
- Composing InvariantsMichel Charpentier. 401-421 [doi]
- Java Applet Correctness: A Developer-Oriented ApproachLilian Burdy, Antoine Requet, Jean-Louis Lanet. 422-439 [doi]
- Improving JML: For a Safer and More Effective LanguagePatrice Chalin. 440-461 [doi]
- Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented SystemsMarc Lettrari. 462-481 [doi]
- A Formal Framework for Modular Synchronous System DesignMaria-Cristina V. Marinescu, Martin C. Rinard. 482-502 [doi]
- Generating Counterexamples for Multi-valued Model-CheckingArie Gurfinkel, Marsha Chechik. 503-521 [doi]
- Combining Real-Time Model-Checking and Fault Tree AnalysisAndreas Schäfer. 522-541 [doi]
- Model-Checking TRIO Specifications in SPINAngelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini. 542-561 [doi]
- Computing Meta-transitions for Linear Transition Systems with PolynomialsJulien Musset, Michaël Rusinowitch. 562-581 [doi]
- Translation-Based Compositional Reasoning for Software SystemsFei Xie, James C. Browne, Robert P. Kurshan. 582-599 [doi]
- Watchdog Transformations for Property-Oriented Model-CheckingMichael Goldsmith, Nick Moffat, Bill Roscoe, Tim Whitworth, Irfan Zakiuddin. 600-616 [doi]
- A Circus Semantics for Ravenscar Protected ObjectsDiyaa-Addein Atiya, Steve King, Jim Woodcock. 617-635 [doi]
- Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee ApproachPascal Fenkam, Harald Gall, Mehdi Jazayeri. 636-657 [doi]
- A General Approach to Deadlock Freedom Verification for Software ArchitecturesAlessandro Aldini, Marco Bernardo. 658-677 [doi]
- Taking ::::Alloy:::: to the MoviesMarcelo F. Frias, Carlos López Pombo, Gabriel Baum, Nazareno Aguirre, T. S. E. Maibaum. 678-697 [doi]
- Interacting State Machines for MobilityThomas A. Kuhn, David von Oheimb. 698-718 [doi]
- Composing Temporal-Logic Specifications with Machine AssistanceJei-Wen Teng, Yih-Kuen Tsay. 719-738 [doi]
- Model Checking FTAAndreas Thums, Gerhard Schellhorn. 739-757 [doi]
- Program Checking with Certificates: Separating Correctness-Critical CodeSabine Glesner. 758-777 [doi]
- Reification of Executable Test Scripts in Formal Specicifation-Based Test Generation: The Java Card Transaction Mechanism Case StudyFabrice Bouquet, Bruno Legeard. 778-795 [doi]
- Checking and Reasoning about Semantic Web through AlloyJin Song Dong, Jing Sun, Hai H. Wang. 796-813 [doi]
- Structuring Retrenchments in B by DecompositionMichael Poppleton, Richard Banach. 814-833 [doi]
- Design of an Automatic Prover Dedicated to the Refinement of Database ApplicationsAmel Mammar, Régine Laleau. 834-854 [doi]
- ProB: A Model Checker for BMichael Leuschel, Michael J. Butler. 855-874 [doi]
- SAT-Based Model-Checking of Security Protocols Using Planning Graph AnalysisAlessandro Armando, Luca Compagna, Pierre Ganty. 875-893 [doi]
- Correctness of Source-Level Safety PoliciesEwen Denney, Bernd Fischer. 894-913 [doi]
- A Topological Characterization of TCP/IP SecurityGiovanni Vigna. 914-939 [doi]