Books

Short works

Books : reviews

Jeannette M. Wing, Jim Woodcock, Jim Davies, eds.
FM'99 volume 1: World Congress on Formal Methods, Toulouse, September 1999.
Springer. 1999

(read but not reviewed)

Contents

• C. A. R. Hoare. Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle. 1999
• Cliff B. Jones. Scientific Decisions which Characterize VDM. 1999
• John M. Rushby. Mechanized Formal Methods: Where Next?. 1999
• Joseph Sifakis. Integration, the Price of Success (extended abstract). 1999
• Michael Jackson. The Role of Formalism in Method (abstract). 1999
• Eric Conquet, Jean-Luc Marty. Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project.. 1999
• Henk Eertink, Wil Janssen, Paul Oude Luttighuis, Wouter B. Teeuw, Chris A. Vissers. A Business Process Design Language. 1999
• Jan Philipps, Bernhard Rumpe. Refinement of Pipe-and-Filter Architectures. 1999
• John Herbert, Bruno Dutertre, Robert A. Riemenschneider, Victoria Stavridou. A Formalization of Software Architecture. 1999
• Reino Kurki-Suonio. Component and Interface Refinement in Closed-System Specifications. 1999
• Dusko Pavlovic. Semantics of First Order Parametric Specifications. 1999
• Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan. A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. 1999
• Frank Reffel, Stefan Edelkamp. Error Detection with Directed Symbolic Model Checking. 1999
• Rajeev Alur, Joel M. Esposito, M. Kim, Vijay Kumar, Insup Lee. Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination. 1999
• Stavros Tripakis, Karine Altisen. On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems. 1999
• Jean-Michel Couvreur. On-the-Fly Verification of Linear Temporal Logic. 1999
• David Deharbe, Anamaria Martins Moreira. Symbolic Model Checking with Fewer Fixpoint Computations. 1999
• Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, Gigliola Vaglini. Formula Based Abstractions of Transition Systems for Real-Time Model Checking. 1999
• Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier. IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. 1999
• Farn Wang. Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes. 1999
• Denis Sabatier, Pierre Lartigue. The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications. 1999
• Patrick Behm, Paul Benoit, Alain Faivre, Jean-Marc Meynadier. Meteor: A Successful Application of B in a Large Project. 1999
• Brian Matthews, Elvira Locuratolo. Formal Development of Databases in ASSO and B. 1999
• Yann Rouzaud. Interpreting the B-Method in the Refinement Calculus. 1999
• Martin Buchi, Ralph-Johan Back. Compositional Symmetric Sharing in B. 1999
• Cesar Munoz,, John M. Rushby. Structural Embeddings: Mechanization with Method. 1999
• Steve Dunne. The Safe Machine: A New Specification Construct for B. 1999
• Michael J. Butler. csp2B: A Practical Approach to Combining CSP and B. 1999
• Salimeh Behnia, Helene Waeselynck. Test Criteria Definition for B Models. 1999
• Richard F. Paige, Eric C. R. Hehner. Bunches for Object-Oriented, Concurrent, and Real-Time Specification. 1999
• Enn Tyugu, Mihhail Matskin, Jaan Penjam. Applications of Structural Synthesis of Programs. 1999
• Michel Charpentier, K. Mani Chandy. Towards a Compositional Approach to the Design and Verification of Distributed Systems. 1999
• Andre Wong, Marsha Chechik. Formal Modeling in a Commercial Setting: A Case Study. 1999
• Igor Burdonov, Alexander Kossatchev, Alexandre Petrenko, Dmitri Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. 1999
• Lydie du Bousquet. Feature Interaction Detection Using Testing and Model-Checking Experience Report. 1999
• Nisse Husberg, Tapio Manner. Emma: Developing an Industrial Reachability Analyser for SDL. 1999
• Jean-Francois Monin, Francis Klay. Correctness Proof of the Standardized Algorithm for ABR Conformance. 1999
• Thomas Arts, Mads Dam. Verifying a Distributed Database Lookup Manager Written in Erlang. 1999
• Fred Gilham, Robert A. Riemenschneider, Victoria Stavridou. Secure Interoperation of Secure Distributed Databases. 1999
• Volkmar Lotz, Volker Kessler, Georg Walter. A Formal Security Model for Microprocessor Hardware. 1999
• Steve Schneider. Abstraction and Testing. 1999
• Dan Zhou, Shiu-Kai Chin. Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol. 1999
• Patrick Lincoln, John C. Mitchell, Mark Mitchell, Andre Scedrov. Probabilistic Polynomial-Time Equivalence and Security Analysis. 1999
• Riccardo Focardi, Fabio Martinelli. A Uniform Approach for the Definition of Security Properties. 1999
• Paul F. Syverson, Stuart G. Stubblebine. Group Principals and the Formalization of Anonymity. 1999
• Richard F. Paige, Jonathan S. Ostroff. Developing BON as an Industrial-Strength Formal Method. 1999
• Luis Mandel, Maria Victoria Cengarle. On the Expressive Power of OCL. 1999
• Eric Meyer, Jeanine Souquieres. A Systematic Approach to Transform OMT Diagrams to a B Specification. 1999
• Shaoying Liu. Verifying Consistency and Validity of Formal Specifications by Testing. 1999
• Marine Tabourier, Ana R. Cavalli, Melania Ionescu. A GSM-MAP Protocol Experiment Using Passive Testing. 1999

Jeannette M. Wing, Jim Woodcock, Jim Davies, eds.
FM'99 volume 2: World Congress on Formal Methods, Toulouse, September 1999.
Springer. 1999

