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 A. 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