(read but not reviewed)

Contents

• Pascal Poizat, Christine Choppy, Jean-Claude Royer. From Informal Requirements to COOP: A Concurrent Automata Approach. 1999
• Frederic Lang, Pierre Lescanne, Luigi Liquori. A Framework for Defining Object-Calculi. 1999
• Sanjit Arunkumar Seshia, R. K. Shyamasundar, A. K. Bhattacharjee, S. D. Dhodapkar. A Translation of Statecharts to Esterel. 1999
• Xia Yong, Chris George. An Operational Semantics for Timed RAISE. 1999
• Heike Wehrheim. Data Abstraction for CSP-OZ. 1999
• Fiona Polack, Susan Stepney. Systems Development Using Z Generics. 1999
full paper
• Perry Alexander, Murali Rangarajan, Phillip Baraona. A Brief Summary of VSPEC. 1999
• Gary T. Leavens, Albert L. Baker. Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. 1999
• Markus Muller-Olm, Andreas Wolf. On Excusable and Inexcusable Failures. 1999
• Richard Verhoeven, Roland Carl Backhouse. Interfacing Program Construction and Verification. 1999
• S. Dellacherie, Samuel Devulder, Jean-Luc Lambert. Software Verification Based on Linear Programming. 1999
• Brendan P. Mahony, Jin Song Dong. Sensors and Actuators in TCOZ. 1999
• Bernd Krieg-Bruckner, Jan Peleska, Ernst-Rudiger Olderog, Alexander Baer. The UniForM Workbench, a Universal Development Environment for Formal Methods. 1999
• Bernhard Schatz, Franz Huber. Integrating Formal Description Techniques. 1999
• Stephan Merz. A More Complete TLA. 1999
• Frank S. de Boer, Ulrich Hannemann, Willem-Paul de Roever. Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach. 1999
• Andrew Martin. Relating Z and First-Order Logic. 1999
• Joao Pedro Sousa, David Garlan. Formal Modeling of the Enterprise JavaBeansTM Component Integration Framework. 1999
• Leonid Mikhajlov, Emil Sekerinski, Linas Laibinis. Developing Components in the Presence of Re-entrance. 1999
• H. B. M. Jonkers. Communication and Synchronisation Using Interaction Objects. 1999
• Loe M. G. Feijs. Modelling Microsoft COM Using pi-Calculus. 1999
• Irina M. Smarandache, Thierry Gautier, Paul Le Guernic. Validation of Mixed SIGNAL-ALPHA Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints. 1999
• Simin Nadjm-Tehrani, Ove Akerlund. Combining Theorem Proving and Continuous Models in Synchronous Design. 1999
• Juliano Iyoda, Augusto Sampaio, Leila Silva. ParTS: A Partitioning Transformation System. 1999
• He Jifeng. A Behavioral Model for Co-design. 1999
• Ana L. C. Cavalcanti, David A. Naumann. A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. 1999
• Ralph-Johan Back, Anna Mikhajlova, Joakim von Wright. Reasoning About Interactive Systems. 1999
• John Derrick, Eerke A. Boiten. Non-atomic Refinement in Z. 1999
• Eric C. R. Hehner, Andrew M. Gravell. Refinement Semantics and Loop Rules. 1999
• Michel R. V. Chaudron, Jan Tretmans, Klaas Wijbrans. Lessons from the Application of Formal Methods to the Design of a Storm Surge Barrier Control System. 1999
• Steve King, Jonathan Hammond, Rod Chapman, Andy Pryor. The Value of Verification: Positive Experience of Industrial Proof. 1999
• Anne Elisabeth Haxthausen, Jan Peleska. Formal Development and Verification of a Distributed Railway Control System. 1999
• Kaisa Sere, Elena Troubitsyna. Safety Analysis in Formal Specification. 1999
• Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita. Formal Specification and Validation of a Vital Communication Protocol. 1999
• Herve Marchand, Mazen Samaan. Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology. 1999
• Akira Mori, Kokichi Futatsugi. Verifying Behavioural Specifications in CafeOBJ Environment. 1999
• Razvan Diaconescu, Kokichi Futatsugi, Shusaku Iida. Component-Based Algebraic Specification and Verification in CafeOBJ. 1999
• Shin Nakajima. Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks. 1999
• Manuel Clavel, Fransisco Duran, Steven Eker, Jose Meseguer, Mark-Oliver Stehr. Maude as a Formal Meta-tool. 1999
• Joseph A. Goguen, Grigore Rosu. Hiding More of Hidden Algebra. 1999
• Robert Eschbach. A Termination Detection Algorithm: Specification and Verification. 1999
• Erich Gradel, Marc Spielmann. Logspace Reducibility via Abstract State Machines. 1999
• Martin Dunstan, Tom Kelsey, Ursula Martin, Steve Linton. Formal Methods for Extensions to CAS. 1999
• Rosa M. Jimenez, Fernando Orejas. An Algebraic Framework for Higher-Order Modules. 1999
• Famantanantsoa Randimbivololona, Jean Souyris, Patrick Baudin, Anne Pacalet, Jacques Raguideau, Dominique Schoen. Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. 1999
• P. Garbett, J. P. Parkes, M. Shackleton, Stuart Anderson. Secure Synthesis of Code: A Process Improvement Experiment. 1999
• Olivier Hainque, Laurent Pautet, Yann Le Biannic, Eric Nassor. Cronos: A Separate Compilation Toolset for Modular Esterel Applications. 1999